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.abstr...
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.
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? 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?
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.
Sorry if I misunderstood the paper. Thanks in advance for any clarification, Abhishek