HyTwin: Hybrid Program Semantics for Digital Twin-Based Security Interventions in Industrial Control Systems

HyTwin: Hybrid Program Semantics for Digital Twin-Based Security Interventions in Industrial Control Systems

연구 분야: Infrastructure

학회: NASA Formal Methods Symposium

Industrial control systems (ICS) are increasingly targeted by sophisticated attacks on sensors and actuators, necessitating advanced frameworks that enable proactive mitigation. This paper introduces HYTWIN, a formal framework that models both adversarial actions and corresponding mitigation strategies through digital twin-based interventions. HYTWIN leverages differential dynamic logic (dL) to represent the temporal evolution of attacks and quantify the mitigation horizon, a critical parameter enabling precise reasoning about when and how to deploy fail-safe mechanisms during ongoing attacks. Our approach integrates temporal semantics with attack models to dynamically engage fail-safe controls. This work provides a rigorous framework for designing proactive countermeasures that preserve system safety, ensuring robustness in adversarial scenarios. The proposed framework establishes a foundation for advancing ICS security through verifiable temporal reasoning and contributes to bridging gaps between theoretical modeling and real-world industrial applications.