scholarly journals VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System

Systems ◽  
2021 ◽  
Vol 9 (1) ◽  
pp. 18
Author(s):  
Baoluo Meng ◽  
Daniel Larraz ◽  
Kit Siu ◽  
Abha Moitra ◽  
John Interrante ◽  
...  

The ever-increasing complexity of cyber-physical systems is driving the need for assurance of critical infrastructure and embedded systems. However, traditional methods to secure cyber-physical systems—e.g., using cyber best practices, adapting mechanisms from information technology systems, and penetration testing followed by patching—are becoming ineffective. This paper describes, in detail, Verification Evidence and Resilient Design In anticipation of Cybersecurity Threats (VERDICT), a language and framework to address cyber resiliency. When we use the term resiliency, we mean hardening a system such that it anticipates and withstands attacks. VERDICT analyzes a system in the face of cyber threats and recommends design improvements that can be applied early in the system engineering process. This is done in two steps: (1) Analyzing at the system architectural level, with respect to cyber and safety requirements and (2) by analyzing at the component behavioral level, with respect to a set of cyber-resiliency properties. The framework consists of three parts: (1) Model-Based Architectural Analysis and Synthesis (MBAAS); (2) Assurance Case Fragments Generation (ACFG); and (3) Cyber Resiliency Verifier (CRV). The VERDICT language is an Architecture Analysis and Design Language (AADL) annex for modeling the safety and security aspects of a system’s architecture. MBAAS performs probabilistic analyses, suggests defenses to mitigate attacks, and generates attack-defense trees and fault trees as evidence of resiliency and safety. It can also synthesize optimal defense solutions—with respect to implementation costs. In addition, ACFG assembles MBAAS evidence into goal structuring notation for certification purposes. CRV analyzes behavioral aspects of the system (i.e., the design model)—modeled using the Assume-Guarantee Reasoning Environment (AGREE) annex and checked against cyber resiliency properties using the Kind 2 model checker. When a property is proved or disproved, a minimal set of vital system components responsible for the proof/disproof are identified. CRV also provides rich and localized diagnostics so the user can quickly identify problems and fix the design model. This paper describes the VERDICT language and each part of the framework in detail and includes a case study to demonstrate the effectiveness of VERDICT—in this case, a delivery drone.

Author(s):  
A.A. Chechulin ◽  
V.O. Popova

The article presents an approach to classification that will help to identify specific areas of possible cyberattacks and significantly narrow the range of targets vulnerable to attackers. Criteria are considered that allow one to classify cyber-physical systems (attack targets) that are part of nuclear facilities. It is proposed to enter into the basis of the classification such concepts as an object, an attacking and attacking action. The novelty in this work lies in the development of a classification that can be used most effectively to assess the vulnerabilities of systems of critical infrastructure facilities.


2020 ◽  
Vol 175 ◽  
pp. 05038
Author(s):  
Marina Ganzhur ◽  
Nikita Dyachenko ◽  
Andrey Gazizov ◽  
Arthur Otakulov ◽  
Dmitry Romanov

Cyber-physical systems are actively explored in the global and domestic scientific community. It is expected that cyber-physical systems will minimize human participation in the production process, as well as in many other areas of society. At the same time, the information security aspect of the interaction of elements remains insufficiently studied. The classical approach to ensuring security is aimed at counteracting a clear destructive information impact - when information security breaches have obvious signs. The risk of failure of one object of the system can lead to critical conditions. Safety modeling of managerial structures is reduced to considering the operability of the functions of the intermediate link and the interaction between objects that make decisions on the management and generating teams. By analyzing these transitions in limiting cases, it allows the use of analysis and synthesis approaches based on structural schemes and logical relationships.


2021 ◽  
Vol 4 ◽  
pp. 60-65
Author(s):  
V.O. Popov ◽  
◽  
A.A. Chechulin

In this part of the article, the application of the approach to the classification proposed in the first part is presented. As a result of the application of the proposed classification using the generalized model, it is supposed to determine the attack vector within the framework of the proposed model and draw conclusions on the main areas of cyber-physical systems that are vulnerable to attacks by malefactors.


2021 ◽  
Author(s):  
Andreas Hohenegger ◽  
Gerald Krummeck ◽  
Janie Banos ◽  
Alvaro Ortega ◽  
Michal Hager ◽  
...  

2019 ◽  
pp. 2-9
Author(s):  
Ani Bicaku ◽  
Christoph Schmittner ◽  
Patrick Rottmann ◽  
Markus Tauber ◽  
Jerker Delsing

In Industry 4.0 independent entities should interoperate to allow flexible and customized production. To assure the parties that individual components are secured to inter-operate, we investigate automated standard compliance. The standard compliance is defined based on given sets of security and safety requirements for which measurable indicator points are derived. Those reflect configurations of systems recommended by security, safety or process management relevant standards and guidelines, which help to demonstrate the state of compliance. We propose in this paper an approach to automate such an assessment when components are inter-operating with each other by using a monitoring and standard compliance verification framework. The framework will assure the parties that services or devices within their organizations operate in a secure and standard compliant way, without compromising the underlying infrastructure.


Author(s):  
Srikanth Yadav M. ◽  
Kalpana R.

In the present computing world, network intrusion detection systems are playing a vital part in detecting malicious activities, and enormous attention has been given to deep learning from several years. During the past few years, cyber-physical systems (CPSs) have become ubiquitous in modern critical infrastructure and industrial applications. Safety is therefore a primary concern. Because of the success of deep learning (DL) in several domains, DL-based CPS security applications have been developed in the last few years. However, despite the wide range of efforts to use DL to ensure safety for CPSs. The major challenges in front of the research community are developing an efficient and reliable ID that is capable of handling a large amount of data, in analyzing the changing behavioral patterns of attacks in real-time. The work presented in this manuscript reviews the various deep learning generative methodologies and their performance in detecting anomalies in CPSs. The metrics accuracy, precision, recall, and F1-score are used to measure the performance.


Electronics ◽  
2019 ◽  
Vol 8 (2) ◽  
pp. 212 ◽  
Author(s):  
Xiaomin Wei ◽  
Yunwei Dong ◽  
Pengpeng Sun ◽  
Mingrui Xiao

As safety-critical systems, grid cyber-physical systems (GCPSs) are required to ensure the safety of power-related systems. However, in many cases, GCPSs may be subject to uncertain and nondeterministic environmental hazards, as well as the variable quality of devices. They can cause failures and hazards in the whole system and may jeopardize system safety. Thus, it necessitates safety analysis for system safety assurance. This paper proposes an architecture-level safety analysis approach for GCPSs applying the probabilistic model-checking of stochastic games. GCPSs are modeled using Architecture Analysis and Design Language (AADL). Random errors and failures of a GCPS and nondeterministic environment behaviors are explicitly described with AADL annexes. A GCPS AADL model including the environment can be regarded as a game. To transform AADL models to stochastic multi-player games (SMGs) models, model transformation rules are proposed and the completeness and consistency of rules are proved. Property formulae are formulated for formal verification of GCPS SMG models, so that occurrence probabilities of failed states and hazards can be obtained for system-level safety analysis. Finally, a modified IEEE 9-bus system with grid elements that are power management systems is modeled and analyzed using the proposed approach.


Sign in / Sign up

Export Citation Format

Share Document