Towards formal verification of cyber security standards
https://doi.org/10.15514/ISPRAS-2018-30(4)-5
Abstract
Cyber security standards are often used to ensure the security of industrial control systems. Nowadays, these systems are becoming more decentralized, making them more vulnerable to cyber attacks. One of the challenges of implementing cyber security standards for industrial control systems is the inability to verify early that they are compliant with the relevant standards. Cyber security standard compliance is also only validated and not formally verified, often not providing strong proofs of correct use of cyber security standard. In this paper, we propose an approach that uses formal analysis to achieve this. We formally define building blocks necessary to define the system formally in order to enable formal modeling of the system and carry out the analysis using the Alloy Analyzer. Our approach can be used at an early design stage, where problems are less expensive to correct, to ensure that the system has the desired security properties. We show the applicability of our approach by modeling two distinct cyber attacks and mitigations strategies used to defend against these attacks and also evaluate our approach based on its flexibility to handle and combine different aspects of the cyber security standards. We discuss the future directions of our research.
References
1. International Society of Automation. The 62443 Series of Standards. http://isa99.isa.org/Public/Information/The-62443-Series-Overview.pdf, accessed on 13/3/18
2. D. Jackson, Software Abstractions: Logic, Language, and Analysis. Heyward Street, Cambridge, MIT Press, April 2006, iSBN-10: 0-262-10114-9.
3. Tomas Kulik, Peter W. V. Tran-Jørgensen, Jalil Boudjadar, and Carl Schultz. A framework for threat-driven cyber security verification of iot systems. In Proc. of the First International Workshop on Verification and Validation of Internet of Things, Västerås, Sweden, april 2018, in print.
4. C. Bekara. Security issues and challenges for the iot-based smart grid. Procedia Computer Science, vol. 34, 2014, pp. 532–537. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S1877050914009193
5. The Alloy Analyzer Modelling website, http://alloy.mit.edu/alloy/, 2018
6. Tomas Kulik and Peter Gorm Larsen. Extensions to formal security modeling framework. https://github.com/kuliktomas/FCSVIoT/commit/189c7962f7f0870fa5315c31a71a6b35e896e47d, 2018.
7. N. Jazdi. Cyber physical systems in the context of industry 4.0. In Proc. of the 2014 IEEE International Conference on Automation, Quality and Testing, Robotics, May 2014, pp. 1–4.
8. M. Ge and D. S. Kim. A framework for modeling and assessing security of the internet of things. In Proc. of the 2015 IEEE 21st International Conference on Parallel and Distributed Systems (ICPADS), 2015, pp. 776–781.
9. C. Heitmeyer, M. Archer, E. Leonard, and J. McLean. Applying Formal Methods to a Certifiably Secure Software System. Software Engineering, IEEE Transactions on Software Engineering, vol. 34, no. 1, 2008, pp. 82 –98.
10. A. N. Haidar and A. E. Abdallah. Formal modelling of pki based authentication. Electronic Notes in Theoretical Computer Science, vol. 235, 2009, pp. 55 – 70. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S157106610900084X
11. D. C. Wardell, R. F. Mills, G. L. Peterson, and M. E. Oxley. A method for revealing and addressing security vulnerabilities in cyber-physical systems by modeling malicious agent interactions with formal verification. Procedia Computer Science, vol. 95, no. Supplement C, 2016, pp. 24 – 31, Available: http://www.sciencedirect.com/science/article/pii/S1877050916324619
12. F. A. Teixeira, F. M. Pereira, H.-C. Wong, J. M. Nogueira, and L. B. Oliveira. Siot: Securing internet of things through distributed systems analysis. Future Generation Computer Systems, 2017. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S0167739X17304235
13. J. Woodcock, S. Stepney, D. Cooper, J. A. Clark, and J. Jacob. The Certification of the Mondex Electronic Purse to ITSEC Level E6. Formal Aspects of Computing, vol. 20, no. 1, 2008, pp. 5–19.
14. D. K. Holstein and K. Stouffer. Trust but verify critical infrastructure cyber security solutions. In Proc. of the 43rd Hawaii International Conference on System Sciences, 2010, pp. 1–8.
15. S. Morimoto, S. Shigematsu, Y. Goto, and J. Cheng. Formal verification of security specifications with common criteria. In Proceedings of the 2007 ACM Symposium on Applied Computing, ser. SAC ’07, 2007, pp. 1506–1512. [Online]. Available: http://doi.acm.org/10.1145/1244002.1244325
16. L. Lamport, Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc., 2002, Boston, MA, USA, 384 pages.
Review
For citations:
Kulik T., Larsen P.G. Towards formal verification of cyber security standards. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(4):79-94. https://doi.org/10.15514/ISPRAS-2018-30(4)-5
Email this article 