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

[baoluomeng]

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

[kityansiu]

@AbhaMoitra, @chrisage, and I looked into this. We used the project Additive_Machine_V3 (AdditiveMachine.aadl, lines 310-336). Specifically, in line 330, here's what happens when changing the DAL level:

• when secureBoot=9, GSN is correctly colored as green
• when secureBoot=7, GSN is correctly colored as red
• when secureBoot=1, GSN is correctly colored as red
• when secureBoot=0, GSN is incorrectly colored as green

We detected that the error is the following:

• When DAL=0, the affected cutset in ImplProperties.txt is different from that in ApplicableDefenseProperties.txt. This difference is correct and is expected.
• In ImplProperties.txt, the Calculated likelihood of successful attack (line 2) is 1e-09 (which is correct according to the implemented cutset). In ApplicableDefenseProperties.txt, the Calculated likelihood of successful attack (line 2) is 1 (which is also correct according to the applicable defense cutset).
• What's misleading is that the implemented, though calculated correctly, leads one to think that the likelihood is acceptable.

The fix should be the following:

• for coloring the GSN, instead of using the Calculated likelihood of successful attack from the ImplProperties.txt file, we should use the number from the ApplicableDefenseProperties.txt file.
• in fact, it looks like that's what's done when coloring the MBAA Result tab when you do Verdict > Run Model Based Architecture Analysis (MBAA)

Actions from meeting on Wed, 4/6/2022

• Chris will look into modifying how GSN is colored based on how the MBAA Result tab is colored
• Kit will write up a new Issue (#228) modifying Calculated likelihood of successful attack (line 2) in *ImpleProperties.txt so it's not misleading. (In short, it's about handling the use case when a defense is listed in the aadl as a property of the component, but then given a DAL=0 which means it's actually not implemented.)

[baoluomeng]

Hi Kit, GSN is looking at and also should read the results in xml files not the txt files as txt files are not machine readable. The txt files i uploaded in this issue are actually xml files. I have to change their suffixes to txt to be able to upload them here.

Also, GSN should look at the ImplProperties.xml file when rendering the colors because that is the result file for the analysis of implemented defenses in the model.

[baoluomeng]

The interesting thing is that I cannot reproduce the issue anymore using the latest versions of the tools on the DeliveryDrone_CASE_v0 model.

Can someone try to reproduce it using the latest OSATE and the latest dev version of VERDICT? @kityansiu @AbhaMoitra @chrisage You can download the latest OSATE from here: https://osate-build.sei.cmu.edu/download/osate/stable/latest/products/ And you can install the latest dev version of VERDICT using this link: https://raw.githubusercontent.com/ge-high-assurance/VERDICT-update-sites/master/verdict-dev

[kityansiu]

@baoluomeng, yes, understood. I was using the txt files to describe the observations, but you're right that the GSN looks at the xml files.

Below is the equivalent observations in xml from the Additive_Machine_V3 project. See "1e-09" on the left in ImplProperties.xml and "1." on the right in ApplicableProperties.xml.

@chrisage, in case it wasn't clear, your modifications should be on the portion of the code that works off the .xml files.

[chrisage]

Can someone try to reproduce it using the latest OSATE and the latest dev version of VERDICT?

I'll need more info on which cyber property DAL was tested in the Delivery_Drone_CASE_v0 test. Below is a comparison of Additive_Machine_v3 run results between stable and latest osate/verdict versions (versions in screenshot). I'm seeing the same results. The GSN graph is all green in both cases but the solution 1 edge is expected to be red.

[baoluomeng]

In *ApplicableDefenseProperties.txt, the Calculated likelihood of successful attack (line 2) is 1 (which is also correct according to the applicable defense cutset).

@kityansiu I am not sure that why there could be cases that the calculated likelihood of successful attack in the "ApplicableDefenseProperties.txt" could be 1 unless there are attacks that have no known defenses, which is not covered by STEM.

[kityansiu]

@baoluomeng, this is because the "Applicable" first lists the cutsets and then uses the DALs to calculate the likelihood. I agree, though, that what's listed in "Applicable" and "Implemented" got intermixed. "Applicable" is reporting the applicable cutset, but then uses the user entered DAL numbers to do the calculation, which can arguably be thought of as "Implemented". This requires more reworking, which I hope can be done with Issue #228.

[AbhaMoitra]

@baoluomeng @chrisage @kityansiu : While I have not downloaded the latest VERDICT version; I did re-run it on DeliveryDrone and I still see the issue and I am not aware of any changes that would alter this behavior. I also noticed additional things that may help; specifically for deliveryItemMechanism, in line 786 if DAL of both properties is set to 0 then VERDICT works correctly. If only one of the DALs is set to 0 then GSN shows incorrect results.

[chrisage]

The accurate MBAS report uses the ApplicableDefenseProperties.xml while the inaccurate (DAL 0 case only) GSN risk fragments are sourced from ImplProperties.xml. In cases ImplProperties DAL 0 properties are "unimplemented" and omitted from the cutset rules rather than valued at risk 0e-1. Populating the GSN from ApplicableDefense will show risk and complete CAPEC cutset rules (even if unimplemented).

[baoluomeng]

Switching the GSN to populate from ApplicableDefense will show risk using complete CAPEC cutsets.

Hi Chris, I think you should not switching the GSN to "ApplicableDefenseProperties.xml" as the names of the files (whether they are ImplProperties or ApplicableDefenseProperties) indicate the content in the files. And GSN uses the ImplProperties file to populate the graphs because the file reflect the actual computation results for the model; whereas the ApplicableDefenseProperties file do not and it just shows you the ideal computation results for the model.

[baoluomeng]

Also, MBAA use both the "Applicable" and "Impl" xml files to display the results because it needs to figure out the missing defense properties in the (implemented) model in case the cyber requirements fail.

[chrisage]

• AD Tree Synthesis (used in calculating risk) drops DAL 0 rules of the cutset (from the tree). Risk is later calculated from the remaining nodes. In cases where only the parent (risk 1 ALeaf) node is left risk is calculated correctly but incorrectly in cases where there are remaining (DLeaf) leaves because removed rule risk is ignored.
• Planning to update the tree synthesis to include DAL 0 DLeaf nodes to be removed only after risk calculation (for readability since rules are considered "unimplemented")

// AD Tree Synthesis implementation of single rule DAL=0 cutsets vs partially implemented cutsets (rules DAL>0)  
[ALeaf (("mainPC", "CAPEC-176"), 1.); ALeaf (("mainPC", "CAPEC-184"), 1.);
    C (ALeaf (("mainPC", "CAPEC-440"), 1.), DSUM [DPRO [DLeaf (("mainPC", "systemAccessControl"), 9)]]);

C (ALeaf (("IO_Module", "CAPEC-176"), 1.),
       DSUM [DPRO [DLeaf (("IO_Module", "remoteAttestation"), 9); DLeaf (("IO_Module", "memoryProtection"), 9)]]);

STEM provides Defense.csv which maps CAPECs to applicable and implemented cutsets. Both excluded and DAL=0 cutset rules are represented with null (with null DALs respectively) in ImplProperties but can be inferred from the applicable rules in soteria++. e.g.

"CompType","CompInst","CAPEC","Confidentiality","Integrity","Availability","ApplicableDefenseProperties","ImplProperties","DAL"
"IO_Module","IO_Module","CAPEC-176",null,"Integrity",null,"RemoteAttestation;MemoryProtection;SecureBoot","remoteAttestation;memoryProtection;null","9;9;null"