Generating CAmkES glue-spec and glue-proofs
Hi everyone, 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. One candidate reason could be that we set up our build environment strangely: We currently check out seL4/camkes-manifest and then symlink our component into the 'projects/global-components' subtree of the seL4. This works for generating bootable images, but I haven't found out how to generate the glue spec yet. Why we have set it up this way I don't know, and I suspect that there is a right way TM that we have overlooked/not found in the documentation. I appreciate any help in this regard. Thanks and have a nice day! Cheers, Ben
March 29, 2021 1:51 PM, "Ben Fiedler" <sel4@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! [1]: https://github.com/seL4/camkes-tool/commit/21becfa909595f0ba204b7fafef9e3629...
Hi Ben, Sorry for taking long to reply to this, a lot was going on.
On 31 Mar 2021, at 1:20 am, Ben Fiedler <sel4@bfiedler.ch> wrote:
March 29, 2021 1:51 PM, "Ben Fiedler" <sel4@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. 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
On 22 Apr 2021, at 13:38, Gerwin Klein <kleing@unsw.edu.au<mailto:kleing@unsw.edu.au>> wrote: 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) The one case where the glue code verification adds real value is if the connector is between two verified components, where it guarantees that the connection is functionally equivalent to a function call. As the number of verified components increase, this will become more of an issue. So we would welcome someone redoing those proofs for the standard connectors, it’s just not high enough on our priorities (for now). Gernot
Hi Gerwin, April 22, 2021 5:38 AM, "Gerwin Klein" <kleing@unsw.edu.au> wrote:
On 31 Mar 2021, at 1:20 am, Ben Fiedler <sel4@bfiedler.ch> wrote:
March 29, 2021 1:51 PM, "Ben Fiedler" <sel4@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
On May 3, 2021, at 04:57, Ben Fiedler <sel4@bfiedler.ch> wrote:
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.
In the past, this was something I dealt with using a hack known as the pruner [0]. These days there may be a better option. [0]: https://github.com/seL4/pruner
On 4 May 2021, at 13:11, Matthew Fernandez <matthew.fernandez@gmail.com> wrote:
On May 3, 2021, at 04:57, Ben Fiedler <sel4@bfiedler.ch> wrote:
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.
That's correct, yes, varargs are not in the verification subset for C.
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.
In the past, this was something I dealt with using a hack known as the pruner [0]. These days there may be a better option.
Just to confirm: this is still the way to go, AFAIK. Cheers, Gerwin
participants (4)
-
Ben Fiedler -
Gernot Heiser -
Gerwin Klein -
Matthew Fernandez