Formal Verification of Security Pattern Composition: Application to SCADA

Authors

  • Fadi Obeid Université Bretagne Loire, Laboratoire Lab-STICC, UMR CNRS 6285, ENSTA Bretagne, 29200 Brest, France
  • Philippe Dhaussy Université Bretagne Loire, Laboratoire Lab-STICC, UMR CNRS 6285, ENSTA Bretagne, 29200 Brest, France

DOI:

https://doi.org/10.31577/cai_2019_5_1149

Keywords:

Information security, security patterns, formal verification, model checking, SCADA

Abstract

Information security was initially required in specific applications, however, nowadays, most companies and even individuals are interested in securing their information assets. The new requirement can be costly, especially with the high demand on security solutions and security experts. Security patterns are reusable security solutions that prove to be efficient and can help developers achieve some security goals without the need for expertise in the security domain. Some security pattern combinations can be beneficial while others are inconsistent. Model checking can be used to verify the production of combining multiple security patterns with an architecture. Supervisory control and data acquisition (SCADA) systems control many of our critical industrial infrastructures. Due to their limitations, and their augmented connectivity, SCADA systems have many unresolved security issues. In this paper, we demonstrate how we can automatically generate a secure SCADA model based on an insecure one and how to verify the generated model.

Downloads

Download data is not yet available.

Downloads

Published

2020-02-11

How to Cite

Obeid, F., & Dhaussy, P. (2020). Formal Verification of Security Pattern Composition: Application to SCADA. Computing and Informatics, 38(5), 1149–1180. https://doi.org/10.31577/cai_2019_5_1149