Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Towards Provable Security in Industrial Control Systems Via Dynamic Protocol Attestation

Arthur Amorim, Trevor Kann, Max Taylor, Lance Joneckis

TL;DR

The paper tackles securing industrial control systems by restricting permissible action sequences through a formally specified protocol language embedded in the proof assistant F*, and enforces runtime conformance using dynamic protocol attestation. By proving that protocol conformance implies safety, it reduces the verification burden to the protocol interface rather than the entire ICS, and it provides automation to generate RPC framework code from the formal specification. The methodology is instantiated on Fischertechnik's High Bay Warehouse, where a concrete HBW protocol is specified, translated to Cap'n Proto RPCs, and evaluated for latency and throughput under dynamic attestation, showing moderate overhead. The work advances ICS security by combining formal methods with runtime enforcement, enabling safer operation even under component compromises, and outlines clear avenues for automation and broader RPC framework support.

Abstract

Industrial control systems (ICSs) increasingly rely on digital technologies vulnerable to cyber attacks. Cyber attackers can infiltrate ICSs and execute malicious actions. Individually, each action seems innocuous. But taken together, they cause the system to enter an unsafe state. These attacks have resulted in dramatic consequences such as physical damage, economic loss, and environmental catastrophes. This paper introduces a methodology that restricts actions using protocols. These protocols only allow safe actions to execute. Protocols are written in a domain specific language we have embedded in an interactive theorem prover (ITP). The ITP enables formal, machine-checked proofs to ensure protocols maintain safety properties. We use dynamic attestation to ensure ICSs conform to their protocol even if an adversary compromises a component. Since protocol conformance prevents unsafe actions, the previously mentioned cyber attacks become impossible. We demonstrate the effectiveness of our methodology using an example from the Fischertechnik Industry 4.0 platform. We measure dynamic attestation's impact on latency and throughput. Our approach is a starting point for studying how to combine formal methods and protocol design to thwart attacks intended to cripple ICSs.

Towards Provable Security in Industrial Control Systems Via Dynamic Protocol Attestation

TL;DR

The paper tackles securing industrial control systems by restricting permissible action sequences through a formally specified protocol language embedded in the proof assistant F*, and enforces runtime conformance using dynamic protocol attestation. By proving that protocol conformance implies safety, it reduces the verification burden to the protocol interface rather than the entire ICS, and it provides automation to generate RPC framework code from the formal specification. The methodology is instantiated on Fischertechnik's High Bay Warehouse, where a concrete HBW protocol is specified, translated to Cap'n Proto RPCs, and evaluated for latency and throughput under dynamic attestation, showing moderate overhead. The work advances ICS security by combining formal methods with runtime enforcement, enabling safer operation even under component compromises, and outlines clear avenues for automation and broader RPC framework support.

Abstract

Industrial control systems (ICSs) increasingly rely on digital technologies vulnerable to cyber attacks. Cyber attackers can infiltrate ICSs and execute malicious actions. Individually, each action seems innocuous. But taken together, they cause the system to enter an unsafe state. These attacks have resulted in dramatic consequences such as physical damage, economic loss, and environmental catastrophes. This paper introduces a methodology that restricts actions using protocols. These protocols only allow safe actions to execute. Protocols are written in a domain specific language we have embedded in an interactive theorem prover (ITP). The ITP enables formal, machine-checked proofs to ensure protocols maintain safety properties. We use dynamic attestation to ensure ICSs conform to their protocol even if an adversary compromises a component. Since protocol conformance prevents unsafe actions, the previously mentioned cyber attacks become impossible. We demonstrate the effectiveness of our methodology using an example from the Fischertechnik Industry 4.0 platform. We measure dynamic attestation's impact on latency and throughput. Our approach is a starting point for studying how to combine formal methods and protocol design to thwart attacks intended to cripple ICSs.

Paper Structure

This paper contains 21 sections, 14 equations, 8 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Background
  3. Fischertechnik
  4. Overview
  5. High Bay Warehouse
  6. Critical Safety Properties
  7. Attack Model
  8. Threats
  9. Attacker
  10. Trusted Computing Base
  11. Interactive Theorem Provers
  12. Methodology
  13. DSL Design
  14. Syntax
  15. Semantics
  16. ...and 6 more sections

Figures (8)

  • Figure 1: Example attack. An adversary infiltrates the control unit to cause a collision in the warehouse.
  • Figure 2: Image of the Fischertechnik's High Bay Warehouse from fischertechnikHBW
  • Figure 3: Overview of an ICS. The demon icon is located adjacent to components that we assume an attacker controls.
  • Figure 4: Semantics of our DSL.
  • Figure 5: Dynamic protocol attestation.
  • ...and 3 more figures