Hi Gerwin,
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
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