Hello,
I understand that the proof for seL4 implies that the compiler and linker
do not need to be trusted, because their output can be verified by a tool.
Does this output-verification also apply to CAmkES
C code for components and interfaces?
Specifically, I'm working on a project where we want to have certain
functionality implemented in C to be run on the seL4 microkernel. Would we
gain any proof by using compcert, or is the output-verification sufficient?
And is there any way to execute previously-compiled C binaries in a CAmkES
component?
I tried system calls, but I learned that won't work with the microkernel :-)
I looked into the build architecture of the project, but I couldn't find
where CAmkES components were being compiled.
I looked into replacing gcc with compcert for the system, but there are
used many flags available to gcc that are not available to compcert, so I
scratched that idea.
Thank you for your help.
-Michael
