market | past-systems | competition | team | intellectual-property | contact
Past systems: six decades of systems that are either weak or brittle
Since the Burroughs tagged memory machines of the early 1960s, many attempts have been made to provide hardware support for the enforcement of meta-data-configured constraints on a running program. Historical failures of this plan are too numerous to mention. The only systems that have succeeded, that is, that are in widespread use today, are as follows.
-
theorem provers / static analyses, such as Rust & Coq,
-
software interpreters, such as Java, JavaScript,
-
virtual memory.
All such systems are either weak, they do not provide enough safety, such as memory safety, or brittle, one exception or mistake anywhere results in a catastrophic failure everywhere.
Static analyses / theorem provers
Static analyses / theorem provers are very hard to use on production code in legacy languages (we did this in our Elsa/Oink system at Berkeley). How many systems that you use have been through a theorem prover? Switching to a language designed from the ground up to work with a theorem prover, such as Rust or Coq can help, but even when these languages work, the amount of legacy code already written in languages not amenable to theorem proving is literally billions of lines of code. As one of my advisors said “No one is going to port Linux or Firefox to Rust anytime soon. Rust and Coq are hardly in widespread use.” https://raywang.tech/2017/12/20/Formal-Verification:-The-Gap-between-Perfect-Code-and-Reality/
I went into the class believing that formal verification is the future — the only solution to a world of software ridden with bugs and security issues. But after recent events and a semester of trying to apply formal methods, I’m a serious skeptic. In this post, I’ll discuss why I think formal verification has a long way to go — and why it just doesn’t work right now.
Even further, and this point may be difficult to appreciate without lots of experience with theorem provers, but the whole theorem-proving approach, when done without hardware support, makes the mistake of picking a fight with the Undecidability of the Halting Problem https://en.wikipedia.org/wiki/Halting_problem . The result is that such systems are brittle: if the theorem prover cannot reason about a single write anywhere your whole theorem fails everywhere. A (perhaps non-obvious) consequence of the Halting Problem being Undecidable is that this brittleness cannot be removed.
Software interpreters
Software interpreters just do not work well enough: is your kernel written in Java? (no); is your web browser written in Java? (no); is your editor written in Java? (maybe). Even the simulators themselves are brittle, that is, themselves too hard to get right: Brendan Eich (the creator of JavaScript) called our lead engineer (Daniel S. Wilkerson) and asked him to use his Berkeley research to help get use-after-free bugs out of the Spider Money JavaScript engine because they were unable to do it manually: such bugs are a devastating attack on the web browser, but they are impossible to reliably reproduce. (A contract dispute prevented this work from going forward.)
Virtual memory
Virtual memory works as designed, but is too coarse-grain, that is, semantically weak. Further, virtual memory is also too brittle, as software errors can defeat its protections: a colleague of our lead engineer at Berkeley, Robert Johnson, found 3 to 6 user-kernel-pointer bugs in every release of the Linux kernel (using his automated tool); note that even one such bug means a user program can take over the kernel https://www2.eecs.berkeley.edu/Pubs/TechRpts/2004/5587.html . Notwithstanding, engineers are so desperate for even some hardware enforcement of software safety that some web browsers now put tabs and plugins into separate virtual memory address spaces.