Detection of Ladder Logic Bombs in PLC Control Programs: an Architecture based on Formal Verification
Abstract
Industrial Control Systems (ICS) are responsible for the operations of production plants and critical infrastructures such as nuclear plants and smart grids. Since failures in such systems may harm people, damage properties, and affect the environment, security (in addition to safety) concerns are of paramount importance. In this work, we present a formal verification architecture for the detection of Ladder Logic Bombs, a class of attacks aimed at disrupting the normal operation of Programmable Logic controllers (PLCs). We built a dataset of PLC programs modeling the control logic of a physical system, containing thirty malicious and thirty legitimate samples, then we tested the proposed framework showing that it is able to detect LLBs with very high values of accuracy and precision.
Integrity signals
Registry
Cites
Statistics
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
Other-data-type-driven anomaly detection studies deliberately move beyond conventional network and process data to monitor artifacts that are closer to the root cause of cyber-physical compromise-such as PLC control logic structure, acoustic side-channel signals, host-level physical resource usage, and power-consumption traces-thereby covering attack surfaces that packet- or sensor-centric dete
“First, they deliberately move beyond conventional network and process data to monitor artifacts that are closer to the root cause of cyber-physical compromise-such as PLC control logic structure, acoustic side-channel signals, host-level physical resource usage, and power-consumption traces-thereby covering attack surfaces that packet- or sensor-centric detectors inherently miss [142-146].”
From AI-Based Anomaly Detection in Industrial Control and Cyber–Physical Systems: A Data-Type-Oriented Systematic Review (2025) · cites this paper as [143]
Cites
de Moura, L., & Bjørner, N. (2008) · Lecture Notes in Computer Science · doi:10.1007/978-3-540-78800-3_24 · Cited by 6,595 · see citing works
Stuxnet: Dissecting a cyberwarfare weapon
Langner, R. (2011) · IEEE Security & Privacy Magazine · doi:10.1109/msp.2011.67 · Cited by 1,922 · see citing works
A Survey on Industrial Control System Testbeds and Datasets for Security Research
Conti, M., Donadel, D., & Turrin, F. (2021) · IEEE Communications Surveys & Tutorials · doi:10.1109/comst.2021.3094360 · Cited by 284 · see citing works
MCMT: A Model Checker Modulo Theories
Ghilardi, S., & Ranise, S. (2010) · Lecture notes in computer science · doi:10.1007/978-3-642-14203-1_3 · Cited by 137 · see citing works
OpenPLC: An open source alternative to automation
Alves, T., Buratto, M., de Souza, F. M., & Rodrigues, T. V. (2014) · IEEE Global Humanitarian Technology Conference (GHTC) · doi:10.1109/ghtc.2014.6970342 · Cited by 132 · see citing works
Modeling programmable logic controllers for logic verification
Moon, I. (1994) · IEEE Control Systems · doi:10.1109/37.272781 · Cited by 115 · see citing works
On Ladder Logic Bombs in Industrial Control Systems
Govil, N., Agrawal, A., & Tippenhauer, N. O. (2017) · Lecture notes in computer science · doi:10.1007/978-3-319-72817-9_8 · Cited by 90 · see citing works
Formal verification of ladder logic programs using NuSMV
Kottler, S., Khayamy, M., Hasan, S. R., & Elkeelany, O. S. A. (2017) · IEEE SoutheastCon · doi:10.1109/secon.2017.7925390 · Cited by 18 · see citing works
AttkFinder: Discovering Attack Vectors in PLC Programs using Information Flow Analysis
Castellanos, J. H., Ochoa, M., Cárdenas, Á. A., Arden, O., & Zhou, J. (2021) · International Symposium on Research in Attacks, Intrusions and Defenses (RAID) · doi:10.1145/3471621.3471864 · Cited by 18 · see citing works
A model-driven engineering approach to formal verification of PLC programs
Farines, J.-M., de Queiroz, M. H., da Rocha, V. G., Carpes, A. M. M., Vernadat, F., & Crégut, X. (2011) · doi:10.1109/etfa.2011.6058983 · Cited by 16 · see citing works
Obtaining formal models from Ladder diagrams
Oliveira, E. A. D. S., da Silva, L. D., Gorgônio, K., Perkusich, Â., & Martins, A. F. (2011) · IEEE International Conference on Industrial Informatics (INDIN) · doi:10.1109/indin.2011.6034994 · Cited by 14 · see citing works
Safe programming of PLC using formal verification methods
Smet, O. D., Couffin, S., Rossi, O., Canet, G., Lesage, J.-J., Schnoebelen, P., Papini, H., Suprieure, E. N., & Fabrications, C. D. (2000) · Cited by 9 · see citing works
Werth, A. W., & Morris, T. H. (2023) · Journal of Cyber Security Technology · doi:10.1080/23742917.2023.2171538 · Cited by 6 · see citing works
Vaidyan, V. M., & Tyagi, A. (2022) · International Conference on Electronic Systems and Intelligent Computing (ICESIC) · doi:10.1109/icesic53714.2022.9783543 · Cited by 4 · see citing works
Formal Verification of ST Programs using CSP
Zhou, Q., Cai, F., Yang, Y., & Wu, C. (2021) · Journal of Physics Conference Series · doi:10.1088/1742-6596/2010/1/012072 · Cited by 2 · see citing works
Flagged first, then by citations
Cited by
Sorted by citations
Seo, J. K., Lee, J., Kim, B., Shim, W., & Seo, J. T. (2025) · Electronics · doi:10.3390/electronics15010020 · Cited by 15 · see citing works
Anomaly Detection Method Considering PLC Control Logic Structure for ICS Cyber Threat Detection
Lee, J. H., Ji, I. H., Jeon, S. H., & Seo, J. T. (2025) · Applied Sciences · doi:10.3390/app15073507 · Cited by 5 · see citing works
Advanced PLC-based Automation for Converging System and Warehousing
Vijayachitra, S., Prabhu, K., Agilan, S., Salih, M. A., & Madhumitha, S. (2025) · International Conference Trends Material Science and Inventive Materials · doi:10.1109/ictmim65579.2025.10988042 · Cited by 1 · see citing works
Benchmarking of OpenPLC Runtime on C-DAC VEGA RISC-V Microcontroller
Retnakumari, V. A., Veettil, P. A., Sivakumaran, N., & Rajadurai, S. R. S. (2025) · Premier journal of science. · doi:10.70389/pjs.100135
Static analysis for Ladder Logic Bombs (LLB) detection in Programmable Logic Controllers (PLC)
de Miranda, D. S., & Hayashi, V. T. (2026) · Simpósio Brasileiro de Cibersegurança (SBSeg) · doi:10.5753/sbseg.2026.27121
- Authors
- Iacobelli, A., Rinieri, L., Melis, A., Sadi, A. A., Prandini, M., & Callegati, F.
- Affiliations
- University of Bologna (IT)
- Venue
- 2024 IEEE 7th International Conference on Industrial Cyber-Physical Systems (ICPS)
- Publisher
- IEEE
- Published
- 2024-05-12
- Pages
- 1-7
- OpenAlex
- W4401880629
- Cited by
- 5
- References
- 15
- Citations by year
- 2026: 1 · 2025: 4
- FWCI
- 3.14
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- IEEE International Conference on Industrial Cyber-Physical Systems (ICPS) (publishedVersion)
- Archivio istituzionale della ricerca (Alma Mater Studiorum Università di Bologna) (submittedVersion)
- Topics
- Physical Sciences › Engineering › Control and Systems Engineering › Smart Grid Security and Resilience
- Physical Sciences › Engineering › Control and Systems Engineering › Industrial Automation and Control Systems
- Physical Sciences › Computer Science › Artificial Intelligence › Security and Verification in Computing
- Keywords
- programmable logic controller, industrial control systems, formal verification, attack detection, PLC control program, malware detection, critical infrastructure security
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
