Hi Gerwin, April 22, 2021 5:38 AM, "Gerwin Klein" <[email protected]> wrote:
>> On 31 Mar 2021, at 1:20 am, Ben Fiedler <[email protected]> wrote: >> >> March 29, 2021 1:51 PM, "Ben Fiedler" <[email protected]> wrote: >> >>> I'm having troubles generating the CAmkES glue component specification and >>> proofs from our source. >>> I can and have successfully generated the ADL/CDL spec and implementations >>> using the documented >>> CMake parameters. >>> >>> Grepping around the docs I've found references to a 'camkes.sh' script, but >>> neither the project >>> tree nor the files generated during build contain it. >> >> Digging around reveals commit 21becfa909595f0ba204b7fafef9e3629e8627c7 [1] >> in camkes-tool to be a >> potential culprit. Even though the camkes.sh script was removed long before, >> it seems that this >> commit >> removed support for the --platform argument and shifted to a more >> CMake-focused build (and the >> documentation was not updated - it still mentions the --platform argument). >> >> In the course of this, the cimp-base.thy template was orphaned and is not >> referenced anymore (at >> least according to grep). I think I can hack some CAmkESGen expression >> together that instantiates >> the >> cimp-base.thy template, but I'm still not entirely clear where/how the >> user-provided UserStubs.thy >> theory comes into play, or what to specify in it. Any help is still greatly >> appreciated! > > 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. That makes a lot of sense, thanks for the explanation. > 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. 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. > 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. 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 _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
