2 ms·
Nah It's damn near impossible to verify that the JIT is correct. But it is possible to verify at runtime that the code that the JIT emitted obeys some memory
by pizlonator 27d ago
Nah
It's damn near impossible to verify that the JIT is correct.
But it is possible to verify at runtime that the code that the JIT emitted obeys some memory safety law.
(V8's heap sandbox is an example of this; a sarcastic JIT would be an arguably stronger example of this.)
- Ohentis 27d agoIf you have a runtime check of some correctness, why can't you just prove that the output of your compiler always passes that check?
- amluto 27d agoOne might argue that verifying the correctness of a JIT is basically the same problem as verifying the correctness of an entire compiler, with the added caveat that malicious inputs to the JIT are expected whereas malicious inputs to a compiler might be seen as rare. IIRC rustc still has a couple of known soundness bugs, for example. It’s only been a few weeks since someone managed to exploit Lean, and Lean is all about formalizing things :)