| Title | Towards Formal Security Analysis of Industrial Control Systems |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Rocchetto, Marco, Tippenhauer, Nils Ole |
| Conference Name | Proceedings of the 2017 ACM on Asia Conference on Computer and Communications Security |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4944-4 |
| Keywords | composability, cyber-physical system, formal analysis, formal methods, formal models, Metrics, physical layer security, practical security assessment, pubcrawl, resilience, Resiliency, security |
| Abstract | We discuss the use of formal modeling to discover potential attacks on Cyber-Physical systems, in particular Industrial Control Systems. We propose a general approach to achieve that goal considering physical-layer interactions, time and state discretization of the physical process and logic, and the use of suitable attacker profiles. We then apply the approach to model a real-world water treatment testbed using ASLan++ and analyze the resulting transition system using CL-AtSe, identifying four attack classes. To show that the attacks identified by our formal assessment represent valid attacks, we compare them against practical attacks on the same system found independently by six teams from industry and academia. We find that 7 out of the 8 practical attacks were also identified by our formal assessment. We discuss limitations resulting from our chosen level of abstraction, and a number of modeling shortcuts to reduce the runtime of the analysis. |
| URL | http://doi.acm.org/10.1145/3052973.3053024 |
| DOI | 10.1145/3052973.3053024 |
| Citation Key | rocchetto_towards_2017 |
Towards Formal Security Analysis of Industrial Control Systems