ge-high-assurance / verdict

DARPA's Cyber Assured Systems Engineering (CASE) project named Verification Evidence and Resilient Design in Anticipation of Cybersecurity Threats (VERDICT)

VERDICT: Tools for architectural and behavioral analysis of AADL models

DARPA Cyber Assured Systems Engineering (CASE) Program

The goal of the DARPA CASE Program is to develop the necessary design, analysis and verification tools to allow system engineers to design-in cyber resiliency and manage tradeoffs as they do other nonfunctional properties when designing complex embedded computing systems. Cyber resiliency means the system is tolerant to cyberattacks in the same way that safety critical systems are tolerant to random faults—they recover and continue to execute their mission function. Achieving this goal requires research breakthroughs in:

• the elicitation of cyber resiliency requirements before the system is built;

• the design and verification of systems when requirements are not testable (i.e., when they are expressed in shall not statements);

• tools to automatically adapt software to new non-functional requirements; and

• techniques to scale and provide meaningful feedback from analysis tools that reside low in the development tool chain.

VERDICT Workflow

VERDICT is a framework to perform analysis of a system at the architectural level. It consists of two major functionalities: Model Based Architecture Analysis and Synthesis (MBAAS) and Cyber Resiliency Verification (CRV). VERDICT user starts with capturing an architectural model using AADL that represents the high-level functional components of the system along with the data flow between them; and then annotate the model with VERDICT properties, relations and requirements for analysis. The VERDICT MBAA back-end tool will analyze the architecture to identify cyber vulnerabilities and recommend defenses. User may also use the VERDICT MBAS feature to synthesize a minimal set of defenses with respect to their implementation costs. VERDICT also supports refinement of the architecture model with behavioral modeling information using AGREE. The VERDICT 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. This valuable capability provides an additional depth of analysis of a model that includes behavioral details of the architectural component models which will help to catch design mistakes earlier in the development process.

Publications

If you are citing VERDICT project, please use the following BibTex entries:

@Article{systems9010018,
AUTHOR = {Meng, Baoluo and Larraz, Daniel and Siu, Kit and Moitra, Abha and Interrante, John and Smith, William and Paul, Saswata and Prince, Daniel and Herencia-Zapana, Heber and Arif, M. Fareed and Yahyazadeh, Moosa and Tekken Valapil, Vidhya and Durling, Michael and Tinelli, Cesare and Chowdhury, Omar},
TITLE = {VERDICT: A Language and Framework for Engineering Cyber Resilient and Safe System},
JOURNAL = {Systems},
VOLUME = {9},
YEAR = {2021},
NUMBER = {1},
ARTICLE-NUMBER = {18},
URL = {https://www.mdpi.com/2079-8954/9/1/18},
ISSN = {2079-8954},
DOI = {10.3390/systems9010018}
}

@inproceedings{siu2019architectural,
  title={Architectural and behavioral analysis for cyber security},
  author={Siu, Kit and Moitra, Abha and Li, Meng and Durling, Michael and Herencia-Zapana, Heber and Interrante, John and Meng, Baoluo and Tinelli, Cesare and Chowdhury, Omar and Larraz, Daniel and others},
  booktitle={2019 IEEE/AIAA 38th Digital Avionics Systems Conference (DASC)},
  pages={1--10},
  year={2019},
  organization={IEEE}
}

For a complete list of publications related to VERDICT, please refer to the Wiki page .

Distribution Statement A: Approved for Public Release, Distribution Unlimited

Copyright © 2020, General Electric Company, Board of Trustees of the University of Iowa

verdict's Issues

Experiment with new model in VERDICT

Apply the VERDICT tool to the following UAV model and report back results.

https://github.com/loonwerks/case-ta6-experimental-platform-models/tree/master/Phase-2-UAV-Experimental-Platform

The report out should include

• What mission requirements were considered?
• What cyber requirements were considered?
• What CAPEC's were identified?
• What NIST 800-53 defenses were recommended?

Cost Model interface automatically changes Component/Connection in certain situations

Under certain click orders, the value in Component/Connection column reverts to the first Component.

To reproduce, do as follows: Here is the starting view of the cost model interface.

Now click on Implementation value in 2nd row then click on Cost value and change it to some other value (say 16). It changes the Component to "actuation"

Changing the cost value should not alter the Component value.

Defense property on connection c1 also showed up on c11 erroneously

This was seen on the Additive model.

Here's the connection.

			c1: port partDescDataFileUSB -> mainPC.partDescDataFileUSB 
			{
			CASE_Consolidated_Properties::connectionType => untrusted;
			CASE_Consolidated_Properties::encryptedTransmission =>0;
			CASE_Consolidated_Properties::deviceAuthentication =>9; 
			CASE_Consolidated_Properties::sessionAuthenticity =>0;
			};		
			c11: port unusedPort -> mainPC.unusedPort 
			{
			CASE_Consolidated_Properties::connectionType => untrusted;
			CASE_Consolidated_Properties::encryptedTransmission =>0;
			CASE_Consolidated_Properties::deviceAuthentication =>0; 
			CASE_Consolidated_Properties::sessionAuthenticity =>0;
			};

Here's the Result tab.

Cyber Requirement set to None

I was using the VERDICT MBAS tool and I had a Cyber Requirement Severity set to "None". The following file is a capture of the error message from the console.

CyberRequirement set to None Error Message.txt

Packaged release in not installable

Describe the bug
The release version (extern.zip) is not installable on OSATE2 (as new software component), and is not available by default in version 2.11.0.

To Reproduce

Expected behavior
An installable package / extension.

Screenshots

Desktop (please complete the following information):

New VDM to Lustre translator

To do list for William

Below is a list of tasks prioritized from high to low

1. Update VERDICT wiki with cost modeling for synthesis
2. Create a new delivery drone model with a realistic cost model that runs with synthesis
3. Test the robustness of the cost model GUI for synthesis
4. Work on the synthesis paper with Paul
5. On a separate branch, work on the unique id for connections and components, and address the issue with a threat instance can be mitigated by a defense on either a connection or a component.

Public set of Charts

Develop a public set of charts and run them through DISTARS.

VDM Translator XML Marshalling Error: JAXB jakarta/activation/DataSource

Describe the bug
VDM xml binding (aadl_in_vdm.xml) throwing error.

Exception in thread "Thread-10" java.lang.NoClassDefFoundError: jakarta/activation/DataSource
	at org.glassfish.jaxb.runtime.v2.model.impl.RuntimeBuiltinLeafInfoImpl.<clinit>(RuntimeBuiltinLeafInfoImpl.java:463)
	at org.glassfish.jaxb.runtime.v2.model.impl.RuntimeTypeInfoSetImpl.<init>(RuntimeTypeInfoSetImpl.java:31)
	at org.glassfish.jaxb.runtime.v2.model.impl.RuntimeModelBuilder.createTypeInfoSet(RuntimeModelBuilder.java:97)
	at org.glassfish.jaxb.runtime.v2.model.impl.ModelBuilder.<init>(ModelBuilder.java:120)
	at org.glassfish.jaxb.runtime.v2.model.impl.RuntimeModelBuilder.<init>(RuntimeModelBuilder.java:61)
	at org.glassfish.jaxb.runtime.v2.runtime.JAXBContextImpl.getTypeInfoSet(JAXBContextImpl.java:405)
	at org.glassfish.jaxb.runtime.v2.runtime.JAXBContextImpl.<init>(JAXBContextImpl.java:255)
	at org.glassfish.jaxb.runtime.v2.runtime.JAXBContextImpl$JAXBContextBuilder.build(JAXBContextImpl.java:1115)
	at org.glassfish.jaxb.runtime.v2.ContextFactory.createContext(ContextFactory.java:144)
	at org.glassfish.jaxb.runtime.v2.JAXBContextFactory.createContext(JAXBContextFactory.java:44)
	at jakarta.xml.bind.ContextFinder.find(ContextFinder.java:368)
	at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:605)
	at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:546)
	at com.ge.verdict.vdm.VdmTranslator.marshalToXml(VdmTranslator.java:31)
	at com.ge.research.osate.verdict.handlers.MBASHandler.runAadl2Csv(MBASHandler.java:146)
	at com.ge.research.osate.verdict.handlers.MBASHandler$1.run(MBASHandler.java:96)
Caused by: java.lang.ClassNotFoundException: jakarta.activation.DataSource cannot be found by com.ge.research.osate.verdict_1.0.0.202206211419
	at org.eclipse.osgi.internal.loader.BundleLoader.findClass(BundleLoader.java:519)
	at org.eclipse.osgi.internal.loader.ModuleClassLoader.loadClass(ModuleClassLoader.java:171)
	at java.base/java.lang.ClassLoader.loadClass(Unknown Source)
	... 16 more

To Reproduce
Steps to reproduce the behavior:

1. Open OSATE
2. Update VERDICT drivers to the latest version (1.7.1) (Help -> Check for Updates)
3. Run the MBAA analysis

Expected behavior
MBAA is expected to run normally

Screenshots
N/A

Desktop (please complete the following information):

• OS: OSX
• Version 1.7.1

Additional context
Possibly a missing dependency to support new functionality:
114433e#diff-8a7ec1031ed404eee878a5afc15c7db34618a6daa129fb5ded3da7d9e1bb31a1R146

New VDM to CSV translator

Implement a new translator from VDM to CSV

• Refer to the current AADL to CSV translator

Cutset likelihood switches between scientific and decimal notation

Cutset likelihood is represented in scientific notation for likelihoods < 1e-5 but as decimals otherwise. The notation effects MBAS output which maps likelihood levels to severity levels where doubles are not expected and default to passing "E" severity.
To reproduce: set a defense DAL to 4 on an otherwise passing aadl configuration, run MBAS and verify results are still passing. Generate the GSN security fragments on the same AADL to visualize the likelihood formatting differences between cutset likelihoods

[Installation issue] requires 'osgi.bundle; org.eclipse.emf.mwe2.launch 0.0.0' but it could not be found

Followed the installation steps till Step 6.

6. Paste the following URL in the Work With: field and press the Enter key. Select the VERDICT for OSATE item and then clicking Next
   https://raw.githubusercontent.com/ge-high-assurance/VERDICT-update-sites/master/verdict-latest

---

In the details window:

Cannot complete the install because one or more required items could not be found.
Software being installed: DARPA CASE VERDICT Feature 1.0.0.202009042137 (com.ge.research.osate.verdict.feature.feature.group 1.0.0.202009042137)
Missing requirement: com.ge.research.osate.verdict.dsl 1.0.0.202009042137 (com.ge.research.osate.verdict.dsl 1.0.0.202009042137) requires 'osgi.bundle; org.eclipse.emf.mwe2.launch 0.0.0' but it could not be found
Cannot satisfy dependency:
From: com.ge.research.osate.verdict 1.0.0.202009042137 (com.ge.research.osate.verdict 1.0.0.202009042137)
To: osgi.bundle; com.ge.research.osate.verdict.dsl 0.0.0
Cannot satisfy dependency:
From: DARPA CASE VERDICT Feature 1.0.0.202009042137 (com.ge.research.osate.verdict.feature.feature.group 1.0.0.202009042137)
To: org.eclipse.equinox.p2.iu; com.ge.research.osate.verdict [1.0.0.202009042137,1.0.0.202009042137]

distinguish when CAPEC-137 is mitigated by a defense property on a connection from defense property on a component

Need to change SOTERIA++ so that if CAPEC-137 is mitigated via Logging or InputValidation properties on the component, it has to be distinguished from mitigation via DeviceAuthentication on a connection. Right now, a "Connection" instance is generated if "Connection" exists in Defenses.csv. Needs to be more specific, like looking at ImplementedDefenses of Defenses.csv.

Start by correcting the following in translator.ml:

(* instantiate "Connection" as components the ones that appear in Defenses.csv  *)
let instancesConn l_defense = 
   let f x tag = List.Assoc.find_exn x tag ~equal:(=) in
   let l_defense_Connection = compInfo "Connection" compType_D l_defense in
   List.dedup_and_sort ~compare:compare (List.map l_defense_Connection ~f:(fun x-> makeInstance ~i:(f x compInst_D) ~c:"Connection" ()));;

New VDM to Lustre translator

Reimplement the VDM2Lus translator

• Do not use the proprietary tool

Implemented defenses should show "and" instead of "or"

In DeliveryDrone.aadl:

			actuation: system Actuation
			{
				-- VERDICT Component Properties
				CASE_Consolidated_Properties::componentType => Hardware;
				CASE_Consolidated_Properties::hasSensitiveInfo => true;
				CASE_Consolidated_Properties::insideTrustedBoundary => true;
				CASE_Consolidated_Properties::pedigree => InternallyDeveloped;

				
				-- VERDICT Cyber Defense and DAL Mitigations
				CASE_Consolidated_Properties::physicalAccessControl => 7;
				CASE_Consolidated_Properties::supplyChainSecurity => 7;
				CASE_Consolidated_Properties::systemAccessControl => 7;
			};

MBAA Result (Security Failure Paths tab) shows the following in the Implemented Defenses column:

But it should really be: actuation:physicalAccessControl and systemAccessControl.

It's currently displaying "or" because it is reading the following from Defenses.csv:

Have to modify Defenses.csv, or think of some other way to read that both defenses are listed under actuation in the aadl file.

Misleading Calculated Likelihood in ImplProperties.txt when DAL=0

Describe the bug
When a defense is listed in the aadl as a property of the component (implying that it is implemented), but then given a DAL=0 (which means it's actually not implemented), the calculated likelihood of successful attack in *ImpleProperties.txt (line 2) is correct but is misleading.

To Reproduce

1. Use the project Additive_Machine_V3. Go to Verdict > Assurance Case Settings. Enter MReq01 as the Requirement Id in the text box.
2. Open the file AdditiveMachine.aadl. Go to line 330
3. Set secureBoot=9. Run Verdict > Create GSN Assurance Case Fragments. Observe that the GSN is correctly colored as green.
4. Set secureBoot=7. Run Verdict > Create GSN Assurance Case Fragments. Observe that the GSN is correctly colored as red.
5. Set secureBoot=1. Run Verdict > Create GSN Assurance Case Fragments. Observe that the GSN is correctly colored as red.
6. Set secureBoot=0. Run Verdict > Create GSN Assurance Case Fragments. Observe that the GSN is incorrectly colored as green.
7. Right click on the circle "SOLUTION_1". This will bring up the file Additive_Machine_V3-CyberReq01-ImplProperties.txt. Observe that the Calculated likelihood of successful attack (line 2) is 1e-09.

Expected behavior
We expect the calculated likelihood to be 1. The number in Additive_Machine_V3-CyberReq01-ApplicableProperties.txt, line 2, shows the number we want. But how can we say that the implemented likelihood is 1, when indeed it is doing the right calculation for the cutset which doesn't have secureBoot?

Bus support in VERDICT

Clarify Cyber Relation for boundary case

Add clear description of how to deal with Cyber Relation definitions for boundary cases.

New VDM to CSV translator

Implement a new translator from VDM to CSV

• Refer to the current AADL to CSV translator

The results portion swapped for the XML and txt files generated by Soteria++

Soteria++ generates two kinds of XML files: ApplicableDefenseProperties.xml and ImplProperties.xml for security analysis. The GSN functionality uses information from ImplProperties.xml to create GSN graphs.

@AbhaMoitra reported that for DeliveryDrone_CASE_v0 example there is a situation where if you set supplyChainSecurity of deliveryItemMechanism to 0 and invoke "Create GSN assurance case fragments", all the branches of GSN graph are green, which is not right.

It turns out that the result portion of the two files somehow were swapped, which causes the GSN functionality to generate all green GSN graphs. Also the content of the txt evidence file is swapped.

Please also check xml and txt files generated by the safety analysis.

Below are two sample xml files (have to change the xml suffix to txt in order to upload it here) for my DeliveryDrone_CASE_v0 example.
ApplicableDefenseProperties.txt
ImplProperties.txt

Discrete cost values at DALs to enable non-linear cost DAL relationships

Currently cost represents a scaling factor to DAL where cost = DAL * cost multiplier. Enabling discrete costs at different DALs would better support scenarios where cost is non-linear with DAL.

Currently costs are configured in the costModel.xml by any combination of:

<cost component="TrainCommunicationSystem.Impl">3</cost>
<cost component="TrainCommunicationSystem.Impl:::antenna">3</cost>
<cost component="TrainCommunicationSystem.Impl:::antenna" defense="antiJamming">3</cost>
where a cost at DAL 5 for a TrainCommunicationSystem.Impl component is expected to be (3*5) = 15

Adding support for discrete cost factors might look something like:

<cost component="TrainCommunicationSystem.Impl:::antenna" defense="antiJamming" dal="0">3</cost>
<cost component="TrainCommunicationSystem.Impl:::antenna" defense="antiJamming" dal="1">4</cost>
<cost component="TrainCommunicationSystem.Impl:::antenna" defense="antiJamming" dal="2">7</cost>
<cost component="TrainCommunicationSystem.Impl:::antenna" defense="antiJamming" dal="...n">...x</cost>
<cost component="TrainCommunicationSystem.Impl:::antenna" defense="antiJamming" dal="9">9</cost>
where the antiJamming component at DAL 2 is mapped to 7

Move some properties from component to connection

The properties to be moved are antiJamming, inputValidation and logging. Currently these properties are on a component but they should be on a connection. The reason for this move is that these actions are specific to a connection.

Soteria++ fails when 2 controllers present in a file

Encountered what appears to be a Soteria++ bug while putting together a model that uses the concept of "library of components".

Specifically, look at the model https://redshare.ge.com/repositories/43b349c7-892d-4480-8e19-380c6fb8a92b/folder/5d6e4243-a46f-4d03-9c63-24c14c0c880d?preview=bbb0afad-c654-45b7-bdb5-3c39a95df9b3 . This has 2 files:

• LibController.aadl defines 2 controllers. The only difference between them is that secureBoot DAL is 3 in Controller1 and is 9 in Controller2.
• In NetworkArch.aadl; line 251-252 can be toggled to say which controller is being used

I did the following 4 runs

1. Using Controller1 in NetworkArch.aadl (using line 251 and commenting line 252). In LibController.aadl commented out Controller2 (lines 66-122). MBAA ran fine, CyberReq1 fails, CyberReq2 passes. These results are what we expect.
2. Using Controller2 in NetworkArch.aadl (using line 252 and commenting line 251). In LibController.aadl commented out Controller1 (lines 6-62). MBAA ran fine, both CyberReq1 and CyberReq2 pass. These results are what we expect.
3. Like Run 1 except kept both controllers in LibController.aadl. MBAA fails on Soteria++. The STEM output seems correct.
4. Like Run 2 except kept both controllers in LibController.aadl. MBAA fails on Soteria++. The STEM output seems correct.

So, basically VERDICT runs fine when there is a single controller in LibController.aadl but not when both are present. I think the underlying issues may be name clash in Soteria++? But I have not really looked into it.

I do have a workaround for this issue in the model https://redshare.ge.com/repositories/43b349c7-892d-4480-8e19-380c6fb8a92b/folder/5d6e4243-a46f-4d03-9c63-24c14c0c880d?preview=a0759a8b-616a-4117-aa8c-5d2bf588e8ed

@kityansiu : If needed, I can run the model and walk you through it. @baoluomeng has already verified that this is an issue.

Defense Feedback

There is a need to clarify the NIST 800-53 calculation and feedback.

The Cyber Defense Properties may be set as integers from 0 to 9. Currently the recommended practice is to use 0 for no defense, 3 for a defense to a minor consequence threat, 5 for a defense to a major consequence threat, 7 for a defense to a hazardous consequence threat and 9 for a defense to a catastrophic consequence threat. The NIST 800-53 standard calls out low, medium and high defense levels.

There is a need to align the NIST low, moderate and high defense control levels with the consequence of threat levels and the cyber defense metrics.

One option is to limit cyber defense property values to 0, 3, 5, 7, 9, then align NIST as 0 - none, 3 - low, 5 - moderate, and 7 and 9 to high.