4 ms·
Equating the provided memory safety of a Rust program without direct unsafe usage to a complex JIT built in C++ seems willfully ignorant. The attack surface wou
by Voultapher 3y ago
Equating the provided memory safety of a Rust program without direct unsafe usage to a complex JIT built in C++ seems willfully ignorant. The attack surface would still be the mostly formally verified Rust type system and standard library https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/.
- kldx 3y agoFor the JS lifetime machinery that's entirely out of rust's borrow checker shouldn't one verify the properties of unsafe code (which I imagine the garbage collector would use)? As I understand it, Rusthornbelt exists to prove unsafe code at the cost of manual verification. As someone who's a novice in verification using model checkers, writing proofs for simple algorithms is hard enough already, so I don't see the viability of a fully verified JIT. Is there a CompCert-C equivalent for V8/JSC?
- Voultapher 3y agoThe isomorphic interpreter that I was talking about, and as shown in the cloudflare blog, does not generate new machine code. All it does is jump around in the statically verified safe Rust code. So it is extremely robust. Even if there are logic bugs in it, they will not manifest as UB.