Workflow
The VERDICT tool is intended to perform analysis of a system at the architectural level. Consider the scenario where the system designer is designing a delivery drone that automatically delivers packages. When designing such a drone, some of the events that the designer will have to account for are “Loss of package”, “Loss of drone”, “Property damage”, etc. For the sake of simplicity, let us consider that the drone has two specific goals, namely “Deliver the package to the location provided to the drone” and “Not to deliver the package to an off-limits location”.
Based on the typical workflow shown in the figure below, the VERDICT user will capture an architectural model using AADL (a modelling language that allows modelling of software/hardware parts and features of a system) that represents the high-level functional components of the system along with the data flow between them.
The VERDICT Model Based Architecture Analysis and Synthesis (MBAAS) back-end tool will analyze the architecture to identify cyber vulnerabilities and recommend defenses. Specifically, for the MBAAS capability of the VERDICT tool, the designer will have to identify and specify the cyber requirements of the system. The cyber requirements of the system are defined in terms “Confidentiality, Integrity and Availability” of inputs or outputs of the system.
The defenses will typically be recommendations to improve the resiliency of components, such as control access and encrypt communications links, or add components to reduce dependence on a specific source of information. For example, let the blue boxes in the figure below be the sub-components of the system (drone). Let us consider the case where a sub-component identified in the system design, say “Delivery Mechanism”, is a COTS (Commercially Off the Shelf) tool. By running the MBAAS capability of the VERDICT tool the designer will be able to identify that the system cannot achieve its goals because it (essentially its sub-component) is vulnerable to “Supply Chain Attacks”. Specifically, MBAAS will help the designer to identify such vulnerabilities and can further suggest alternate design options. For example, MBAAS will suggest solutions like “Using internally developed tools for delivery mechanism” can help eliminate the vulnerability to “Supply Chain Attacks”.
Once the architectural analysis is complete, VERDICT supports refinement of the architecture model with behavioral modeling information using AGREE. The VERDICT Cyber Resiliency Verifier (CRV) back-end tool performs a formal analysis of the updated model with respect to formal cyber properties to identify vulnerabilities to cyber threat effects. Specifically, CRV performs architectural analysis by focusing on the behavioral information of the system and its sub-components. The behavioral information i.e., details of how the inputs are transformed into outputs can be expressed as “Assume-Guarantee Contracts” in AADL/AGREE. Along with the system architecture (defined in AADL), goals and behavioral information (defined as Assume-Guarantee Contracts in AGREE), information related to threats are fed as inputs to CRV. CRV analyzes and reports if the goals/properties are satisfiable even in the presence of threats. If the goals/requirements are satisfiable, CRV returns Merit Assignment, i.e., set of components that played a vital role in goal satisfaction. If the requirements/goals are unsatisfiable, then CRV returns Blame Assignment, i.e., components that played a vital role in requirement violation.
The CRV capability provides an additional depth of analysis of a model that includes behavioral details of the architectural component models which help to identify design mistakes earlier in the development process. Once the CRV analysis is complete, the developer can create a detailed implementation. MBAAS and CRV work hand in hand to analyze the system design for resiliency. MBAAS analyzes the system design for resiliency using minimal information. Whereas CRV captures behavioral information, therefore it can be used to validate requirements that need such detailed behavioral information for their analysis.