...

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.

It just occurred to me what the confusion might be: by conservatively modelling which effects a user program may have with nondeterministic, we implicitly model the hardware mechanisms of the platform at a fairly coarse-grained level. I.e. instead of describing what precisely each user-level instruction in the ARM or x64 instruction set can do, we just say a user execution (no matter how long or short) might change *any* aspect of user-accessible state in any order and in any magnitude, including any register or memory it can access. However, these nondeterministic behaviours do not include any changes to state that is only accessible in kernel mode or to memory that is not mapped by the MMU, which are the hardware mechanisms the kernel relies on to protect its own state.

The proof shows that these are the only mechanisms the kernel needs for that, if the hardware actually enforces them (e.g. Meltdown without mitigation means that the MMU effectively provides more readable mappings than the ISA specification says).

We do have an additional unpublished proof for ARM that the instruction set does not include any instructions that go beyond what these nondeterministic effects model. Since this is precisely how the ISA is designed, this proof is not really kernel correctness, more hardware platform and kernel assumption sanity check.

Cheers, Gerwin

I think the problem you've got here is that you are trying to split your application up into multiple separate processes and this is causing needless complexity.

If you just put the client, server and kernel into one monolithic process, you'll find it a lot easier to prove correctness as this will eliminate the exponential explosion of potential interleavings of your proposed architecture.

Just kidding ;)

I think you would need to extend the seL4 non-deterministic state monad with support for interleaving, extend the seL4 abstract spec with the abstract spec for your two processes and then prove the properties you are interested in over that whole at the abstract level.

As long as you are single threaded and avoid shared memory, you could do the above with OG based on chunks of user space code delineated by system calls with stuttering for the timer interrupt.

You could then independently prove your processes were implemented by their binaries using the existing toolchain and rely on the existing kernel correctness proof for the kernel. You also need to prove your processes refine the non-deterministic processes of the seL4 abstract spec used for the kernel proof which ought to be trivial.

The above will only allow you to prove that the memory contents are correct at specific points during execution. This isn't really good enough for memory-mapped devices which might, for example, require that the correct value is written exactly once within an interval.

If you want to prove properties about I/O to memory mapped devices you will need a memory model which tracks the details of interest (a history of writes to a given location for the above example) and you will need to extend the proof framework to support this memory model. This is similar to the work that would be required to support proofs involving relaxed shared memory concurrency.

You'd want to restrict the use of the complex memory model to just the shared regions of memory and prove separation between those regions and the remainder where you'd want to continue using the simpler memory model.

You can do this by wrapping access to the shared memory and using additional shadow state for the memory model.

If you are interested in proving properties about _interacting_ with a memory mapped I/O device, you will need to model the device and enhance the shared memory access methods to insert OG chunk boundaries so you can show all interleavings of program and device operation are correct. Again, this is similar to what would be required for relaxed memory concurrency but not quite the same because the device model execution needs to be independent of the kernel scheduler.

Proving real-time properties of the interaction with the device would require more work to annotate the OG chunks with WCET information and then keep track of properties of interest in shadow state during interleaving. Interleaving would need to model true concurrency in this case --- some interleavings would be filtered out because they would be inconsistent with potential execution times.

I did a bit of (unpublished) work on the first steps of the above a few years ago before moving on to other things. I'm not up to date with anything that may have been done recently except I know some progress was subsequently made on an operational semantics for C++ concurrency ( https://dl.acm.org/citation.cfm?id=2983997) which might be helpful for the memory model for the concurrency case and might perhaps be useful to model memory mapped I/O as if the device was another thread. On the other hand, real hardware also has features like write combining regions, cached regions with pre-fetch or cached but non cache coherent regions (requiring explicit cache flushes and invalidates) so the C++ model might not be sufficient for memory mapped I/O.

The non-deterministic behaviour of the user process used for the seL4 refinement proof means the refinement holds for any possible user code. This allows you to plug in your specific behaviour into the abstract spec and prove properties at the abstract level without having to re-prove the refinemement of the kernel.

So, the answer to your question "Can the existing sel4 theorems help me prove the above theorem about external traces?" is "yes" because the existing theorems prove the seL4 binary implements the abstract spec for any user space program including yours and this allows you to work with the abstract spec to model interactions with the kernel.

In the case of your example, you have a fair amount of additional work to do, outlined above, to complete an end-to-end proof of your system behaviour.

I'm just an amateur at this. Hopefully Gerwin will follow up with a better answer.

On Fri, 17 Aug 2018, 21:10 Abhishek Anand, abhishek.anand.iitg@gmail.com wrote:

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@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.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.

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/ _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel