Reason about FR when the ancestor PD is formally verified to be correct

[sid-agrawal]

One of the criticisms of the current model is that:

a. FR=1 for two procesess in seL4 with a correct caps setup b. FR=2 for two processes in linux-KVM guests.

But folks would consider (a) to be more secure than (b). We need to somehow in the first case kernel is trusted, and in second case VMM is trusted. And since the kernel is formally verified, the FR path via kernel cannot read to bug exploits.

But what about resource exhaustion in the kernel? Is that a bug?

[sid-agrawal]

Some notes from a brain storming

• What is correctness of the ancestor PD
  • What ways in which it can still affect
  • 1. Ignore
  • 2. Model should show that FR is more than 1.
  • 3. Model aug to show that PD will do the right thing and hence FR=infinite
  • 4. May be RSI can say something
• seL4 case:
  • How would PT caps show in thde mode
  • PD has rights to change some parts of the AS
  • steps
    • assume linerat PT in some physical pahe
    • there is some vortual page which maps to this physical page
• Who is controlling map edge and where it is stored

[sid-agrawal]

• There are two types of seL4 systems 1) RT plays and important role (CellulOS) 2) RT pretty much goes away (MicroKit).
  • In both cases we can look at OSmosis state and say whether it was setup or not.
• In CellulOS, would there be a way to conceptually do away with the RT and still do model extraction?