18 Aug
2018
18 Aug
'18
6:09 a.m.
Thanks for all the responses. These helped clarify some aspects.
But my core concern persists. Sorry, I did not explain my concern properly.
Let us take consider a concrete example;
Let P1 be a user program (in ARMv8 ISA) that does the following:
1) do syscalls to get enough privileges for the next lines to succeed
2) read from the (virtual) address 0x1000
3) send the data read in the previous step as an IPC to P2.
Let P2 be a user program (in ARMv8 ISA) that does the following:
1) do syscalls to get enough privileges for the next lines to succeed
2) wait to receive IPC from P1
3) write the value received in IPC to the virtual address 0x1001
Suppose we run sel4 with the user programs P1 and P2 after configuring the
initial capabilities in a way that enables them to complete their actions.
Suppose this system (sel4+P1+P2) is running on an ARMv8 CPU.
Suppose the addresses 0x1000 and 0x1001 are (identity-)mapped to physical
addresses 0x1000 and 0x1001, and that these physical addresses refer to
external IO devices (not RAM).
I would like to prove that this system generates the following trace of
external IO actions, for some word V:
[read 0x1000 v; write 0x1001 v]
Can the existing sel4 theorems help me prove the above theorem about
external traces?
It seems the answer is no, because, in the sel4 abstract model, the model
of what the user programs do is too non-deterministic: even programs that
do have well-defined deterministic behavior are allowed to
non-deterministically do anything they have the right to.
Because the user programs interact with the kernel and with each other via
the kernel (e.g. IPC), as shown in the above example, it is not clear to me
how to separately specify the user behavior.
Shouldn't the sel4 abstract model be parametrized by a model of user
programs, which can be fully/partially non-deterministic, instead of
imposing the maximally non-deterministic instantiation?
Thanks,
Abhishek
On Thu, Aug 16, 2018 at 7:06 PM <Gerwin.Klein(a)data61.csiro.au> wrote:
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
--
-- Abhishek
http://www.cs.cornell.edu/~aa755/