More Web Proxy on the site http://driver.im/

research-article

A process calculus approach to detection and mitigation of PLC malware

Authors:

Ruggero Lanotte,

Andrei MunteanuAuthors Info & Claims

Volume 890, Issue C

Pages 125 - 146

https://doi.org/10.1016/j.tcs.2021.08.021

Published: 12 October 2021 Publication History

Highlights

•

Timed process calculi for expressing both genuine and malicious activities within a PLC.

•

Runtime enforcement based on Ligatti et al.’s edit automata.

•

Algorithms to synthesise edit automata from PLC specifications.

•

Simulation and bisimulation proof techniques.

•

Simulations of a significant use case in Simulink/Matlab.

Abstract

We define a simple process calculus, based on Hennessy and Regan's Timed Process Language, for specifying networks of communicating programmable logic controllers (PLCs) enriched with monitors enforcing specification compliance at runtime. We define a synthesis algorithm that given an uncorrupted PLC returns a monitor that enforces the correctness of the PLC, even when injected with malware that may forge/drop actuator commands and inter-controller communications. Then, we strengthen the capabilities of our monitors by allowing the insertion of actions to mitigate malware activities. This gives us deadlock-freedom monitoring: malware may not drag monitored controllers into deadlock states. Our enforcing monitors represent a formal mechanism for prompt detection of malicious activities within PLCs. Finally, we illustrate our results by implementing in Simulink a non-trivial Water Transmission Network (WTN) system, and testing the effectiveness of our monitors in detecting and mitigating three different attacks targeting the PLCs of our WTN.

References

[1]

R. Lanotte, M. Merro, A. Munteanu, A process calculus approach to correctness enforcement of PLCs, in: ICTCS, CEUR Workshop Proceedings, 2020, pp. 81–95. CEUR-WS.org.

[2]

B. Radvanovsky, Project SHINE: 1,000,000 internet-connected SCADA and ICS systems and counting, Tofino Security, 2013.

[3]

R. Spenneberg, M. Brüggerman, H. Schwartke, PLC-blaster: a worm living solely in the PLC, in: Black Hat, 2016, pp. 1–16.

[4]

A. Abbasi, M. Hashemi, Ghost in the PLC designing an undetectable programmable logic controller rootkit via pin control attack, in: Black Hat Europe, 2016, pp. 1–35.

[5]

S.E. McLaughlin, CPS: stateful policy enforcement for control system device usage, in: ACSAC, ACM, 2013, pp. 109–118.

[6]

S. Mohan, S. Bak, E. Betti, H. Yun, L. Sha, M. Caccamo, S3A: secure system simplex architecture for enhanced security and robustness of cyber-physical systems, in: HiCoNS, ACM, 2013, pp. 65–74.

[7]

J. Giraldo, D.I. Urbina, A. Cardenas, J. Valente, M. Faisal, J. Ruths, N.O. Tippenhauer, H. Sandberg, R. Candell, A survey of physics-based attack detection in cyber-physical systems, ACM Comput. Surv. 51 (4) (2018) 76:1–76:36.

Digital Library

[8]

I. Lanese, L. Bedogni, M. Di Felice, Internet of things: a process calculus approach, in: SAC, ACM, 2013, pp. 1339–1346.

[9]

C. Bodei, P. Degano, G. Ferrari, L. Galletta, Tracing where IoT data are collected and aggregated, Log. Methods Comput. Sci. 13 (3) (2017) 1–38.

[10]

R. Lanotte, M. Merro, A semantic theory of the Internet of Things, Inf. Comput. 259 (1) (2018) 72–101.

[11]

R. Lanotte, M. Merro, A calculus of cyber-physical systems, in: LATA, in: Lecture Notes in Computer Science, vol. 10168, Springer, 2017, pp. 115–127.

[12]

R. Lanotte, M. Merro, S. Tini, A probabilistic calculus of cyber-physical systems, Inf. Comput. 104618 (2021) 1–35.

[13]

M. Abadi, B. Blanchet, C. Fournet, The applied Pi calculus: mobile values, new names, and secure communication, J. ACM 65 (1) (2018) 1:1–1:41.

Digital Library

[14]

M. Abadi, A.D. Gordon, A calculus for cryptographic protocols: the spi calculus, in: CCS, ACM, 1997, pp. 36–47.

[15]

R. Lanotte, M. Merro, A. Munteanu, L. Viganò, A formal approach to physics-based attacks in cyber-physical systems, ACM Trans. Priv. Secur. 23 (1) (2020) 3:1–3:41.

[16]

F.B. Schneider, Enforceable security policies, ACM Trans. Inf. Syst. Secur. 3 (1) (2000) 30–50.

Digital Library

[17]

J. Ligatti, L. Bauer, D. Walker, Edit automata: enforcement mechanisms for run-time security policies, Int. J. Inf. Secur. 4 (1–2) (2005) 2–16.

Digital Library

[18]

Y. Falcone, L. Mounier, J. Fernandez, J. Richier, Runtime enforcement monitors: composition, synthesis, and enforcement abilities, Form. Methods Syst. Des. 38 (3) (2011) 223–262.

[19]

M. Hennessy, T. Regan, A process algebra for timed systems, Inf. Comput. 117 (2) (1995) 221–239.

Digital Library

[20]

N. Govil, A. Agrawal, N.O. Tippenhauer, On ladder logic bombs in industrial control systems, in: SECPRE@ESORICS 2017, in: Lecture Notes in Computer Science, vol. 10683, Springer, 2018, pp. 110–126.

[21]

L. Aceto, A. Achilleos, A. Francalanza, A. Ingólfsdóttir, S.Ö. Kjartansson, On the complexity of determinizing monitors, in: CIAA, in: Lecture Notes in Computer Science, vol. 10329, Springer, 2017, pp. 1–13.

[22]

MATLAB, 9.7.0.1190202 (R2019b), The MathWorks Inc., Natick, Massachusetts, 2018.

[23]

M. Heymann, F. Lin, G. Meyer, S. Resmerita, Analysis of Zeno behaviors in a class of hybrid systems, IEEE Trans. Autom. Control 50 (3) (2005) 376–383.

[24]

M. Leucker, C. Schallhart, A brief account of runtime verification, J. Log. Algebraic Program. 78 (5) (2009) 293–303.

[25]

L. Aceto, A. Achilleos, A. Ingólfsdóttir, K. Lehtinen, Adventures in monitorability: from branching to linear time and back again, in: POPL, ACM, 2019, pp. 52:1–52:29.

[26]

M. Hennessy, Algebraic Theory of Processes, MIT Press, Cambridge, 1988.

Digital Library

[27]

R. Milner, Communication and Concurrency, Prentice Hall, 1989.

Digital Library

[28]

N. Trifunovic, Introduction to Urban Water Distribution: Unesco-IHE Lecture Note Series, CRC Press, 2006.

[29]

M. Barrère, C. Hankin, N. Nicolaou, D.G. Eliades, T. Parisini, Measuring cyber-physical security in industrial control systems via minimum-effort attack strategies, J. Inf. Secur. Appl. 52 (2020).

[30]

L. Aceto, I. Cassar, A. Francalanza, A. Ingólfsdóttir, On runtime enforcement via suppressions, in: CONCUR, Schloss Dagstuhl, 2018, pp. 34:1–34:17.

[31]

M. Bielova, A theory of constructive and predictable runtime enforcement mechanisms, Ph.D. thesis University of Trento, 2011.

[32]

Y. Falcone, J.-C. Fernandez, L. Mounier, What can you verify and enforce at runtime?, Int. J. Softw. Tools Technol. Transf. 14 (3) (2012) 349–382.

[33]

B. Könighofer, M. Alshiekh, R. Bloem, L. Humphrey, R. Könighofer, U. Topcu, C. Wang, Shield synthesis, Form. Methods Syst. Des. 51 (2) (2017) 332–361.

Digital Library

[34]

A. Francalanza, A theory of monitors, Inf. Comput. (2021).

[35]

P.J. Ramadge, W.M. Wonham, Supervisory Control of a Class of Discrete Event Processes, SIAM J. Control Optim. 25 (1) (1987) 206–230.

Digital Library

[36]

W.M. Brandin, B.A. Wonham, Supervisory control of timed discrete-event systems, IEEE Trans. Autom. Control 39 (2) (1994) 329–342.

[37]

R. Lanotte, M. Merro, A. Munteanu, Runtime enforcement for control system security, in: CSF, IEEE Computer Society, 2020, pp. 246–261.

[38]

N. Bielova, F. Massacci, Predictability of enforcement, in: Engineering Secure Software and Systems, 2011, pp. 73–86.

[39]

Z. Manna, A. Pnueli, A hierarchy of temporal properties, Tech. rep. Stanford University, 1987.

[40]

S. Pinisetty, P.S. Roop, S. Smyth, N. Allen, S. Tripakis, R. Hanxleden, Runtime enforcement of cyber-physical systems, ACM Trans. Embed. Comput. Syst. 16 (5s) (2017) 178:1–178:25.

[41]

F. Martinelli, I. Matteucci, Through modeling to synthesis of security automata, Electron. Notes Theor. Comput. Sci. 179 (2007) 31–46.

[42]

I. Cassar, Developing theoretical foundations for runtime enforcement, Ph.D. thesis University of Malta and Reykjavik University, 2020.

[43]

M. Fabian, A. Hellgren, PLC-based implementation of supervisory control for discrete event systems, CDC, vol. 3, IEEE, 1998, pp. 3305–3310.

Cited By

Lanotte RMerro MMunteanu A(2022)Industrial Control Systems Security via Runtime EnforcementACM Transactions on Privacy and Security10.1145/354657926:1(1-41)Online publication date: 4-Jul-2022
https://dl.acm.org/doi/10.1145/3546579
Moradi FBagheri MRahmati HYazdi HAsadollah SSirjani M(2022)Monitoring Cyber-Physical Systems Using a Tiny Twin to Prevent Cyber-AttacksModel Checking Software10.1007/978-3-031-15077-7_2(24-43)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1007/978-3-031-15077-7_2

Index Terms

A process calculus approach to detection and mitigation of PLC malware

Index terms have been assigned to the content through auto-classification.

Recommendations

Malware detection using adaptive data compression
AISec '08: Proceedings of the 1st ACM workshop on Workshop on AISec

A popular approach in current commercial anti-malware software detects malicious programs by searching in the code of programs for scan strings that are byte sequences indicative of malicious code. The scan strings, also known as the signatures of ...
A semantics-based approach to malware detection
POPL '07: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Malware detection is a crucial aspect of software security. Current malware detectors work by checking for "signatures," which attempt to capture (syntactic) characteristics of the machine-level byte sequence of the malware. This reliance on a syntactic ...
Malware Detection Method Focusing on Anti-debugging Functions
CANDAR '14: Proceedings of the 2014 Second International Symposium on Computing and Networking

Malware has received much attention in recent years. Antivirus software is widely used as a countermeasure against malware. However, some kinds of malware can evade detection by antivirus software, hence, a new detection method is required. In this ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Theoretical Computer Science

Theoretical Computer Science Volume 890, Issue C

Oct 2021

240 pages

ISSN:0304-3975

Issue’s Table of Contents

Elsevier B.V.

Publisher

Elsevier Science Publishers Ltd.

United Kingdom

Publication History

Published: 12 October 2021

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 22 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lanotte RMerro MMunteanu A(2022)Industrial Control Systems Security via Runtime EnforcementACM Transactions on Privacy and Security10.1145/354657926:1(1-41)Online publication date: 4-Jul-2022
https://dl.acm.org/doi/10.1145/3546579
Moradi FBagheri MRahmati HYazdi HAsadollah SSirjani M(2022)Monitoring Cyber-Physical Systems Using a Tiny Twin to Prevent Cyber-AttacksModel Checking Software10.1007/978-3-031-15077-7_2(24-43)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1007/978-3-031-15077-7_2

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents