Formally designing and implementing cyber security mechanisms in industrial control networks.

seL4;TLA+;model checking;CAmkES;verification;cyber security

Mehdi Sabraoui

University:University of Louisville

Department:Computer Engineering and Computer Science

关键词: seL4;    TLA+;    model checking;    CAmkES;    verification;    cyber security;   

Others  :  https://ir.library.louisville.edu/cgi/viewcontent.cgi?article=4490&context=etd

美国|英语

来源: The Universite of Louisville's Institutional Repository

【 摘 要 】

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.