Comment on JIT Compiling Code in 5μsparentComments−pjmlp20dMachine code is insecure, we should all run interpreted code in a formally verified interpreter.Alternatively, only allow for the execution of cryptographly signed static linked binaries, this naturally includes the interpreter above.−genxy20dIf we are sprinkling formal verification on things, we can sprinkle it on a JIT.−bastawhiz20dBut then we'd have to admit that it's not the JIT that's a problem, it's the lack of guardrails and analysis features in the machine code interfaces that higher level languages expose!−pjmlp20dOnly if it goes through verified bytecode, and the set of instructions is provable.The JIT must also only be allowed to call into specific code, controlled by the runtime, and nothing else.
Comments
Machine code is insecure, we should all run interpreted code in a formally verified interpreter.
Alternatively, only allow for the execution of cryptographly signed static linked binaries, this naturally includes the interpreter above.
If we are sprinkling formal verification on things, we can sprinkle it on a JIT.
But then we'd have to admit that it's not the JIT that's a problem, it's the lack of guardrails and analysis features in the machine code interfaces that higher level languages expose!
Only if it goes through verified bytecode, and the set of instructions is provable.
The JIT must also only be allowed to call into specific code, controlled by the runtime, and nothing else.