[_Nat_]

I'd prefer a [provably secure](https://en.wikipedia.org/wiki/Provable_security ) JavaScript-engine as a default. Or, if provable-security would be a bit much for a near-term project, something more heavily based in a simple engine-design, without trying to optimize stuff and perhaps including seemingly-redundant run-time checks.

Ya know, stuff like type-checking arguments, using stronger restrictions on async-calls to avoid potential race-conditions, more parameter-validation, relying on automatic-memory-management to avoid bugs, always bound-checking on array-accesses, always overflow-checking math, and so forth. In general, code that's designed to be simple and plainly correct, resisting the temptation to optimize.

Don't get me wrong, I appreciate that a lot of security-folks do good work trying to help identify-and-patch vulnerabilities in V8/etc.. And I appreciate that that enables a balance between performance and security that might be right for some applications. However, there're a lot of cases where I'd prefer a heavier focus on security.

[rurban]

https://bellard.org/quickjs/ would be the easiest effort then

[relaunched]

I've been in the security field a while, what exactly do you mean by provably secure?

[sterlind]

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.

[labawi]

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.

[stjohnswarts]

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