3 ms·
Myreen et al can go from specs to machine code directly with verified translation, which seL4 used IIRC. His special method is to meet in the middle, to analyz
by hga 10y ago
Myreen et al can go from specs to machine code directly with verified translation, which seL4 used IIRC.
His special method is to meet in the middle, to analyze the binary code and "turn it into logic" and then check that against the higher level spec. Or something to that effect.
They tried CompCert but there was evidently too great an impedance mismatch. Good thing, too, since CompCert isn't free for most uses.
- nickpsecurity 10y agoBasically. 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. https://www.cl.cam.ac.uk/~mom22/stacks.html 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 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 https://www.isa-afp.org/entries/Simpl.shtml