Hi Michael, > Does this output-verification also apply to CAmkES C code for components and > interfaces?
In principle it would, but currently that verification is not being performed, because our binary tool chain works best if there is also a proof stack on top of the C code. > 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? Using CompCert would indeed make sense in this setting. > 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. I’ll leave these to one of our systems people to answer.. Cheers, Gerwin _______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
