3 ms·
In the future we can ask that your JaveScript and Wasm comes with a proof of being benign.
by eru 1mo ago
In the future we can ask that your JaveScript and Wasm comes with a proof of being benign.
- valleyer 1mo agoPrior art: the evil bit https://datatracker.ietf.org/doc/html/rfc3514 https://datatracker.ietf.org/doc/html/rfc3514
- muvlon 1mo agoWhat would that even look like? What is "benign"? The browser environment already has pretty strict rules for what the JS can do. It's not allowed to read your files, see your webcam without permission, know about other tabs or windows etc. The problem here is that the browser failed to correctly implement those rules. If the chromium team cannot do that, what makes you think they can implement any other kind of "benign code" verification with zero bugs?
- eru 1mo agoTo give an example that goes beyond what you already suggested: You can prove that your code terminates (or rather responds to events in a finite time, even if the event loop itself runs forever.) Or you can even prove that your code reacts quickly, ie within some time limit. You can also prove memory limits. > The problem here is that the browser failed to correctly implement those rules. If the chromium team cannot do that, what makes you think they can implement any other kind of "benign code" verification with zero bugs? Defense in depth. And you can have competing implementations relatively easily for this, and another way to find and report bugs. Especially if the verifier is open source. The verifier itself can be pretty simple: it's the prover that's complicated and needs smarts, but that's being run on the author's computer, not in the user's browser.
- muvlon 1mo agoI'll believe this when it's done. Nothing I've seen so far indicates that this would be feasible. As a practical counterexample, the Linux kernel has a verifier for eBPF code that is loaded by untrusted users. That is a much more constrained environment than JS, but they still constantly have verifier bugs. It's so bad that distros almost universally distrust the verifier and instead set things up s.t. only root can load any eBPF code.
- account42 1mo agoIn practice it would be "big tech has provided a digital signature that the author has paid the required software tax".
- eru 1mo agoSignatures are very different from proofs.