skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.

Explore Research Products in the PAR
It may take a few hours for recently added research products to appear in PAR search results.


This content will become publicly available on June 8, 2026

Title: HyTwin: Hybrid Program Semantics for Digital Twin-Based Security Interventions in Industrial Control Systems
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.  more » « less
Award ID(s):
2427581 2425711
PAR ID:
10639166
Author(s) / Creator(s):
; ;
Publisher / Repository:
Springer Nature Switzerland
Date Published:
Page Range / eLocation ID:
294 to 312
Subject(s) / Keyword(s):
cyber-physical systems differential dynamic logic digital twin security verified attack detection verified attack mitigation
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. ; ; ; (, Electronics)
    null (Ed.)
    Industrial Control Systems (ICS) are used to control physical processes in critical infrastructure. These systems are used in a wide variety of operations such as water treatment, power generation and distribution, and manufacturing. While the safety and security of these systems are of serious concern, recent reports have shown an increase in targeted attacks aimed at manipulating physical processes to cause catastrophic consequences. This trend emphasizes the need for algorithms and tools that provide resilient and smart attack detection mechanisms to protect ICS. In this paper, we propose an anomaly detection framework for ICS based on a deep neural network. The proposed methodology uses dilated convolution and long short-term memory (LSTM) layers to learn temporal as well as long term dependencies within sensor and actuator data in an ICS. The sensor/actuator data are passed through a unique feature engineering pipeline where wavelet transformation is applied to the sensor signals to extract features that are fed into the model. Additionally, this paper explores four variations of supervised deep learning models, as well as an unsupervised support vector machine (SVM) model for this problem. The proposed framework is validated on Secure Water Treatment testbed results. This framework detects more attacks in a shorter period of time than previously published methods. 
    more » « less
  2. (, Numerical Software Verification, 2019)
    In this tutorial, we present our recent work on building trusted, resilient and interpretable AI models by combining symbolic methods developed for automated reasoning with connectionist learning methods that use deep neural networks. The increasing adoption of artificial intelligence and machine learning in systems, including safety-critical systems, has created a pressing need for developing scalable techniques that can be used to establish trust over their safe behavior, resilience to adversarial attacks, and interpretability to enable human audits. This tutorial is comprised of three components: review of techniques for verification of neural networks, methods for using geometric invariants to defend against adversarial attacks, and techniques for extracting logical symbolic rules by reverse engineering machine learning models. These techniques form the core of TRINITY: Trusted, Resilient and Interpretable AI framework being developed at SRI. In this tutorial, we identify the key challenges in building the TRINITY framework, and report recent results on each of these three fronts. 
    more » « less
  3. ; ; ; ; (, IEEE)
    The adoption of digital technology in industrial control systems (ICS) enables improved control over operation, ease of system diagnostics and reduction in cost of maintenance of cyber physical systems (CPS). However, digital systems expose CPS to cyber-attacks. The problem is grave since these cyber-attacks can lead to cascading failures affecting safety in CPS. Unfortunately, the relationship between safety events and cyber-attacks in ICS is ill-understood and how cyber-attacks can lead to cascading failures affecting safety. Consequently, CPS operators are ill-prepared to handle cyber-attacks on their systems. In this work, we envision adopting Explainable AI to assist CPS oper-ators in analyzing how a cyber-attack can trigger safety events in CPS and then interactively determining potential approaches to mitigate those threats. We outline the design of a formal framework, which is based on the notion of transition systems, and the associated toolsets for this purpose. The transition system is represented as an AI Planning problem and adopts the causal formalism of human reasoning to asssit CPS operators in their analyses. We discuss some of the research challenges that need to be addressed to bring this vision to fruition. 
    more » « less
  4. ; ; ; ; ; ; ; ; ; ; et al (, IEEE Symposium on Security and Privacy (SP))
    Safety violations in programmable logic controllers (PLCs), caused either by faults or attacks, have recently garnered significant attention. However, prior efforts at PLC code vetting suffer from many drawbacks. Static analyses and verification cause significant false positives and cannot reveal specific runtime contexts. Dynamic analyses and symbolic execution, on the other hand, fail due to their inability to handle real-world PLC programs that are event-driven and timing sensitive. In this paper, we propose VetPLC, a temporal context-aware, program analysis-based approach to produce timed event sequences that can be used for automatic safety vetting. To this end, we (a) perform static program analysis to create timed event causality graphs in order to understand causal relations among events in PLC code and (b) mine temporal invariants from data traces collected in Industrial Control System (ICS) testbeds to quantitatively gauge temporal dependencies that are constrained by machine operations. Our VetPLC prototype has been implemented in 15K lines of code. We evaluate it on 10 real-world scenarios from two different ICS settings. Our experiments show that VetPLC outperforms state-of-the-art techniques and can generate event sequences that can be used to automatically detect hidden safety violations. 
    more » « less
  5. ; ; ; ; (, IEEE)
    Operation efficiency in cyber physical system (CPS) has been significantly improved by digitalization of industrial control systems (ICS). However, digitalization exposes ICS to cyber attacks. Of particular concern are cyber attacks that trigger ICS failure. To determine how cyber attacks can trigger failures and thereby improve the resiliency posture of CPS, this study presents the Resiliency Graph (RG) framework that integrates Attack Graphs (AG) and Fault Trees (FT). RG uses AI planning to establish associations between vulnerabilities and system failures thereby enabling operators to evaluate and manage system resiliency. Our deterministic approach represents both system failures and cyber attacks as a structured set of prerequisites and outcomes using a novel AI planning language. AI planning is then used to chain together the causes and the consequences. Empirical evaluations on various ICS network configurations validate the framework’s effectiveness in capturing how cyber attacks trigger failures and the framework’s scalability. 
    more » « less
  • Citation Formats
  • MLA
  • APA
  • Chicago
  • BibTeX
  • Save / Share this Record
  • Send to Email