Formal Security Analysis of Cloud-Connected Industrial Control Systems

  • Tomas KulikEmail author
  • Peter W. V. Tran-Jørgensen
  • Jalil Boudjadar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11359)


Industrial control systems are changing from isolated to remotely accessible cloud-connected architectures. Despite their advantages, these architectures introduce extra complexity, which makes it more difficult to ensure the security of these systems prior to deployment. One way to address this is by using formal methods to reason about the security properties of these systems during the early stages of development. Specifically, by analyzing security attacks and verifying that the corresponding mitigation strategies work as intended. In this paper, we present a formal framework for security analysis of cloud-connected industrial control systems. We consider several well-known attack scenarios and formally verify mitigation strategies for each of them. Our framework is mechanized using TLA+ in order to enable formal verification of security properties. Finally we demonstrate the applicability of our work using an industrial case study.


Control systems Cloud systems Security Formal verification Model checking TLA 


  1. 1.
    Baker, T., Mackay, M., Shaheed, A., Aldawsari, B.: Security-oriented cloud platform for SOA-based SCADA. In: 2015 15th IEEE/ACM International Symposium on Cluster, Cloud and Grid Computing, pp. 961–970, May 2015.
  2. 2.
    Bekara, C.: Security issues and challenges for the IoT-based smart grid. Procedia Comput. Sci. 34, 532–537 (2014)., The 9th International Conference on Future Networks and Communications (FNC 2014)/The 11th International Conference on Mobile Systems and Pervasive Computing (MobiSPC 2014)/Affiliated WorkshopsCrossRefGoogle Scholar
  3. 3.
    Bodeveix, J.-P., Boudjadar, A., Filali, M.: An alternative definition for timed automata composition. In: Bultan, T., Hsiung, P.-A. (eds.) ATVA 2011. LNCS, vol. 6996, pp. 105–119. Springer, Heidelberg (2011). Scholar
  4. 4.
    Chen, P., Cheng, S., Chen, K.: Information fusion to defend intentional attack in internet of things. IEEE Internet Things J. 1(4), 337–348 (2014). Scholar
  5. 5.
    Cui, A., Costello, M., Stolfo, S.J.: When firmware modifications attack: a case study of embedded exploitation. In: NDSS (2013)Google Scholar
  6. 6.
    Ge, M., Kim, D.S.: A framework for modeling and assessing security of the internet of things. In: 2015 IEEE 21st International Conference on Parallel and Distributed Systems (ICPADS), pp. 776–781 (2015).
  7. 7.
    Gunawan, L.A., Herrmann, P.: Compositional verification of application-level security properties. In: Jürjens, J., Livshits, B., Scandariato, R. (eds.) ESSoS 2013. LNCS, vol. 7781, pp. 75–90. Springer, Heidelberg (2013). Scholar
  8. 8.
    Hawblitzel, C., et al.: Ironclad apps: end-to-end security via automated full-system verification. In: Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI 2014, pp. 165–181. USENIX Association, Berkeley (2014).
  9. 9.
    Jeon, B.S., Na, J.C.: A study of cyber security policy in industrial control system using data diodes. In: 2016 18th International Conference on Advanced Communication Technology (ICACT), pp. 314–317, January 2016.
  10. 10.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co. Inc., Boston (2002)Google Scholar
  11. 11.
    Lamport, L.: The PlusCal algorithm language. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 36–60. Springer, Heidelberg (2009). Scholar
  12. 12.
    Miller, B., Rowe, D.: A survey SCADA of and critical infrastructure incidents. In: Proceedings of the 1st Annual Conference on Research in Information Technology, RIIT 2012, pp. 51–56. ACM, New York (2012).
  13. 13.
    Pedroza, G., Apvrille, L., Knorreck, D.: AVATAR: a SysML environment for the formal verification of safety and security properties. In: 2011 11th Annual International Conference on New Technologies of Distributed Systems, pp. 1–10, May 2011.
  14. 14.
    Piggin, R.S.H.: Securing SCADA in the cloud: managing the risks to avoid the perfect storm. In: IET Conference Proceedings, pp. 1.2–1.2(1), January 2014.
  15. 15.
    Rong, C., Nguyen, S.T., Jaatun, M.G.: Beyond lightning: a survey on security challenges in cloud computing. Comput. Electr. Eng. 39(1), 47–54 (2013)., Special issueon Recent Advanced Technologies and Theories for Grid and Cloud Computingand Bio-engineeringCrossRefGoogle Scholar
  16. 16.
    Sheyner, O., Haines, J., Jha, S., Lippmann, R., Wing, J.M.: Automated generation and analysis of attack graphs. In: Proceedings 2002 IEEE Symposium on Security and Privacy, pp. 273–284, May 2002.
  17. 17.
    Shrestha, R., Mehrpouyan, H., Xu, D.: Model checking of security properties in industrial control systems (ICS). In: Proceedings of the Eighth ACM Conference on Data and Application Security and Privacy, CODASPY 2018, pp. 164–166. ACM, New York (2018).
  18. 18.
    Ten, C., Manimaran, G., Liu, C.: Cybersecurity for Critical infrastructures: attack and defense modeling. IEEE Trans. Syst. Man Cybern. B Cybern. - Part A: Syst. Hum. 40(4), 853–865 (2010). Scholar
  19. 19.
    Kulik, T., Peter W.V.: Tran-Jørgensen and Jalil Boudjadar: TLA+ model for security verification of industrial cloud-connected control system (2018).
  20. 20.
    Wardell, D.C., Mills, R.F., Peterson, G.L., Oxley, M.E.: A method for revealing and addressing security vulnerabilities in cyber-physical systems by modeling malicious agent interactions with formal verification. Procedia Comput. Sci. 95, 24–31 (2016)., Complex Adaptive Systems Los Angeles, CA November 2-4, 2016CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Tomas Kulik
    • 1
    Email author
  • Peter W. V. Tran-Jørgensen
    • 1
  • Jalil Boudjadar
    • 1
  1. 1.DIGIT, Department of EngineeringAarhus UniversityAarhusDenmark

Personalised recommendations