4 ms·
The frustrating thing is that we know how to write absolutely secure browsers (or other executors/renderers/etc. of untrusted data) using formal methods. Unfort
by wyager 5y ago
The frustrating thing is that we know how to write absolutely secure browsers (or other executors/renderers/etc. of untrusted data) using formal methods. Unfortunately, because most of the negative externality falls on users who don't know any better, the economics don't really work out.
- astrange 5y agoI'm not sure you can actually prove a TLS implementation is correct. It depends on the system clock being right, OCSP server being online, etc. Even the encryption has to be free of side channels like timing attacks which are left out of what most people think of as a proof.
- wyager 5y agoYou can prove a TLS implementation correct up to defined assumptions (e.g. clock consistency). There are already some projects working on this, eg https://project-everest.github.io/ https://project-everest.github.io/
- twox2 5y agoUnlikely... these bugs are all logic bugs. They won't be mitigated by using formal methods, because most of these bugs adhere to pre-defined specs. The problem with browses is that these specs are often in conflict with each other for new and/or obscure features.
- wyager 5y agoLogic bugs are the primary category of bugs targeted by heavyweight formal methods. Most JS features don't even have a formal spec which is part of the problem.