Skip to Main content Skip to Navigation
New interface
Conference papers

Modeling and Machine-Checking Bump-in-the-Wire Security for Industrial Control Systems

Abstract : This chapter describes the formal modeling and machine-checking of a bump-in-the-wire device that secures field device communications in industrial control networks. Field devices serve as the connection points between computer-based control systems and the physical processes being controlled. Industrial control network traffic is routinely checked for transmission errors, but limited mechanisms are available for combating attacks that exploit industrial control protocols to target critical infrastructure assets.This chapter focuses on a bump-in-the-wire solution that can be retrofitted on field devices to provide security functionality. The TLA+ formal specification language in combination with the isolation guarantees provided by the seL4 microkernel are used to demonstrate that the bump-in-the-wire solution provides important security and liveness properties. The resulting machine-checked system correctly applies hash-based message authentication to verify the authenticity of incoming messages while being resistant to attacks.
Document type :
Conference papers
Complete list of metadata
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Monday, October 4, 2021 - 5:49:27 PM
Last modification on : Wednesday, November 3, 2021 - 7:05:58 AM
Long-term archiving on: : Wednesday, January 5, 2022 - 7:06:42 PM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Mehdi Sabraoui, Jeffrey Hieb, Adrian Lauf, James Graham. Modeling and Machine-Checking Bump-in-the-Wire Security for Industrial Control Systems. 13th International Conference on Critical Infrastructure Protection (ICCIP), Mar 2019, Arlington, VA, United States. pp.271-288, ⟨10.1007/978-3-030-34647-8_14⟩. ⟨hal-03364565⟩



Record views


Files downloads