{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,2]],"date-time":"2026-06-02T10:04:50Z","timestamp":1780394690399,"version":"3.54.1"},"reference-count":70,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2022,11,9]],"date-time":"2022-11-09T00:00:00Z","timestamp":1667952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Dipartimenti di Eccellenza 2018"},{"name":"Ministry of Universities and Research"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Priv. Secur."],"published-print":{"date-parts":[[2023,2,28]]},"abstract":"<jats:p>\n            With the advent of\n            <jats:italic>Industry 4.0<\/jats:italic>\n            , industrial facilities and critical infrastructures are transforming into an ecosystem of heterogeneous physical and cyber components, such as\n            <jats:italic>programmable logic controllers<\/jats:italic>\n            , increasingly interconnected and therefore exposed to\n            <jats:italic>cyber-physical attacks<\/jats:italic>\n            , i.e., security breaches in cyberspace that may adversely affect the physical processes underlying\n            <jats:italic>industrial control systems<\/jats:italic>\n            .\n          <\/jats:p>\n          <jats:p>\n            In this article, we propose a\n            <jats:italic>formal approach<\/jats:italic>\n            based on\n            <jats:italic>runtime enforcement<\/jats:italic>\n            to ensure specification compliance in networks of controllers, possibly compromised by\n            <jats:italic>colluding malware<\/jats:italic>\n            that may locally tamper with actuator commands, sensor readings, and inter-controller communications. Our approach relies on an ad-hoc sub-class of Ligatti et\u00a0al.\u2019s\n            <jats:italic>edit automata<\/jats:italic>\n            to enforce controllers represented in Hennessy and Regan\u2019s\n            <jats:italic>Timed Process Language<\/jats:italic>\n            . We define a synthesis algorithm that, given an alphabet \ud835\udcab of observable actions and a timed correctness property\n            <jats:italic>e<\/jats:italic>\n            , returns a monitor that enforces the property\n            <jats:italic>e<\/jats:italic>\n            during the execution of any (potentially corrupted) controller with alphabet \ud835\udcab, and complying with the property\n            <jats:italic>e<\/jats:italic>\n            . Our monitors do\n            <jats:italic>mitigation<\/jats:italic>\n            by correcting and suppressing incorrect actions of corrupted controllers and by generating actions in full autonomy when the controller under scrutiny is not able to do so in a correct manner. Besides classical requirements, such as\n            <jats:italic>transparency<\/jats:italic>\n            and\n            <jats:italic>soundness<\/jats:italic>\n            , the proposed enforcement enjoys\n            <jats:italic>deadlock- and diverge-freedom<\/jats:italic>\n            of monitored controllers, together with\n            <jats:italic>scalability<\/jats:italic>\n            when dealing with networks of controllers. Finally, we test the proposed enforcement mechanism on a non-trivial case study, taken from the context of industrial water treatment systems, in which the controllers are injected with different malware with different malicious goals.\n          <\/jats:p>","DOI":"10.1145\/3546579","type":"journal-article","created":{"date-parts":[[2022,7,4]],"date-time":"2022-07-04T09:29:48Z","timestamp":1656926988000},"page":"1-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Industrial Control Systems Security via Runtime Enforcement"],"prefix":"10.1145","volume":"26","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3335-234X","authenticated-orcid":false,"given":"Ruggero","family":"Lanotte","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi dell\u2019Insubria, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1712-7492","authenticated-orcid":false,"given":"Massimo","family":"Merro","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Verona, Verona, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5453-1120","authenticated-orcid":false,"given":"Andrei","family":"Munteanu","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Verona, Verona, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,11,9]]},"reference":[{"key":"e_1_3_2_2_2","volume-title":"Programmable Controllers - Part 3: Programming Languages","author":"61131-3 Int\u2019l Standard IEC","year":"2003","unstructured":"Int\u2019l Standard IEC 61131-3. 2003. Programmable Controllers - Part 3: Programming Languages. second ed., Int\u2019l Electrotechnical Commission."},{"key":"e_1_3_2_3_2","volume-title":"Function Blocks - Part 1: Architecture","author":"61499-1 Int\u2019l Standard IEC","year":"2005","unstructured":"Int\u2019l Standard IEC 61499-1. 2005. Function Blocks - Part 1: Architecture. first ed., Int\u2019l Electrotechnical Commission."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3127586"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1145\/266420.266432"},{"key":"e_1_3_2_6_2","first-page":"1","volume-title":"Proceedings of the Black Hat Europe","author":"Abbasi A.","year":"2016","unstructured":"A. Abbasi and M. Hashemi. 2016. Ghost in the PLC designing an undetectable programmable logic controller rootkit via pin control attack. In Proceedings of the Black Hat Europe. 1\u201335."},{"key":"e_1_3_2_7_2","first-page":"34:1\u201334:17","volume-title":"Proceedings of the CONCUR","author":"Aceto L.","year":"2018","unstructured":"L. Aceto, I. Cassar, A. Francalanza, and A. Ing\u00f3lfsd\u00f3ttir. 2018. On runtime enforcement via suppressions. In Proceedings of the CONCUR. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 34:1\u201334:17."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-78089-0_1"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/GHTC.2014.6970342"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5_5"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-013-0195-8"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_3_2_13_2","volume-title":"A Theory of Constructive and Predictable Runtime Enforcement Mechanisms","author":"Bielova M.","year":"2011","unstructured":"M. Bielova. 2011. A Theory of Constructive and Predictable Runtime Enforcement Mechanisms. Ph.D. Dissertation. University of Trento."},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19125-1_6"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_51"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/9.272327"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00231-5"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/1966913.1966959"},{"key":"e_1_3_2_19_2","volume-title":"Developing Theoretical Foundations for Runtime Enforcement","author":"Cassar I.","year":"2020","unstructured":"I. Cassar. 2020. Developing Theoretical Foundations for Runtime Enforcement. Ph.D. Dissertation. University of Malta and Reykjavik University."},{"key":"e_1_3_2_20_2","first-page":"1","volume-title":"Proceedings of the Black Hat USA","author":"Pinto A. Di","year":"2018","unstructured":"A. Di Pinto, Y. Dragoni, and A. Carcano. 2018. TRITON: The first ICS cyber attack on safety instrument systems. In Proceedings of the Black Hat USA (2018). 1\u201328."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/CDC.1998.758209"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.5555\/3115971.3116162"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0114-4"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2021.104704"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","DOI":"10.23919\/ACC.2018.8431324"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/2678062"},{"issue":"4","key":"e_1_3_2_27_2","first-page":"76:1\u201376:36","article-title":"A survey of physics-based attack detection in cyber-physical systems","volume":"51","author":"Giraldo J.","year":"2018","unstructured":"J. Giraldo, D. I. Urbina, A. Cardenas, J. Valente, M. Faisal, J. Ruths, N. O. Tippenhauer, H. Sandberg, and R. Candell. 2018. A survey of physics-based attack detection in cyber-physical systems. ACM Computing Surveys 51, 4 (2018), 76:1\u201376:36.","journal-title":"ACM Computing Surveys"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-71368-7_8"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-72817-9_8"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.12.024"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1041"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2005.843874"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijcip.2009.06.001"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-90-481-9157-4"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49052-6_9"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0276-9"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/MSPEC.2013.6471059"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-53733-7_8"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF49147.2020.00025"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2021.08.021"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/CSF51468.2021.00040"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373270"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104618"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10207-004-0046-8"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/892426"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.08.029"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1109\/CySWater.2016.7469060"},{"key":"e_1_3_2_48_2","volume-title":"9.7.0.1190202 (R2019b)","year":"2018","unstructured":"MATLAB. 2018. 9.7.0.1190202 (R2019b). The MathWorks Inc., Natick, Massachusetts."},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/2523649.2523673"},{"key":"e_1_3_2_50_2","unstructured":"Mentor Graphics. 2014. Mentor Graphics ModelSim. Retrieved on 17 July 2022 https:\/\/cseweb.ucsd.edu\/classes\/fa10\/cse140L\/lab\/docs\/modelsim_user.pdf."},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1145\/2461446.2461456"},{"key":"e_1_3_2_52_2","volume-title":"Introduction to Industrial Automation","author":"Nikolakopoulos G.","year":"2018","unstructured":"G. Nikolakopoulos and S. Manesis. 2018. Introduction to Industrial Automation. Taylor & Francis Group."},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.5555\/2501720"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2019.2945520"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","DOI":"10.1145\/3126500"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40648-0_7"},{"key":"e_1_3_2_57_2","unstructured":"B. Radvanovsky. 2013. Project shine: 1 000 000 internet-connected SCADA and ICS stystems and counting. 19 (2013). Tofino Security ."},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/1837274.1837461"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1137\/0325013"},{"key":"e_1_3_2_60_2","unstructured":"Raspberry Pi. 2019. Raspberry Pi 4 Model B. Retrieved 10 June 2022 from https:\/\/www.raspberrypi.org\/products\/raspberry-pi-4-model-b\/."},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1145\/353323.353382"},{"key":"e_1_3_2_62_2","first-page":"469","article-title":"Mobile robots","author":"Siciliano Bruno","year":"2009","unstructured":"Bruno Siciliano, Lorenzo Sciavicco, Luigi Villani, and Giuseppe Oriolo. 2009. Mobile robots. Robotics: Modelling, Planning and Control (2009), 469\u2013521.","journal-title":"Robotics: Modelling, Planning and Control"},{"key":"e_1_3_2_63_2","first-page":"1","article-title":"Anatomy of an attack: Detecting and defeating CRASHOVERRIDE","author":"Slowik J.","year":"2018","unstructured":"J. Slowik. 2018. Anatomy of an attack: Detecting and defeating CRASHOVERRIDE. VB\u201918, (2018), October, 1\u201323.","journal-title":"VB\u201918, (2018),"},{"key":"e_1_3_2_64_2","first-page":"1","volume-title":"Proceedings of the Black Hat Asia","author":"Spenneberg R.","year":"2016","unstructured":"R. Spenneberg, M. Br\u00fcggerman, and H. Schwartke. 2016. PLC-blaster: A worm living solely in the PLC. In Proceedings of the Black Hat Asia. 1\u201316."},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","DOI":"10.5555\/1502144"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.5555\/983326"},{"key":"e_1_3_2_67_2","unstructured":"Xilinx. 2022. Vivado design suite. White Paper 5 (2012) 1\u201330."},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2015.2460391"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1109\/TAC.2015.2484359"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2009.128"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1145\/2829988.2790029"}],"container-title":["ACM Transactions on Privacy and Security"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3546579","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3546579","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:44:02Z","timestamp":1750272242000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3546579"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,9]]},"references-count":70,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,2,28]]}},"alternative-id":["10.1145\/3546579"],"URL":"https:\/\/doi.org\/10.1145\/3546579","relation":{},"ISSN":["2471-2566","2471-2574"],"issn-type":[{"value":"2471-2566","type":"print"},{"value":"2471-2574","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,9]]},"assertion":[{"value":"2021-04-29","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-06-22","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-11-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}