Hi Ben, Sorry for taking long to reply to this, a lot was going on. So the story is that yes, the glue-code proofs have been removed, and cimp-base.thy should have been removed as well, but was forgotten. Two main reasons why the glue-code proofs were removed: 1) they were for a specific RPC connector only, which was written specifically to be verifiable. That worked well as a proof of concept, but it was not very fast, mainly because it could not use the “Call” system call pattern at the time, because that pattern back then implied Grant capability between components, which we wanted to avoid. That has since changed (Grant is no longer implied), but it meant that the connector was basically unused outside the project it was written for. After the project, it was no longer maintained and it was eventually removed including its proof generation. 2) this might sound counter-intuitive, but the glue-code proofs bring fairly low return of investment in terms of assurance vs proof effort. This is because they are about generated code, i.e. code that has systematic errors instead of random errors, because they have to assume well-behaved component code (running in the same address space as the glue code), which is only satisfied for fairly high-assurance components (i.e. needs at least a proof of memory-safety), and because the theorems you get out are hard to use: you get for free that the glue code will not crash and composed with the correct counterpart will correctly encode/decode messages, but that’s it. If you compare that to the architecture (cdl-refine) proofs, they have assumptions that are comparatively easy to satisfy and they provide strong assurance about behaviour boundaries for completely untrusted code. So we concentrated on those rather than the glue code. Having said all that, there is nothing wrong with verifying glue code automatically. It’s a good thing to have, we just had limited resources to maintain them. So if you have the desire and time to dig out the old proofs and write a verified RPC connector that is fast (using the new GrantReply rights) in the new CAmkES setup, it’d be a cool thing to do and I might be able to assist at least on the conceptual level. Depending on what the theorems are you want from your system, I suspect your project is better served with the cdl-refine proofs in addition to component-specific proofs, though. Cheers, Gerwin

Hi Gerwin, April 22, 2021 5:38 AM, "Gerwin Klein" <kleing(a)unsw.edu.au> wrote: That makes a lot of sense, thanks for the explanation. Unfortunately I'm not versed well enough in the design of seL4 to be of much use here. I will talk about it with David though. That's the conclusion I came to as well. May I ask how you have done the component-specific proofs? I'm trying to feed the CAmkES-generated code to AutoCorres, but it's (seemingly) unhappy somewhere in the underlying musllibc code. I suspect that Isabelle's C parser doesn't understand variadic function arguments and trips over the va_list definition. Have you experienced this as well, and if so how did you solve it? I peeked at another (non-seL4) project of ours and it dealt with these issues by ifdef'ing the relevant imports, so that all relevant code is self-contained. Thanks a lot for your help. Cheers, Ben

That's correct, yes, varargs are not in the verification subset for C. Just to confirm: this is still the way to go, AFAIK. Cheers, Gerwin