CRV
After the architecture has been revised to be secure, we then consider cyber-resiliency properties of the system design. To achieve this, the CRV component of VERDICT considers the system architecture (defined using AADL) together with a component-level specification of the system behavior formulated the AGREE language.
Capturing the component-level behavior allows CRV to take advantage of automated formal reasoning techniques such as model checking to analyze the satisfaction of formal cyber-resiliency properties while considering an adversarial environment.
The design philosophy of CRV is to decouple the modeling of the system's functionality from the possible security attacks it must withstand when deployed. The user is responsible for providing a system design model, a set of cyber-resiliency behavioral properties to analyze, and values for applicable VERDICT Properties. Then, the user only has to choose one or more appropriate threat models from a predefined list of such models under which to carry out the necessary formal resiliency analysis.
Unlike other approaches that rely on adversarial models capturing only known cyber-threats, CRV groups possible attacks based on their effects on the system and collectively reasons about them considering abstract threat effect models.
The class of cyber-resiliency properties currently supported by CRV consists of system integrity properties that can be formalized as temporal safety guarantees using the AGREE language. Considering integrity properties for a system under design is relevant as their violation can cause the system to take unintended actions which may jeopardize system safety or security.
The following figure shows an example of cyber-resiliency property written in AGREE for a Delivery Drone system:
Like MBAS, CRV also takes into account non-functional properties of the system for its analysis. A comprehensive list of meta-level attributes used in CRV, and a list of threat models used in CRV together with their English and formal descriptions can be found here.
The behavioral analysis depends on a set of configurable options. They can be accessed from the CRV Setting menu under Verdict in OSATE:
The next subsections provides more information on these options.
The user can select threat (effect) models from the menu:
If no threat model is selected, CRV will check the satisfaction of the cyber-resiliency properties for the benign case, that is, without considering any adversarial model. This setting is useful as a sanity check to be sure the system design satisfies the properties in a benign scenario, when no attacks are present. It should be the first check to be performed, before analyzing the model under any adversarial environment. When one or more threat models are selected, CRV will check whether the system satisfies the cyber-resiliency properties when considering the possible effects of the selected threat models.
CRV implements a blame assignment technique to generate an explanation of cyber-resiliency property violations which details which components and links vulnerable to attack.
When the blame assignment analysis is enabled, CRV will try to identify a minimal number of responsible components or links to assist the System Designer in pinpointing the vulnerable parts of the system.
A component-level analysis will minimize the number of compromised components that must be compromised to carry out an successful attack. The analysis is done once CRV finds an execution trace that leads to a property violation. In contrast, a link-level analysis will minimize the number of compromised connections in the system.
The following figure shows CRV user feedback in the VERDICT tool. After the CRV is executed, this feedback is provided in the CRV Result console tab.
The tab shows the verification result for each system-level cyber-resiliency property, along with explanatory information if a property violation has been detected (red failure icon) and blame assignment was enabled. In the last case, the identified attack type is reported together with a minimal set of compromised ports involved in the attack. The user can right click on the red failure icon and select View Counter-example to view an execution trace that leads the system to a state where the property in question is violated, as shown in the following figure:
For each component port, the trace shows the list of values at each step of the execution.
To perform the behavioral analysis on our model, we need to:
-
extend the architectural model with the fair amount of behavioral information for the components, in the form of AGREE assume-guarantee contracts; and,
-
specify system-level properties of interest to be verified by VERDICT given the expressed behaviors.
For each of these two main steps, VERDICT can carry out a thorough behavioral analysis on the given model under the user-selected threat models. in particular, VERDICT's behavioral analysis will answer the following questions:
-
Does this behavioral model satisfy the specified properties under the target threat models?
-
For any property falsified, which threat was it vulnerable to? And which component(s) could be responsible for that vulnerability?
In what follows, we will explain the steps needed for performing behavioral analysis.
In the first step, we need to add behavior for the components in the architectural model of our Delivery Drone system. As you have seen in Section 4.1, an architectural model consists of high-level definition of each component including its interface (i.e., in ports and out ports), cyber relations, error events, and safety relations. Now we specify the intended functionality of that component. Using AGREE contract to specify that the functionality allows us to choose a level of abstraction in the specification that is enough to prove the system-level cyber-resilience property (as opposed to provide a complete and detailed specification). This functional behavior, for each component, simply expresses temporal constraints between the values of out ports and the value or in ports. Sometimes these constraints may need to be expressed also in terms of the internal state of a component. In that case, relevant information on the internal states may be provided in virtual output ports that we refer to as probes.
Now let's revisit the Radio component in our Delivery Drone model. This component has the following in port–out port interface:
-
comm_in: in port representing radio response communication -
radio_in: in port representing a command issued for radio communication to base station -
comm_out: out port representing radio request communication -
radio_out: out port representing radio response data received from the communication -
health_status: out port representing the health status of the radio component
Specifying the relation between out ports and in ports (and/or the internal states) depends on the level of abstraction we want to have for this component which eventually hinges on the properties we want to verify. However, the rule of thumb is to stay at the highest level of abstraction first and then try to verify the properties. If we need to specify more about this component to prove the desired system-level properties we can refine its specification later.
Now, for radio component we know at least the following:
- Two main pieces of information in the radio communication are important to us: (i) communication data is available (ii) data shows the delivery target is confirmed.
- The radio component receives data from the remote communication channel (i.e.,
comm_in) and presents the response data at itsradio_outout port if a command was issued for radio communication - If no command for radio communication (i.e.,
radio_in) is issued, there is no available radio data.
This is a minimal level of information about about the expected behavior of the radio component. To formalize (1), we define a record using the following syntax.
data RadioResponse
end RadioResponse;
data implementation RadioResponse.impl
subcomponents
data_available: data Base_Types::Boolean;
target_confirmed: data Base_Types::Boolean;
end RadioResponse.impl;
To specify point (2) above, we add a guarantee stating that radio_out is the same as comm_in when radio_in is true:
guarantee "Radio receives data from remote communication channel
if there is a request":
radio_in => (radio_out.data_available = comm_in.data_available and
comm_in.target_confirmed = radio_out.target_confirmed);
Similarly, for point (3) we add the following guarantee:
guarantee "Without a request, no radio data is available":
not radio_in => not radio_out.data_available;
The behavioral requirements above are included inside the AGREE annex as follows:
annex agree {**
guarantee "Radio receives data from remote communication channel
if there is a request":
radio_in => (radio_out.data_available = comm_in.data_available and
comm_in.target_confirmed = radio_out.target_confirmed);
guarantee "Without a request, no radio data is available":
not radio_in => not radio_out.data_available;
**};
As can be seen, so far we have only added constraints about the radio_out out port. Any value that satisfies those constraints will be considered valid during the analysis performed by CVR. This also means that since we have not added any constraints about comm_out and health_status, CRV will assume that they can take any value allowed by their type.
There are situations when one needs to add more detail to the specification in order to capture the behavior of a component more precisely. This can be seen in the specification of DeliveryPlanner component here. This the AGREE specification of that component relies on an abstract representation of the component internal states (using mode notion) to specify its functionality.
The next step is to review the list of safety functional requirements for the system that may affect its integrity, and formalize them as formal cyber-resiliency properties in the AGREE language.
For instance, let's consider the following cyber-requirement for DeliveryDroneSystem that talks about the drone operation and the radio communication: A command to release a valuable package is issued only if drone has received confirmation from base.
To formalize this cyber-requirement we have to identify first the components and ports of the system that are relevant for the description of the property. In our example, the Radio is the component that receives the confirmation through the input port comm1, and the DeliveryPlanner is the component that issues the command to release a package by setting the output port delivery_cmd to RELEASE_PACKAGE_CMD. Moreover, to know whether a package is valuable or not, we need to check the item value of the most recent order, which is transmitted through the input port bus1.
Notioce that some event conditions in our property only depends on the value of a port in the current step, for example, when a command to release a package is issued. However, other conditions depends on past values of one or more signals, like the item value of the most recent order, or the fact that a confirmation from base has been received. In the later case we will use temporal operators, like pre or HasHappened, to express conditions about past values. Furthermore, we will introduce local variables to simplify the definition of conditions and values.
For instance, we can declare a local variable called most_recent_order that will act as a register. It will store the most recent value of the field order of the input port bus1 when the drone is in the initialization mode, and it will keep the last registered value otherwise. If no such previous value exists, it will use an arbitrary order value.
eq arbitrary_value: Data_Types::DeliveryOrder.impl = ...
eq most_recent_order: Data_Types::DeliveryOrder.impl =
if init_mode then
bus1.order
else
arbitrary_value -> pre(most_recent_order);
There is one problem with the previous definition. The variable init_mode is a local variable of DeliveryPlanner's contract that is not accessible from the DeliveryDroneSystem interface. For these cases, the interface of DeliveryPlanner and DeliveryDroneSystem can be extended with a probe signal which is not part of the actual architecture of the system, but it will be used only for specification and verification purposes. In order to identity the new port as a probe, the user can set the VERDICT property probe to true for the new port:
probe_init_mode: out data port Base_Types::Boolean
{ VERDICT_Properties::probe => true; };
Here is again the definition of most_recent_order using the new probe port probe_init_mode. For simplicity's shake, the revised definition uses the initial value of bus1.order as the arbitrary value for most_recent_order in case of no initialization:
eq most_recent_order: Data_Types::DeliveryOrder.impl =
if probe_init_mode then
bus1.order
else
bus1.order -> pre(most_recent_order);
Once most_recent_order has been defined, we can express easily that a package is valuable if the item value of the most recent order is greater or equal to a threshold value:
eq valuable_package: bool =
most_recent_order.item_value >=
Agree_Constants.ITEM_VALUE_THRESHOLD;
We said above that a command to release a package is issued if delivery_cmd is set to RELEASE_PACKAGE_CMD. We can capture this condition with the following local definition:
eq release_cmd: bool =
probe_delivery_cmd = Agree_Constants.RELEASE_PACKAGE_CMD;
where probe_delivery_cmd is a probe signal for delivery_cmd.
The last definition we need before we can express our cyber-resiliency property is for the confirmation event. We would say a confirmation from base has been received if at any point in the past a confirmation was requested by setting radio_cmd to true, and an acknowledge was received through input port comm1. The first condition can be defined as follows:
eq confirmation_requested: bool =
Agree_Nodes.HasHappened(radio_cmd);
where the unary temporal operator HasHappened(X) is true at any point if and only if X has been true from the beginning until that point.
The second condition is true when radio data is available and the confirmation is positive:
eq acknowledge_received: bool =
comm1.data_available and
comm1.target_confirmed;
Using the definition for the first and second condition, now we can define target_confirmed as follows:
eq target_confirmed: bool =
Agree_Nodes.HasHappened(
confirmation_requested and
acknowledge_received
);
Finally, we express the definition of the cyber-resiliency property as a guarantee for DeliveryDroneSystem using the previous defined auxiliary variables:
guarantee "P4: A command to release a valuable package is issued only
if drone has received confirmation from base":
release_cmd and valuable_package => target_confirmed;
Once we have specified formally the properties of interest, the first thing we have to check is that our system design model satisfies all the properties in a benign scenario, that is, without considering the effects of any threat model. In order to do that, open the CRV Settings window:
Make sure no Threat Model is selected, and save the settings:
Select DeliveryDrone model on the left pane, and select Run Cyber Resilience Verifier from the Verdict - Cyber Resilience Verifies (CRV) tab on the Verdict menu:
This initiates the translation of the AADL model to an Intermediate Modeling Language (IML) and then to the VERDICT design model and finally the analysis. The user can observe the steps of the progression in the Console pane. The process can take from several minutes.
The result of the analysis confirms that all cyber-resiliency properties, including property P4 described in the previous section, are satisfied in the benign scenario:
If this had not been the case, that is, one or more property violations would have been detected, it would be time to review the system design model because that might be indicative of a faulty behavioral specification.
After checking all cyber-resiliency properties are satisfied in the benign case (see previous section), it is time for analyzing the behavioral model under an adversarial environment. For that, we have to repeat the steps described in the previous section except that now we will select two threat models, Network Injection and Remote Code Injection, that we suspect could lead to the identification of an attack that violates property P4. We will also make sure the Blame Assignment option is selected:
The following figure shows the result of the analysis after running CRV using the new setting:
All properties except P4 are satisfied under the effects of the two selected threat models. Moreover, CRV is able to identify a Network Injection attack by compromising only the data going through port comm1. The user can right click on the red failure icon and select View Counter-example to view an execution trace that leads the system to a state where property P4 is violated as it is shown in the following figure:
Once a vulnerable component or connection is identified, the user can consider multiple possibilities to address the root cause of the attack. Let's assume the user decide in this case to introduce resiliency measures such as cryptographic authentication and encryption for the compromised connection. The user can inform the tool about these measures by changing the corresponding VERDICT property values for the connection:
A new analysis of the system confirm the applied fix is enough to rule out new Network Injection attacks: