5 ms·

For it to be memory safe, do you have to disable the JIT?

• pizlonator 12d ago
  Yeah
  • amluto 12d ago
    It sounds technically possible to build a JIT where a verifier checks that the JIT-generated code is correctly pizlonated before allowing it to become executable. :)
    • pizlonator 12d ago
      Yes I have a new tech called SaRCAsm, which is a memory-safe assembler. So the next step is a "Sarcastic JIT" :-)
    • Ohentis 12d ago
      I think it makes more sense to verify that the jit is correct than to verify that it's output is correct at runtime.
      • pizlonator 12d 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 11d ago
          If 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 11d ago
          One 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 :)