Verification process in a commercial project

Verification
1

Hello,
I’m having a hard time finding the answer to my question.

In a real life & commercial system that needs to be accredited, how can the seL4 proofs by used by the accreditors? I have problems understanding what’s the output generated from those proofs and how the accreditors can trust that output?

Thanks for your help :slight_smile:

2

Somehow I missed this one, sorry. I was hoping I could point you to a video from the last seL4 summit where someone from an evaluation authority was talking about this topic, but it seems this one was not recorded.

First of all, the answer very much depends on what you mean by “accredited”, i.e. under which scheme and under which criteria. The answer ranges from “no help at all” to “almost everything you need”.

E.g. for Common Criteria EAL4, I don’t think the proofs would help much, because the rules for that don’t mention any proofs and you’d likely have a hard time convincing a certification authority that they should waive other requirements, because those proof exists (even though the proofs are likely to produce much higher assurance for correctness). For EAL 7, formal specifications and proofs are required, so they would directly fulfil some (but not all) of the needs of that certification scheme.

Other schemes like DO-178C in aviation together with DO-333 explicitly mention formal proofs as alternative for some of the testing requirements. In this case specifically, the tools that are used to check the proofs (here the theorem prover Isabelle/HOL) would have to be “qualified”, i.e. itself approved to be used for the purpose. We think that Isabelle/HOL would be possible to qualify for that purpose.

Other schemes again are much more flexible and don’t require a specific certification process, but instead a deep evaluation by experts in the evaluation authority (e.g. institutions like the NSA in the US, or NCSC in the UK). Those experts would want to understand what the seL4 specification mean, which parts of the proof you have to look at to understand what the underlying proof assumptions are, and understand enough about the proof tool to see that the instructions we have for running the proofs prevent us from cheating in the sense that they actually do check the proofs. Such evaluations have been done for seL4 in the past. The actually interesting part of such evaluations (if done well) is understanding which risks still need to be mitigated by other means for the overall security goals of the system to be achieved. We hope that our list of explicit proof assumptions in the FAQ and on the website are useful for that, but we don’t usually get to see the inside of such evaluations for very sensitive systems.

Overall, what you need to understand to figure out if the proofs mean something for a particular system is:

  • are the properties that we have proved useful for what you want to achieve (needs analysis of the system and an understanding of the properties)
  • are the properties you think we have proved the ones we actually have proved (needs understanding of the formal specifications/high-level properties, e.g. in the published research papers and in the proof repository – you need an expert for that, but only once, because these properties don’t change much)
  • are the underlying proof assumptions suitable for your system (e.g. the information flow proof does not prove absence of timing channels – if you need absence of timing channels, do you have other mitigations in place)
  • do the proofs actually check (can you run the proofs with the provided instructions, and can you easily enough scan for absence of cheating – this is one of the easier parts)
1 Like