April 22, 2021 5:38 AM, "Gerwin Klein" <kleing(a)unsw.edu.au> wrote:
On 31 Mar
2021, at 1:20 am, Ben Fiedler <sel4(a)bfiedler.ch> wrote:
March 29, 2021 1:51 PM, "Ben Fiedler" <sel4(a)bfiedler.ch> 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
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  in camkes-tool
to be a
potential culprit. Even though the camkes.sh script was removed long before, it seems
removed support for the --platform argument and shifted to a more CMake-focused build
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
least according to grep). I think I can hack some CAmkESGen expression together that
cimp-base.thy template, but I'm still not entirely clear where/how the user-provided
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
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
That worked well as a proof of concept, but it was not very fast, mainly because it could
the “Call” system call pattern at the time, because that pattern back then implied Grant
between components, which we wanted to avoid. That has since changed (Grant is no longer
but it meant that the connector was basically unused outside the project it was written
the project, it was no longer maintained and it was eventually removed including its
2) this might sound counter-intuitive, but the glue-code proofs bring fairly low return
investment in terms of assurance vs proof effort. This is because they are about
i.e. code that has systematic errors instead of random errors, because they have to
well-behaved component code (running in the same address space as the glue code), which
satisfied for fairly high-assurance components (i.e. needs at least a proof of
because the theorems you get out are hard to use: you get for free that the glue code
crash and composed with the correct counterpart will correctly encode/decode messages,
it. If you compare that to the architecture (cdl-refine) proofs, they have assumptions
comparatively easy to satisfy and they provide strong assurance about behaviour
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
to dig out the old proofs and write a verified RPC connector that is fast (using the new
rights) in the new CAmkES setup, it’d be a cool thing to do and I might be able to assist
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
I'm trying to feed the CAmkES-generated code to AutoCorres, but it's (seemingly)
in the underlying musllibc code. I suspect that Isabelle's C parser doesn't
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
issues by ifdef'ing the relevant imports, so that all relevant code is
Thanks a lot for your help.