ge-high-assurance/VERDICT

Soteria++ fails when 2 controllers present in a file

Opened this issue · 0 comments

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.