3 ms·

The issue here isn’t things being “verifiably secure”. languages like js and lua run in a sandboxes environment where the only functions and operations that are

by olliej 2y ago

The issue here isn’t things being “verifiably secure”. languages like js and lua run in a sandboxes environment where the only functions and operations that are permitted are those explicitly added by the host environment. Those sources languages are easily validated as correct code. [edit: I realize I should clarify something “correct” and “verifiable” here do not mean “bug free”, it means ‘cannot interfere with or violate language or environment state, memory, or other invariants’] The issue here is that the hosting environment is allowing the user/attacker to provide the bytecode that is generated from the provably correct code. That byte code is not itself verifiable statically, and is not verified at runtime (and it might not even be possible to). This is not to say that bytecode is not verifiable - Java, .NET, or even WASM (which is intentionally very low level) are verifiable bytecode environments. The issue is that a byte code must be _designed_ to be verifiable (and early Java bytecode was not due to JSR or similar iirc). Lua’s bytecode is designed for execution, and so allowing arbitrary bytecode execution is not too dissimilar from a JS engine allowing a website to provide direct access to their bytecode interpreter which would be similarly catastrophic.

dfox 2y ago
The issue is not really about the verifiability of the bytecode but about the interpreter checking the invariants. JVM bytecode is intentionally designed to be verifiable so that the inner loop of the interpreter does not need to care about whether the operation is executed with correctly typed operands (which in the JVM case would be highly impractical and would essentially mean that you need twice the amount of memory). You can design a system where the bytecode is not verifiable, but instead the checks are done at runtime, CPython works that way.
worewood 2y ago
Yeah absolutely. This exploit is akin to V8 allowing websites to supply its own bytecode (not WASM -- talking about the internal bytecode here) to it instead of Javascript.

by olliej 2y ago

dfox 2y ago

The issue is not really about the verifiability of the bytecode but about the interpreter checking the invariants. JVM bytecode is intentionally designed to be verifiable so that the inner loop of the interpreter does not need to care about whether the operation is executed with correctly typed operands (which in the JVM case would be highly impractical and would essentially mean that you need twice the amount of memory). You can design a system where the bytecode is not verifiable, but instead the checks are done at runtime, CPython works that way.

worewood 2y ago

Yeah absolutely. This exploit is akin to V8 allowing websites to supply its own bytecode (not WASM -- talking about the internal bytecode here) to it instead of Javascript.