Hi all
I have a couple of questions on how user-level proofs are constructed in
the seL4 ecosystem.
Just to start, can someone point me to an example of a user-level proof,
just so I can take a look at how specifications are exported to user
processes and how everything is stitched together.
But also, I'm a bit confused on what kind of assumptions are needed to
build verified user-level code in the face of revocable memory. I.e.,
it seems that one needs to assume (and trust) that the memory of any
verified (or even rather mission critical) process is never revoked.
Maybe I'm wrong and missing something and you have a way in mind for how
to bypass such trust. Or maybe one can argue that such trust is
reasonable, which is probably true for a "flat" system in which the
mission critical domain is created right from the trusted boot process
or some trusted TCB above it. Yet it seems hard to argue that such trust
is reasonable when the recursion is deeper, e.g., the boot process
launches Linux, and then Linux tries to start some kind of a mission
critical process like a microkernel-protected software TEE or something
(out of its memory hence it can later revoke it). And one wants to build
a proof about this TCB yet such proof needs to deal with memory that can
be revoked at any time or assume that revocation is impossible.
Just wandering what is the take on this. I apologize if this all is
covered somewhere in seL4 docs and I just didn't dig deep enough.
Thank you!
Anton
