Hello — I come at this from the formal-verification-of-C side and I’m still finding my feet with seL4, so a pointer from people who reason about the proof guarantees properly would be very welcome.
I maintain a formally-specified C99 library (Frama-C/WP + ACSL) for safety-critical embedded use. Its proofs are sequential — they assume single-threaded access to a given object — which has me thinking carefully about what happens at a preemption boundary.
I’m trying to understand the established way to reason about this in an seL4 context. If a sequentially-verified component runs inside a partition, with concurrency mediated by the kernel’s IPC/scheduling rather than shared mutable state, is the accepted approach to (a) thread-confine the component per partition and treat cross-partition exchange as the only concurrency, or (b) something more structured I should be reading about? I’m aware of work extending CompCert’s single-threaded proofs toward multi-threaded settings and suspect there’s a cleaner mental model here than I currently have.
Grateful for a pointer to the right paper or the right way to think about it — happy to be told I’m asking it wrong.
I think you’re asking the right question, but I don’t think we have any good answers yet. From my perspective your instinct is correct. If the system is set up to keep memory strictly separate, then IPC and other kernel calls are the only observable effects of concurrency.
There are projects at UNSW ongoing that do user-level verification and also at Kry10. @mbrcknl might be able to say more about the latter. Maybe @gernot can refer someone from UNSW?
This sort of guarantee seems to be exactly what our kernel-userland gap verification project is trying to address: Closing the Kernel-Userland Gap | TS @robs is the expert
Thank you both — this is exactly the direction I was hoping for.
Gernot, the kernel-userland gap project is strikingly on-point. If I’ve understood it, the “intervening irrelevant” entries in your composed Hoare triples are the formal counterpart to the confinement argument I was reaching for informally — establishing that other activity has no effect on the state my sequential reasoning depends on, rather than assuming it. That reframes my (a)-vs-(b) helpfully: confinement is the property, and the composed triples are how you actually prove it.
Gerwin, thank you — reassuring to hear the instinct holds, and that it’s a live problem rather than something I’d simply missed. I’d genuinely welcome a connection to whoever at UNSW or Kry10 is closest to this.
I’ll read the project and the Microkit verification work closely. @robs — I’d be glad to hear how you draw the line between what the kernel establishes and what user-level code is entitled to assume across a blocking call.
Existing practice leans heavily on the assumption that the system has a static configuration of protection domains, with strong isolation between components. The integrity theorem gives a precise account of the conditions that apply, and an upper bound on the effects components can have on each other when those conditions are satisfied.
If your library code is only interacting with a component’s private resources, and the component has only a single thread, then it is quite reasonable to assume a sequential model.
However, If the component has multiple threads, or if it interacts with memory regions writeable by other components (including DMA-capable peripheral devices), then you need a model that can account for the possible interference.
To some extent, you can approximate memory interference by inserting calls to ghost functions whose behaviour is axiomatised to nondeterministically perturb the memory region, possibly subject to a “rely” condition. But this is error prone: you have to be careful to insert such calls everywhere that interference could effect the program you’re verifying. Ultimately, you would want to prove that you’ve inserted all relevant interference points, by refinement to a model that includes all possible interference by construction.
If your code makes seL4 API calls, then you also need a model of what those calls do in your context. There is currently not a good answer for that, but there is work underway to close the gap. Gernot mentioned some work being done is his group. At Kry10, we are independently building our userspace verification on the Iris separation logic framework in Rocq. We aim to support verification of whole-system functional correctness, security and safety, including for dynamic multikernel systems. In our work, the same model accounts for seL4 API behaviour and memory interference, so the logic forces us to account for all the possible interactions. We think this will ultimately give a more comprehensive answer, but there is still a lot of work to get there.
Thank you, Matthew — that’s the precise boundary I was missing. Private resources + single thread makes the sequential model sound; multiple threads, shared-writable memory, or DMA break it. That effectively tells me the envelope my existing proofs are actually valid in, so the honest thing is to treat “confined, single-threaded” as an explicit assumption rather than something I was quietly relying on.
The ghost-function point is well taken — the hard part isn’t inserting the interference calls, it’s proving you’ve caught them all. The Kry10 approach of one model covering both API behaviour and interference, so the logic forces you to account for everything, sounds like the cleaner answer. I’ll read the integrity theorem and follow the Iris/Rocq work.
Hi @Fikoko - as you’ll have seen from the others’ responses, we’ve got various projects in progress whose aim is to demonstrate and establish canonical ways going forward to reason about the composition of programs running on top of seL4. These vary because there are also alternatives in the literature. While @mbrcknl & co. at Kry10 are going with a concurrent separation logic route with Iris in Rocq, inside TS we’re using a Viper-based deductive verification front-end for our Pancake (C-like) systems language for the local properties, and reasoning about their composition using a rely-guarantee framework in Isabelle/HOL. We’ve also used model checking to some extent to prove absence of deadlock for models of the concurrency-heavy queuing protocols.
As a Frama-C user, you’d probably be most interested in what we’re doing with Pancake. The Pancake language helps us a bit here as it distinguishes reads and writes to shared/device memory with instructions that are distinct to the usual memory reads/assignments to exclusively mapped memory. That way our local deductive verification (via transpilation to Viper’s IR) can apply requires and ensures to the shared memory interactions that reflect appropriate relies and guarantees, while not worrying about arbitrary changes happening to the rest of memory reads/writes. That last bit about what memory is mapped locally vs shared is something we can check from the system configuration - in our case, seL4 Microkit system description files.
With shared/device memory taken care of in that way, the rest is - as you say - in what happens on IPC. To the local analysis, this is a Hoare triple assumed to hold over the invocation of seL4_Signal or seL4_Recv. Proving that the seL4 abstract spec actually satisfies these Hoare triples is the scope of the kernel-userland gap project @gernot mentioned. Of course, for a blocking seL4_Recv call this means knowing that all intervening system calls occurring until the eventual unblocking seL4_Signalare irrelevant, which should follow if nobody else is exercising the caps to signal that notification until that moment. For that last part, again who has what caps is determined by the system configuration, giving us a basis to know that anybody who doesn’t hold the cap needed toseL4_Signal scheduled in between could only possibly be doing something irrelevant.
Coming out of that project, we’d like to present a bunch of Hoare triples verified over a local abstraction of the kernel state that is suitable to capture, among other things, what caps are present to the local process. To the Viper-based analysis of Pancake programs running on Microkit, things look promising that we will have such abstracted kernel state available to refer to in a way that’s generated from the system configuration files. However, we’re still working our way towards tying everything together in a nice clean story, so it may be a little while before a publication on it.
Thanks @Rob, that’s really the full picture. The part that clicked for me is the capability angle — that “intervening syscalls are irrelevant” isn’t an assumption but something you get from who holds the cap to signal, checked from the config. That’s much cleaner than the informal confinement argument I started with.
The Pancake shared/local memory distinction is interesting because it’s exactly what I don’t get in Frama-C — in C those accesses look the same, so I don’t have that syntactic hook to scope the relies/guarantees. Something I’ll have to handle differently.
So for a plain sequentially-verified C component, private memory, single thread — it sounds like mine is the local-properties layer, and the IPC/composition story is what your rely-guarantee and the kernel-userland-gap work sits above it. Roughly right?
Looking forward to the publication whenever it lands.