ge-high-assurance/VERDICT

Misleading Calculated Likelihood in ImplProperties.txt when DAL=0

kityansiu opened this issue · 0 comments

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?