MBAAS
The Model Based Architecture Analysis and Synthesis (MBAAS) consists of two functionalies: analysis (MBAA) and synthesis (MBAS).
MBAA takes in architecture models annotated with properties, mission, safety and cyber-resiliency requirements, performs probablistic analysis, and generates fault and attack-defense trees with resiliency metrics. The analysis identifies system vulnerabilities (CAPEC threats) and suggests defenses (NIST Defenses) to mitigate them. The analysis encompasses two major tools: STEM and SOTERIA++, where SOTERIA++ is built as an extension to a Fault Tree modeling and synthesis tool named SOTERIA that was developed previously for NASA.
MBAS is to synthesize a minimal set of defenses with Design Assurance Level (DAL) while minimizing their implementation costs and satisfying all the cyber requirements. There are several operating modes for the synthesis tool based on the input. Synthesis can ignore the existing implemented defenses and yield a globally optimal defense solution, or it can find a locally optimal defense solution where it uses the existing implemented defenses. Synthesis with implemented defenses has two modes depending on whether the existing implemented defenses satisfy all the cyber requirements or not.
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.
Known issues:
- The MBAAS tool expects unique names for components and connections in an AADL project.
The following figure shows a table listing all the CAPEC threats supported by the 1.x version of VERDICT. For more information on CAPEC please refer to https://capec.mitre.org/.
The following figure shows a list of NIST Defenses supported by the 1.x version of VERDICT. For more information on NIST 800-53 Control defenses please refer to https://nvlpubs.nist.gov/nistpubs/SpecialPublications/NIST.SP.800-53r4.pdf.
The following tabls shows the mapping of CAPEC threats to NIST 800-53 mitigation controls and Cyber Defense Properties. The tables are very useful when analyzing the MBAAS feedback in the Failure Path tab.
CAPECs to Mitigations to NIST Controls where CAPECs map to single mitigation.
CAPECs to Mitigations to NIST Controls where CAPECs map to multiple mitigations.
The following figure shows MBAAS user feedback in the VERDICT tool. After the VERDICT MBAAS tool is executed, user feedback is provided in the MBAAS Result console tab. When the Severity of Successful Attack is not satisfied, the user can right click on the red failure icon to view the Failure Paths. This tab shows the Likelihood of successful attack for each of the attacked components, along with the CAPEC Attack Type and Suggested NIST 800-53 Defense. The System and Design Engineers using the VERDICT tool will use this information to help them understand where this system is vulnerable and to suggest options for improving resilience.
The idea of synthesis is to transform attack-defense tree to only defense tree, where each defense node is associated with a user-specified cost. Then the defense tree with costs is further encoded into logical formulas in MaxSMT.
By default defense implementation costs are equal to the design assurance level required. The user can configure how costs are calculated based on the defense definition (component, defense, dal tuple) using the costModel.xml XML file placed at the top-level of the AADL project repository. Costs can be specified with any combination of the defense profile properties (examples shown below). Depending on which defense properties are included the cost function will change. If a DAL is included in the defense cost configuration the cost is treated as an absolute value, otherwise the cost becomes a scaling factor to DAL. When a DAL is configured the absolute value is used as a base cost for all greater DALs (example below). Configured costs must be monotonic meaning any defense profile cost must be equal to or greater than more general defense profiles and all DALs must have costs greater to or equal costs to lower DALs.
- By default (no costs specified), a scaling factor of 1 is used for all <component-property-DAL> triples.
- More specific costs take precedence over less specific defense profile configurations
- If a cost configuration includes DAL in the defense profile the cost is treated as an absolute value, otherwise its used as a scaling factor to DAL. Costs configured by DAL becomes the base absolute value for all greater DALs
- Configured costs must be monotonic meaning all defense profiles must have costs greater than or equal to more general defense profiles, and lower DALs
The below configurations result in the expected target costs for the drone AADL example.
## Given the <cost-model>, get cost for the example defense:
<component="DeliveryDroneSystem.Impl:::camera" defense="antiJamming" dal="5">
## Default mode (a scaling factor of 1 will be used for all \<component-defense-DAL\> triples):
<cost-model></cost-model> -- cost = 1 * 5 (DAL) => 5
## A scaling factor of 2.0 for all <component-defense-DAL> triples
<cost>2.0</cost> -- cost = 2 * 5 (DAL) => 10
## A scaling factor of 3.0 for all defense properties of the actuation subcomponent of DeliveryDroneSystem.Impl. (Note that the triple colon ":::" is used to concatenate the component implementation with the subcomponent instance. Also, the XML field keyword for connections is also component.)
<cost component="DeliveryDroneSystem.Impl:::camera">3.0</cost> -- cost = 3 * 5 (DAL) => 15
## Configurations growing in specificity
<cost>4.0</cost> -- cost = 4 * 5 (DAL) => 20
<cost component="DeliveryDroneSystem.Impl:::camera">5.0</cost> -- cost = 5 * 5 (DAL) => 25
<cost component="DeliveryDroneSystem.Impl:::camera" defense="antiJamming">6.0</cost> -- cost = 5 * 6 (DAL) => 30
<cost component="DeliveryDroneSystem.Impl:::camera" defense="antiJamming" dal="3">40.0</cost> -- cost = 40 (Next highest DAL cost)
## Fallback costs
<cost dal="1">3</cost> -- cost = 3 (Next highest DAL cost)
Configurations must be monotonic meaning costs grow (or remain equal) with greater specificity and greater DALs otherwise an error explains the offending cost configuration pair. Examples below
## Not-Monotonic since the base multiplier is greater than a more specific identifier
<cost>4</cost>
<cost component="DeliveryDroneSystem.Impl:::camera">3</cost>
## Not-Monotonic since the base multiplier * the next lowest DAL is greater than the DAL configured cost e.g. 2 * 3 (DAL-2) > 5
<cost>2</cost>
<cost component="DeliveryDroneSystem.Impl:::camera" dal="5">5</cost>
## Not-Monotonic since more specific DAL configurations have costs less than the more general
<cost component="DeliveryDroneSystem.Impl:::camera" dal="5">5</cost>
<cost component="DeliveryDroneSystem.Impl:::camera" defense="antiJamming" dal="5">4</cost>
Under this mode, synthesis will synthesize a globally optimal defense solution that satisfy all cyber-requirements without considering existing implemented defenses. The solution is globally optimal with respect to the set of NIST-800-53 controls supported by VERDICT. It is a minimal (not necessarily unique) set of entity-defense-DAL triples. The synthesis problem is reduced to MaxSMT to be solved with Z3 solver. A globally optimal defense solution example for the delivery drone example returned by the synthesis is shown below.
Under this mode, synthesis will synthesize a locally optimal solution using existing implemented defenses based on whether the implemented defenses satisfy the cyber requirements or not. In the case that implemented defenses do not satisfy the cyber requirements, synthesis selects a minimal set of component-defense-DAL triples to implement or upgrade in order to satisfy all cyber requirements. An example of such synthesis solution is shown below. This mode considers the already-implemented defenses to be free. The output of the tool still specifies the cost of the already-implemented defenses. The implemented defenses are free for the purposes of minimizing total cost. This solution is minimal among the solutions that can be obtained without removing or downgrading any defenses. Note that there may be already implemented defenses that are unnecessary, which if removed (as recommended by the other mode below) will yield a solution with smaller cost.
Conversely, if the implemented defenses already satisfy the cyber requirements, synthesis performs additional cost reductions, which is to select a maximal set of entity-defense-DAL triples to remove or downgrade while still satisfying the cyber requirements. In essence, we no longer treat the already-implemented defenses as free. This solution is minimal among solutions that can be obtained without implementing or upgrading any defenses. The resulting solution is locally minimal because achieving a more minimal solution, if one exists, requires removing or downgrading some defenses and implementing or upgrading others. An example of such case is shown below.
