Hi William Thank you for bringing this up! I've heard of this technique and that's why I wanted to explicitly clarify this use case. Intuitively it feels extremely hard to get right -- transactions that can abort on any memory access, yet you want to recover to some clean state. Imagine trying to verify something like this -- it's concurrency on steroids. I.e., I get it, maybe it's possible, especially with some careful programming primitives but it seems very very hard and impractical.
Is there a link to source code? Anton On Wed, Mar 26, 2025 at 12:49:59PM +1000, William ML Leslie wrote: > 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 _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
