Summary
This wiki provides an overview of the VERDICT tool and highlights from an illustrative example use case. For a more detailed report please contact the developers.
Bugs in deployed systems are hard to eliminate. Therefore, considering resiliency during the design phase of the system development can save future costs associated with debugging. Also, accounting for resiliency at the design level can help in designing stable systems. Specifically, by analyzing the system design for cyber resiliency, one can develop reliable system architectures, where the system has the ability to degrade gracefully even when exposed to cyber-attacks.
System Design V model includes the various phases of system development lifecycle. The VERDICT project focuses on the initial design phases of the System Design V model.
The system designer is an integral part of the system design process. Our goal is to enhance the capabilities of the system designer. Specifically, the VERDICT tool can aid the system designer in making efficient and informed design choices, by accounting for resiliency while achieving essential system goals and capabilities. The VERDICT tool has two capabilities namely 1. Model-based Architecture Analysis and Synthesis (MBAAS) and 2. Cyber-Resiliency Verifier (CRV).
The MBAAS capability of the VERDICT tool helps the designer to analyze the system architecture by focusing on the safety and cyber properties of the system, its subcomponents and connections. The CRV capability of the VERDICT tool helps the designer to analyze the system architecture by focusing on the safety properties, cyber properties and behavioral properties of the system, its subcomponents and connections.
The figure below highlights the capabilities that we have now that did not exist when the program began.
Figure below shows an overview of the VERDICT program along with a figure that highlights the intended interactions of the various teams performing research in each of the technical areas (TAs). The toolchain is designed to enable System Engineers to analyze security along with other desired properties (e.g., safety, performance, cost, weight) at design time.
The program has seven Technical Areas (TA). TA 6 are the System Providers. They provide the systems to analyze including requirements, models, and code. TA 5 are the Systems Integrators. They facilitate integration of all the tools into a toolchain. TA 4 is focused on Explainable Formal Methods. They are developing technology and tools that enables system engineers to benefit from formal methods technology without being formal methods experts. TA 3 supports Legacy Components such as binary and source code. TA 3 is working on tools that will extract models and properties from legacy code, so that it may be understood more clearly and reused. TA 2 is Design for Resiliency. The TA 2 performers are developing design tools to model, analyze and verify improvements in cyber-resiliency properties. The TA 1 performers are generating cyber-resiliency properties from the content provided to them by the TA 6 system providers. The GE team is working on TA 2, Design for Resiliency. Table below shows the CASE program Technical Areas and describes our interaction expectations as a TA2 performer.
| Technical Area | Our expectation |
|---|---|
| TA1: Design Cyber-resiliency requirements | Based on the inputs from TA6, provides a list of component-level functional requirements, mission-level requirements, and other cyber-resiliency properties in some formal language |
| TA3: Support Legacy Components | Based on the component source code/binary provided by TA6, develops an abstract model of the binary |
| TA4: Explainable Formal Methods | Provides improvements of underlying reasoning engines and design of an intermediate language that is general enough so that TA1, TA2, TA3, and TA4 tools can communicate effectively. |
| TA5: Engineering Workflow Integration | Provides integration between different tools and writes translators when necessary to facilitate integration. |
| TA6: Platform Provider | Provides architectural and behavioral models, functional requirements, mission-level requirements, source code/binary for legacy components |
The GE VERDICT tool has two major functions. The first is the Model Based Architecture Analysis and Synthesis (MBAAS). The MBAAS tool, takes in architecture models, mission, cyber-resiliency and safety requirements, then generates attack-defense trees with resiliency metrics and fault trees with reliability metrics. The MBAAS tool uses the attack-defense tree information along with cyber-security requirements and constraints as inputs to a synthesis function that generates an architecture that meets predefined resiliency design constraints. The MBAAS tool is built as an extension to a Fault Tree modeling and synthesis tool named SOTERIA that was developed previously for NASA. The MBAAS tool enables the system engineer to model components, then synthesize architectures that meet both safety (based on fault tree analysis) and security (based on attack-defense tree analysis) design goals.
The second tool in the GE TA 2 Design for Resiliency project is the Cyber-Resiliency Verifier (CRV). The CRV takes in cyber-resiliency properties/requirements, architecture, and behavioral models - performs a formal analysis using an improved version of the Kind2 model checker developed at the University of Iowa, then returns design proof evidence, localized design errors, suggested run time monitors, blame and merit assignment.