Marco Rocchetto
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.
- S. Adepu and A. Mathur. An investigation into the response of a water treatment system into cyber attacks. In IEEE Symposium on High Assurance Systems Engineering (HASE), 2015. Google Scholar
Digital Library
- D. Antonioli, H. R. Ghaeini, S. Adepu, M. Ochoa, and N. O. Tippenhauer. Gamifying education and research on ics security: Design, implementation and results of s3. 2017. Cornell University, ArXiv e-Prints, http://arxiv.org/abs/1702.03067v1.Google Scholar
- A. Armando, W. Arsac, T. Avanesov, M. Barletta, A. Calvi, A. Cappai, R. Carbone, Y. Chevalier, L. Compagna, J. Cuéllar, G. Erzse, S. Frau, M. Minea, S. Mödersheim, D. von Oheimb, G. Pellegrino, S. E. Ponta, M. Rocchetto, M. Rusinowitch, M. T. Dashti, M. Turuani, and L. Viganò. The AVANTSSAR platform for the automated validation of trust and security of service-oriented architectures. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pages 267--282, 2012. Google ScholarDigital Library
- A. Armando, D. A. Basin, Y. Boichut, Y. Chevalier, L. Compagna, J. Cuéllar, P. H. Drielsma, P. Héam, O. Kouchnarenko, J. Mantovani, S. Mödersheim, D. von Oheimb, M. Rusinowitch, J. Santiago, M. Turuani, L. Viganò, and L. Vigneron. The AVISPA tool for the automated validation of internet security protocols and applications. In Proceedings of Computer Aided Verification, (CAV), pages 281--285, 2005. Google ScholarDigital Library
- A. Armando and L. Compagna. SATMC: a SAT-based model checker for security protocols. In JELIA, LNAI 3229. Springer, 2004.Google Scholar
- AVANTSSAR. Deliverable 5.3: AVANTSSAR Library of validated problem cases. www.avantssar.eu, 2010.Google Scholar
- AVANTSSAR. Deliverable 2.3 (update): ASLan++ specification and tutorial, 2011. Available at http://www.avantssar.eu.Google Scholar
- D. Basin, S. Capkun, P. Schaller, and B. Schmidt. Let's get physical: Models and methods for real-world security protocols. In Proceedings of Theorem Proving in Higher Order Logics, 2009. Google ScholarDigital Library
- D. Basin, S. Capkun, P. Schaller, and B. Schmidt. Formal reasoning about physical properties of security protocols. Transactions on Information and System Security (TISSEC), 14(2):16, 2011. Google ScholarDigital Library
- D. Basin, S. Mödersheim, and L. Viganò. OFMC: A symbolic model checker for security protocols. Journal of Information Security, 4(3):181--208, 2005. Google ScholarDigital Library
- M. Bugliesi, S. Calzavara, S. Mödersheim, and P. Modesti. Security protocol specification and verification with AnBx. behaviour, 15:16, 2015.Google Scholar
- A. A. Cárdenas, S. M. Amin, B. Sinopoli, A. Giani, A. Perrig, and S. S. Sastry. Challenges for securing cyber physical systems. In Workshop on Future Directions in Cyber-physical Systems Security. DHS, July 2009.Google Scholar
- A. A. Cárdenas, T. Roosta, and S. Sastry. Rethinking security properties, threat models, and the design space in sensor networks: A case study in SCADA systems. Ad Hoc Networks, 7(8):1434--1447, 2009. Google ScholarDigital Library
- D. E. Denning. Activism, hacktivism, and cyberterrorism: The internet as a tool for influencing foreign policy. In Networks and Netwars: The Future of Terror, Crime, and Militancy. RAND Corporation, 2001. Google ScholarDigital Library
- P. Derler, E. A. Lee, and A. S. Vincentelli. Modeling cyber-physical systems. Proceedings of the IEEE, 100(1):13--28, Jan 2012.Google ScholarCross Ref
- D. Dolev and A. C. Yao. On the security of public key protocols. IEEE Transactions on Information Theory, 29(2):198--207, 1983. Google ScholarDigital Library
- A. Doupé, M. Cova, and G. Vigna. Why Johnny Can't Pentest: An Analysis of Black-Box Web Vulnerability Scanners, pages 111--131. Springer Berlin Heidelberg, 2010.Google Scholar
- B. Feddersen, K. Keefe, W. H. Sanders, C. Muehrcke, D. Parks, A. Crapo, A. Gabaldon, and R. Palla. An ontological model for constructing mobius advise security models. In Proceedings of Conference on Dependable Systems and Networks (DSN), 2015.Google Scholar
- M. D. Ford, K. Keefe, E. LeMay, W. H. Sanders, and C. Muehrcke. Implementing the ADVISE security modeling formalism in möbius. In IEEE/IFIP Conference on Dependable Systems and Networks (DSN), 2013. Google ScholarDigital Library
- B. Galloway and G. Hancke. Introduction to industrial control networks. Communications Surveys Tutorials, IEEE, 15(2):860--880, 2013.Google ScholarCross Ref
- D. Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, 2006. Google ScholarDigital Library
- K. H. John and M. Tiegelkamp. IEC 61131--3: Programming Industrial Automation Systems Concepts and Programming Languages, Requirements for Programming Systems, Decision-Making Aids. Springer, 2nd edition, 2010. Google ScholarDigital Library
- E. Kang, S. Adepu, D. Jackson, and A. P. Mathur. Model-based security analysis of a water treatment system. In Proceedings of the Workshop on Software Engineering for Smart Cyber-Physical Systems, pages 22--28. ACM, 2016. Google ScholarDigital Library
- E. LeMay, M. D. Ford, K. Keefe, W. H. Sanders, and C. Muehrcke. Model-based security metrics using adversary view security evaluation (ADVISE). In Proceedings of Conference on Quantitative Evaluation of Systems, QEST, 2011. Google ScholarDigital Library
- A. Mathur and N. O. Tippenhauer. A water treatment testbed for research and training on ics security. In Proceedings of Workshop on Cyber-Physical Systems for Smart Water Networks (CySWater), Apr. 2016.Google ScholarCross Ref
- A. Ornaghi and M. Valleri. Ettercap. https://ettercap.github.io/ettercap/, last visited August 3 2016.Google Scholar
- M. Rocchetto, M. Ochoa, and M. Torabi Dashti. Model-based detection of CSRF. In ICT Systems Security and Privacy Protection, volume 428 of IFIP Advances in Information and Communication Technology. Springer Berlin Heidelberg, 2014.Google ScholarCross Ref
- M. Rocchetto and N. O. Tippenhauer. APE (Attacker Profile Examiner), 2016. Available at http://research.scy-phy.net/ape/.Google Scholar
- M. Rocchetto and N. O. Tippenhauer. ASLan++ formal model of SWaT, 2016. Available at https://research.scy-phy.net/swatmodel.Google Scholar
- M. Rocchetto and N. O. Tippenhauer. CPDY: Extending the dolev-yao attacker with physical-layer interactions. In Proceedings of the International Conference on Formal Engineering Methods (ICFEM), 2016.Google ScholarCross Ref
- M. Rocchetto and N. O. Tippenhauer. On attacker models and profiles for cyber-physical systems. In Proceedings of the European Simposium on Research in Computer Security (ESORICS), 2016.Google ScholarCross Ref
- P. Schaller, B. Schmidt, D. A. Basin, and S. Capkun. Modeling and verifying physical properties of security protocols for wireless networks. In Computer Security Foundations Symposium (CSF), pages 109--123, 2009. Google ScholarDigital Library
- V. Schiffer, D. Vangompel, and R. Voss. The common industrial protocol (CIP) and the family of CIP networks. ODVA, 2006.Google Scholar
- M. Schmidt and H. Lipson. Distilling free-form natural laws from experimental data. science, 324(5923):81--85, 2009.Google Scholar
- R. Software. Studio 5000®. http://www.rockwellautomation.com/rockwellsoftware/products/studio-5000.page, last visited August 3 2016.Google Scholar
- D. Steinmetzer, M. Schulz, and M. Hollick. Lockpicking physical layer key exchange: Weak adversary models invite the thief. In Proc. ACM Conference Wireless Security (WiSeC), 2015. Google ScholarDigital Library
- M. Turuani. The CL-Atse Protocol Analyser. In RTA, LNCS 4098, 2006. Google ScholarDigital Library
- D. Urbina, J. Giraldo, N. O. Tippenhauer, and A. Cardenas. Attacking fieldbus communications in ICS: Applications to the SWaT testbed. In Proceedings of Singapore Cyber Security R&D Conference (SG-CRC), Jan. 2016.Google Scholar
- R. Vigo. The cyber-physical attacker. In Proceedings of Workshop of Conference on Computer Safety, Reliability, and Security (SAFECOMP), 2012. Google ScholarDigital Library
- D. von Oheimb and S. Mödersheim. ASLan++ -- a formal security specification language for distributed systems. In FMCO, LNCS 6957. Springer, 2010. Google ScholarDigital Library
- A. H. Vu, N. O. Tippenhauer, B. Chen, D. M. Nicol, and Z. Kalbarczyk. CyberSAGE: A tool for automatic security assessment of cyber-physical systems. In Proceeding of Quantitative Evaluation of Systems (QEST), pages 384--387, 2014.Google ScholarCross Ref
- S. Weinberger. Computer security: Is this the start of cyberwarfare? Nature, 174:142--145, June 2011.Google ScholarCross Ref
Index Terms
- Towards Formal Security Analysis of Industrial Control Systems
Recommendations
Using high-level synthesis and formal analysis to predict and preempt attacks on industrial control systems
FPGA '14: Proceedings of the 2014 ACM/SIGDA international symposium on Field-programmable gate arraysIndustrial control systems (ICSes) have the conflicting requirements of security and network access. In the event of large-scale hostilities, factories and infrastructure would more likely be targeted by computer viruses than the bomber squadrons used ...
A Formal Framework for ASTRAL Intralevel Proof Obligations
ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Comments