Working Example
To illustrate VERDICT, an architecture model of a representative delivery drone system was constructed. This model was created in AADL within the OSATE toolchain. The drone system is a part of the delivery operation which consists of a van with packages to be delivered and one or more of these delivery drones. After the van arrives at a location that is close to multiple delivery sites, the delivery drones are initialized with their current position, delivery location, and the package to be delivered is loaded up. After a delivery drone is launched, it uses the inputs from the GPS and IMU to navigate to the delivery location. When the drone reaches the delivery location, it uses its Camera to capture an image of the receiving site to confirm that it is free of obstacles and it is safe for the package to be dropped off. For a high-value package, the Delivery Planner will use the Radio to get confirmation from the operator in the van. If there are no obstacles on the receiving site and confirmation (if needed) is received from the operator, then the Delivery Planner will activate the Delivery Item Mechanism to drop off the package. The Delivery Drone also needs to avoid certain locations and airspace, for example airports, schools and government buildings. The GPS and IMU are subcomponents of GNC to illustrate model hierarchy.
To analyze the system design of the Delivery Drone using VERDICT, the system designer will have to model the system architecture in AADL, specify the properties of the system and its sub-components in VERDICT annex along with the defense properties, and specify safety and cyber requirements at the system and sub-component level.
The system designer creates the architectural model of the delivery drone in AADL modeling language.
The following figure shows Component, Cyber Defense and Design Assurance Level (DAL) properties being applied to the radio AADL model component.
Next, define the Mission, Cyber and Safety Requirements at the system level using the VERDICT annex.
Feedback on each mission, cyber and safety requirement – localized to components is returned.
Right click on a failed requirement to view failure paths.
List of failure paths are displayed.
At this point, the user can manually update the Cyber Defenses in the AADL Model. Once the defenses have been implemented, update the AADL model accordingly and rerun MBAA.
As an alternative to the manual analysis iteration loop, VERDICT also provides an automated Synthesis capability. The Synthesis feature allows the user to select a cost model for each of the defenses, then automatically generate a solution that satisfies all of the resiliency constraints with the minimum cost. The following figure shows the pull down menu used to configure and run VERDICT Synthesis. Select "Use Implemented Defenses" if you want the tool to consider the defenses already captured in the model.
The following figure shows the results from Synthesis. The tool recommends adding tamper protection to 4 components and increasing the memory defense on the radio from design assurance level 5 to 7.
VERDICT provides feedback to the designer in the console, in generated fault and attack-defense trees, and it also generates assurance case fragments. The following figure shows example results from running the "Create GSN Assurance Case Fragments" function. The GSN output is also saved in xml format.
Add behavior for the components in the architectural model of the Delivery Drone system. For example, the component "DeliveryItemMechanism" must be in one of these four possible states: the delivery has not started, it is in progress, it has been completed, or it has failed and this is formalized by defining the enumeration type below,
system DeliveryPlanner
features
-- inputs
bus_in: in data port Data_Types::InputBus.impl;
cur_pos: in data port Data_Types::Position.impl;
delivery_status: in data port Data_Types::DeliveryStatus;
end DeliveryPlanner