Journal article
VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System
Systems (Basel), Vol.9(1), p.18
03/01/2021
DOI: 10.3390/systems9010018
Abstract
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.
Details
- Title: Subtitle
- VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System
- Creators
- Baoluo Meng - GE Global ResearchDaniel Larraz - University of IowaKit Siu - GE Global ResearchAbha Moitra - GE Global ResearchJohn Interrante - GE Global ResearchWilliam Smith - GE Global ResearchSaswata Paul - GE Global ResearchDaniel Prince - GE Aviation, 3290 Patterson Ave SE, Grand Rapids, MI 49512, USAHeber Herencia-Zapana - GE Global ResearchM. Fareed Arif - Univ Iowa, Dept Comp Sci, Iowa City, IA 52242 USAMoosa Yahyazadeh - University of IowaVidhya Tekken Valapil - GE Global ResearchMichael Durling - GE Global ResearchCesare Tinelli - University of IowaOmar Chowdhury - University of Iowa
- Resource Type
- Journal article
- Publication Details
- Systems (Basel), Vol.9(1), p.18
- Publisher
- Mdpi
- DOI
- 10.3390/systems9010018
- ISSN
- 2079-8954
- eISSN
- 2079-8954
- Number of pages
- 37
- Grant note
- N66001-18-C-4006 / Space and Naval Warfare Systems Center, Pacific (SSC Pacific) Defense Advanced Research Projects Agency (DARPA); United States Department of Defense
- Language
- English
- Date published
- 03/01/2021
- Academic Unit
- Computer Science
- Record Identifier
- 9984411105002771
Metrics
3 Record Views