4 ms·
Did NICTA or Data61 do the work w/ x86 that they did with ARM (the Cambridge model stuff) to be able to assert equivalence between the C code and the resulting
by im_down_w_otp 8y ago
Did NICTA or Data61 do the work w/ x86 that they did with ARM (the Cambridge model stuff) to be able to assert equivalence between the C code and the resulting asm?
If not, then it wouldn't surprise me that there's a conformance problem between the Isabelle, the Haskell, the C, and the asm.
- ratmice 8y agoI don't believe that they did, at least last I read x86 was not a verification target. http://sel4.systems/pipermail/devel/2017-June/001477.html http://sel4.systems/pipermail/devel/2017-June/001477.html
- im_down_w_otp 8y agoYeah I didn't think so. We only use x86_64 for convenience during active hacking on our workstations, then we simulate ARM for local testing and intermediate CI, and do release candidate CI & deployments to ARM target hardware.
- amluto 8y agoI’m not sure, but I’m quite confident that they made no effort to extend the proof to include a model of the hardware and the low-level asm. Doing this would be hard — consider bugs like BadIRET or CVE-2018-8897. BadIRET would have been caught by any halfway credible model of the hardware. CVE-2018-8897, on the other hand, was the result of CPU behavior that was totally unclear in the manual and made no sense from a first-principles perspective.