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.

翻译：工业控制系统（ICS）日益依赖易受网络攻击的数字技术。网络攻击者能够渗透ICS并执行恶意操作。单独来看，每个操作似乎无害，但综合起来会导致系统进入不安全状态。此类攻击已造成物理损坏、经济损失和环境灾难等严重后果。本文提出一种利用协议限制操作的方法论，这些协议仅允许安全操作的执行。协议采用我们嵌入交互式定理证明器（ITP）的领域特定语言编写，ITP支持形式化、机器可验证的证明，以确保协议保持安全属性。我们采用动态认证技术，即使攻击者已攻陷系统组件，仍能保证ICS符合其协议规范。由于协议一致性可阻止不安全操作，前述网络攻击将无法实现。我们通过Fischertechnik工业4.0平台的案例验证了该方法的有效性，并测量了动态认证对系统延迟与吞吐量的影响。本研究为探索如何结合形式化方法与协议设计以抵御旨在瘫痪ICS的攻击提供了起点。