More Like this

1. Reasoning about Trustworthiness in Cyber-Physical Systems Using Ontology-Based Representation and ASP

   Thanh Hai Nguyen, Tran Cao (November 2020, Proceedings of the 23rd International Conference on Principles and Practice on Multi-Agent Systems (PRIMA) 2020)

   null (Ed.)

   This paper presents a framework for reasoning about trustworthiness in cyber-physical systems (CPS) that combines ontology-based reasoning and answer set programming (ASP). It introduces a formal definition of CPS and several problems related to trustworthiness of a CPS such as the problem of identification of the most vulnerable components of the system and of computing a strategy for mitigating an issue. It then shows how a combination of ontology based reasoning and ASP can be used to address the aforementioned problems. The paper concludes with a discussion of the potentials of the proposed methodologies. 

   more » « less
2. Reasoning About Trustworthiness in Cyber-Physical Systems Using Ontology-Based Representation and ASP

   https://doi.org/10.1007/978-3-030-69322-0_4  

   Nguyen, Thanh H; Son, Tran C; Bundas, Matthew; Balduccini, Marcello; Garwood, Kathleen C; Griffor, Edward (November 2020, Principles and Practice of Multi-Agent Systems (PRIMA 2020))

   This paper presents a framework for reasoning about trustworthiness in cyber-physical systems (CPS) that combines ontology-based reasoning and answer set programming (ASP). It introduces a formal definition of CPS and several problems related to trustworthiness of a CPS such as the problem of identification of the most vulnerable components of the system and of computing a strategy for mitigating an issue. It then shows how a combination of ontology based reasoning and ASP can be used to address the aforementioned problems. The paper concludes with a discussion of the potentials of the proposed methodologies. 

   more » « less
3. Resilient Machine Learning for Networked Cyber Physical Systems: A Survey for Machine Learning Security to Securing Machine Learning for CPS

   https://doi.org/10.1109/COMST.2020.3036778  

   Felix Olowononi, Danda B. (September 2020, IEEE Communications surveys and tutorials)

   null (Ed.)

   Cyber Physical Systems (CPS) are characterized by their ability to integrate the physical and information or cyber worlds. Their deployment in critical infrastructure have demonstrated a potential to transform the world. However, harnessing this potential is limited by their critical nature and the far reaching effects of cyber attacks on human, infrastructure and the environment. An attraction for cyber concerns in CPS rises from the process of sending information from sensors to actuators over the wireless communication medium, thereby widening the attack surface. Traditionally, CPS security has been investigated from the perspective of preventing intruders from gaining access to the system using cryptography and other access control techniques. Most research work have therefore focused on the detection of attacks in CPS. However, in a world of increasing adversaries, it is becoming more difficult to totally prevent CPS from adversarial attacks, hence the need to focus on making CPS resilient. Resilient CPS are designed to withstand disruptions and remain functional despite the operation of adversaries. One of the dominant methodologies explored for building resilient CPS is dependent on machine learning (ML) algorithms. However, rising from recent research in adversarial ML, we posit that ML algorithms for securing CPS must themselves be resilient. This article is therefore aimed at comprehensively surveying the interactions between resilient CPS using ML and resilient ML when applied in CPS. The paper concludes with a number of research trends and promising future research directions. Furthermore, with this article, readers can have a thorough understanding of recent advances on ML-based security and securing ML for CPS and countermeasures, as well as research trends in this active research area. 

   more » « less
4. Universal CPS Environment for Federation (UCEF)

   Burns, Martin; Roth, Thomas; Griffor, Edward; Boynton, Paul; Sztipanovits, Janos; Neema, Himanshu (January 2018, 2018 Winter Simulation Innovation Workshop)

   NIST, in collaboration with Vanderbilt University, has assembled an open-source tool set for designing and implementing federated, collaborative and interactive experiments with cyber-physical systems (CPS). These capabilities are used in our research on CPS at scale for Smart Grid, Smart Transportation, IoT and Smart Cities. This tool set, "Universal CPS Environment for Federation (UCEF)," includes a virtual machine (VM) to house the development environment, a graphical experiment designer, a model repository, and an initial set of integrated tools including the ability to compose Java, C++, MATLABTM, OMNeT++, GridLAB-D, and LabVIEWTM based federates into consolidated experiments. The experiments themselves are orchestrated using a "federation manager federate," and progressed using courses of action (COA) experiment descriptions. UCEF utilizes a method of uniformly wrapping federates into a federation. The UCEF VM is an integrated toolset for creating and running these experiments and uses High Level Architecture (HLA) Evolved to facilitate the underlying messaging and experiment orchestration. Our paper introduces the requirements and implementation of the UCEF technology and indicates how we intend to use it in CPS Measurement Science. 

   more » « less
5. Towards Building Verifiable CPS using Lingua Franca

   https://doi.org/10.1145/3609134  

   Lin, Shaokai; Manerkar, Yatin A.; Lohstroh, Marten; Polgreen, Elizabeth; Yu, Sheng-Jung; Jerad, Chadlia; Lee, Edward A.; Seshia, Sanjit A. (October 2023, ACM Transactions on Embedded Computing Systems)

   Formal verification of cyber-physical systems (CPS) is challenging because it has to consider real-time and concurrency aspects that are often absent in ordinary software. Moreover, the software in CPS is often complex and low-level, making it hard to assure that a formal model of the system used for verification is a faithful representation of the actual implementation, which can undermine the value of a verification result. To address this problem, we propose a methodology for building verifiable CPS based on the principle that a formal model of the software can be derivedautomaticallyfrom its implementation. Our approach requires that the system implementation is specified inLingua Franca(LF), a polyglot coordination language tailored for real-time, concurrent CPS, which we made amenable to the specification of safety properties via annotations in the code. The program structure and the deterministic semantics of LF enable automatic construction of formal axiomatic models directly from LF programs. The generated models are automatically checked using Bounded Model Checking (BMC) by the verification engineUclid5using theZ3SMT solver. The proposed technique enables checking a well-defined fragment of Safety Metric Temporal Logic (Safety MTL) formulas. To ensure the completeness of BMC, we present a method to derive an upper bound on the completeness threshold of an axiomatic model based on the semantics of LF. We implement our approach in the LF Verifierand evaluate it using a benchmark suite with 22 programs sampled from real-life applications and benchmarks for Erlang, Lustre, actor-oriented languages, and RTOSes. The LF Verifiercorrectly checks 21 out of 22 programs automatically. 

   more » « less