Next Article in Journal
The Architecture Design of Electrical Vehicle Infrastructure Using Viable System Model Approach
Previous Article in Journal
A Systems Approach to Examining PhD Students’ Well-Being: An Australian Case
Previous Article in Special Issue
Will There Be Enough Water? A System Dynamics Model to Investigate the Effective Use of Limited Resources for Emergency Water Supply
Article

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

1
GE Research, 1 Research Cir, Niskayuna, NY 12309, USA
2
Department of Computer Science, The University of Iowa, Iowa City, IA 52242, USA
3
GE Aviation, 3290 Patterson Ave SE, Grand Rapids, MI 49512, USA
*
Author to whom correspondence should be addressed.
This manuscript is an extension version of the conference paper: K. Siu et al. “Architectural and Behavioral Analysis for Cyber Security.” 2019 IEEE/AIAA 38th Digital Avionics Systems Conference (DASC), San Diego, CA, USA, 2019.
Received: 6 January 2021 / Revised: 12 February 2021 / Accepted: 20 February 2021 / Published: 3 March 2021
(This article belongs to the Special Issue Engineering Resilient Systems)
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. View Full-Text
Keywords: cyber resilient systems engineering; model-based architectural analysis and synthesis; assurance case generation; cyber resiliency verification; formal analysis cyber resilient systems engineering; model-based architectural analysis and synthesis; assurance case generation; cyber resiliency verification; formal analysis
Show Figures

Figure 1

MDPI and ACS Style

Meng, B.; Larraz, D.; Siu, K.; Moitra, A.; Interrante, J.; Smith, W.; Paul, S.; Prince, D.; Herencia-Zapana, H.; Arif, M.F.; Yahyazadeh, M.; Tekken Valapil, V.; Durling, M.; Tinelli, C.; Chowdhury, O. VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System. Systems 2021, 9, 18. https://0-doi-org.brum.beds.ac.uk/10.3390/systems9010018

AMA Style

Meng B, Larraz D, Siu K, Moitra A, Interrante J, Smith W, Paul S, Prince D, Herencia-Zapana H, Arif MF, Yahyazadeh M, Tekken Valapil V, Durling M, Tinelli C, Chowdhury O. VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System. Systems. 2021; 9(1):18. https://0-doi-org.brum.beds.ac.uk/10.3390/systems9010018

Chicago/Turabian Style

Meng, Baoluo, Daniel Larraz, Kit Siu, Abha Moitra, John Interrante, William Smith, Saswata Paul, Daniel Prince, Heber Herencia-Zapana, M. F. Arif, Moosa Yahyazadeh, Vidhya Tekken Valapil, Michael Durling, Cesare Tinelli, and Omar Chowdhury. 2021. "VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System" Systems 9, no. 1: 18. https://0-doi-org.brum.beds.ac.uk/10.3390/systems9010018

Find Other Styles
Note that from the first issue of 2016, MDPI journals use article numbers instead of page numbers. See further details here.

Article Access Map by Country/Region

1
Back to TopTop