I have been reading the following paper for some time:
Klein, Gerwin, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal
Kolanski, and Gernot Heiser. “Comprehensive Formal Verification of an OS Microkernel.”
Trustworthy Sytems, 2014.
https://ts.data61.csiro.au/publications/nictaabstracts/Klein_AEMSKH_14.abst…
This is fantastic work and provides powerful guarantees about kernel behavior. However, I
am confused about the guarantees about the behavior of user programs.
The paper seems to suggest that in the abstract model of sel4, the user transitions are
nondeterministic.
That is correct, the behaviour of the user is modelled as demonic nondeterminism to make
minimal (or no) assumptions about what users might do.
page 21 bottom: "User transitions are specified as nondeterministically changing
arbitrary user-accessible parts of the state space"
Does this mean that the refinement theorem of sel4 (Theorem 3 in the above paper: the C
implementation refines the abstract model) provides no guarantee about what the user
program does, except that the user program does not mess up with the kernel state?
Correct. This means the kernel refinement theorem applies to all possible user programs
(known and unknown).
Is it fair to say that the refinement theorem does not preclude the sel4 implementation
from incorrectly changing the behavior of the user programs, e.g. by messing up the user
state?
No, that is not correct. The refinement theorem says that the kernel will do precisely
what the kernel specification says, and the specification gives details on what exactly
the kernel will do to user state. It constrains the kernel behaviour, but not the user
behaviour. Since the spec is fairly detailed, the integrity theorem in addition gives a
high-level approximation of what the kernel will do on behalf of a user, based solely on
the authority (capabilities) of that user, i.e. it allows you to constrain the effects of
a user program without knowing the code of that user program.
I was expecting the abstract model in Isabelle to concretely specify how the user programs
behave, perhaps according to x86/arm/riscv semantics extended with syscalls.
If it did that, the theorem would only apply to user programs with known behaviour, i.e.
these would be user theorems, not kernel theorems.
To get the fully detailed behaviour of an entire system (kernel + user), you would need to
provide code + semantics for the parts of the system that you are interested in, for
instance using an ARM ISA model. These concrete user programs then trivially refine the
fully nondeterministic user operations of the kernel theorem, i.e. they plug into the
existing refinement theorem for the kernel (specifically into user_op in the ADT_*
theories), and you would then have a combined description of kernel + user behaviour.
While this is theoretically easy to do, you will have to deal with concurrency or at least
interleaving for user executions, since device (incl timer) interrupts could happen at any
time, upon which the kernel will typically schedule another thread. This means
instantiating the entire system is easy, but reasoning about it is not trivial.
Cheers,
Gerwin