Re:On the history and justification of the C programming lan...
by nickpsecurity on Thursday August 18, 2016 @08:02PM
(#12317136)
Basically. The good news is CompCert might not be needed. Remember that seL4 bypassed need for CompCert by somehow translating it directly to ASM. I found out they used Myreen et al's method.
Their work is mindblowing. There's almost no TCB left lol. I still want diverse verifiers in diverse logics and machine codes to verify the HOL checkers and such. I don't trust their verify it in itself sort of method. Not entirely. They do have a nice projects page for CakeML listing each improvement that would be useful and skill estimate. More should do that.
Look at NICTA's COGENT, too. It's open-source now with an ext2 implementation partly or mostly done.
https://www.cl.cam.ac.uk/~mom22/stacks.html
Their work is mindblowing. There's almost no TCB left lol. I still want diverse verifiers in diverse logics and machine codes to verify the HOL checkers and such. I don't trust their verify it in itself sort of method. Not entirely. They do have a nice projects page for CakeML listing each improvement that would be useful and skill estimate. More should do that.
Look at NICTA's COGENT, too. It's open-source now with an ext2 implementation partly or mostly done.
https://ts.data61.csiro.au/projects/TS/cogent.pml
Here's the Simpl language I referenced that's I believe at the heart of AutoCorres tool. They embedded C in it but it's not C specific.
https://www.isa-afp.org/entries/Simpl.shtml