On Wed, 26 Mar 2025 at 03:54, Anton Burtsev via Devel <devel@sel4.systems> wrote:
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.
I hope this is helpful - some learnings from trying to support mutual suspicion in an EROS descendant that follows a very similar model to seL4. Note that we do not need to handle the case of arbitrary memory being rescinded, only memory that we've been sent by a client. The driver's own memory is owned by the driver, so the only way it can go away without the driver's consent is if the process is destroyed. I don't know if that matters to you. When you set up a driver that maps some client memory that could be revoked out from under it: - the driver should have a handler registered for memory faults. - the memory handler should be able to identify which faults are from regions that were used for mapping client pages. - if a fault happens on a user-supplied page, the handler should either adjust the instruction pointer and stack to a function that can abandon the transaction, or map an empty page in that location and make a note that the driver can check when it is done working with client pages. the driver needs to accept that it might experience a partial read/write of a client's data and decide how to deal with that. Additionally, if we are going to map the page to the driver via the iommu, we pin it, which among other things prevents re-allocation of the page. As far as I know, this isn't necessary in seL4, but maybe there's a similar mechanism to ensure devices can't read re-allocated memory without having to copy. -- William ML Leslie