Date on Master's Thesis/Doctoral Dissertation
8-2019
Document Type
Doctoral Dissertation
Degree Name
Ph. D.
Department
Computer Engineering and Computer Science
Degree Program
Computer Science and Engineering, PhD
Committee Chair
Lauf, Adrian
Committee Co-Chair (if applicable)
Hieb, Jeff
Committee Member
Yampolskiy, Roman
Committee Member
Losavio, Michael
Committee Member
Elmaghraby, Adel
Author's Keywords
seL4; TLA+; model checking; CAmkES; verification; cyber security
Abstract
This dissertation describes progress in the state-of-the-art for developing and deploying formally verified cyber security devices in industrial control networks. It begins by detailing the unique struggles that are faced in industrial control networks and why concepts and technologies developed for securing traditional networks might not be appropriate. It uses these unique struggles and examples of contemporary cyber-attacks targeting control systems to argue that progress in securing control systems is best met with formal verification of systems, their specifications, and their security properties. This dissertation then presents a development process and identifies two technologies, TLA+ and seL4, that can be leveraged to produce a high-assurance embedded security device. The method presented in this dissertation takes an informal design of an embedded device that might be found in a control system and 1) formalizes the design within TLA+, 2) creates and mechanically checks a model built from the formal design, and 3) translates the TLA+ design into a component-based architecture of a native seL4 application. The later chapters of this dissertation describe an application of the process to a security preprocessor embedded device that was designed to add security mechanisms to the network communication of an existing control system. The device and its security properties are formally specified in TLA+ in chapter 4, mechanically checked in chapter 5, and finally its native seL4 architecture is implemented in chapter 6. Finally, the conclusions derived from the research are laid out, as well as some possibilities for expanding the presented method in the future.
Recommended Citation
Sabraoui, Mehdi, "Formally designing and implementing cyber security mechanisms in industrial control networks." (2019). Electronic Theses and Dissertations. Paper 3271.
https://doi.org/10.18297/etd/3271
Included in
Computer and Systems Architecture Commons, Controls and Control Theory Commons, Information Security Commons, OS and Networks Commons, Other Computer Engineering Commons, Software Engineering Commons, Systems Architecture Commons, Theory and Algorithms Commons
