Hacker News new | ask | show | jobs
by relaunched 1547 days ago
I've been in the security field a while, what exactly do you mean by provably secure?
2 comments

probably a JS engine with guarantee through formal methods that sandbox escapes are impossible. for a JIT engine, this might mean asserting that control flow inside generated code never leaves it, and only accesses pages allocated to it. these obligations would also need to be carried through to standard library implementations.

i.e. probably secure analogously to how seL4 is provably secure. this would be infeasible for a browser, but you could actually accomplish it by running seL4 and executing the JS in an seL4 VM. you'd still have to prove everything the VM has access to is similarly secure, so still not feasible for a browser, but you could maybe make the Node.js equivalent of MSR's Ironclad.

I wish we could and I think we should.

I'm just very sad we don't have safe hardware w.r.t. memory corruption via rowhammer and I don't think any of the typical formal methods or seL4 account for it. Safely running untrusted code is nearly impossible on modern computers.

What he wants is basically impossible for software projects as big as v8 or chrome, but I guess one can dream :)