Re: [seL4] formal guarantee about preserving user behaviour

Right, I understand your concern now, and the short version is: the model is also parametric in the user operations, the nondeterminism is just the most general instance. In more detail:

On 18.08.2018, at 06:09, Abhishek Anand wrote: 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?

Yes, you can do that, although strictly speaking you’d need a device/trace model for that, which is ongoing work -- the current model is memory-based. That means, what you can do right now is reason that the content of 0x1000 will be present in 0x1001 after the IPC.

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.

If you only apply the theorem with the nondeterministic instance, then you are correct, but fortunately the model is also parametric, i.e. you can instantiate it with specific user code. As soon as you do that, you resolve the non-determinism and can reason about what exactly is going on.

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.

You can provide the behaviour of the user as the parameter “uop” to the function do_user_op, which restricts what the user can see and affect: https://github.com/seL4/l4v/blob/2151a57c51f95d2b5c2a2204dbdcc8dc2d1db473/pr... In the most detailed version, the function uop would be the fetch/decode/execute step function of an ISA model, operating on the registers and memory it can see, but you can also plug in higher-level representations of user executions that abstract from that.

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?

Yes, it should, and it is :-). The non-deterministic instance we mention in the paper is just the most general instance, you can plug in any other instance as well. Since any other instance trivially refines the maximal non-determinism, you don’t need to reprove anything about the kernel for using existing theorems, but you can prove additional things about the behaviour of the system. Cheers, Gerwin