San Diego, Aug. 8, 2012 -- In part two of our three-part series on UC San Diego computer-science research papers delivered at the USENIX Security Symposium in Bellevue, WA, this week, we report on efforts by a team from the Computer Science and Engineering department to design a more secure browser. It's called Quark, and the paper delivered today by Ph.D. student Dongseok Jang was co-authored with fellow graduate student Zachary Tatlock and CSE professor Sorin Lerner. This article also appears in the Summer 2012 issue of the Center for Networked Systems (CNS) Newsletter.
There is one known way to bridge this formality gap: implement the software in a proof assistant and use the proof assistant’s interactive environment to formally prove, in full formal detail, that the software implementation is correct. More specifically, the programmer defines a specification stating what the code should do, and then uses the proof assistant to formally prove that the code in fact satisfies this specification, beginning with the most basic axioms and then building on them. Because of the precise way in which the program has been constructed, and the foundational nature of the proof, this kind of formal verification provides extremely strong guarantees.
In the past, however, this kind of verification has faced a number of practical barriers. One of the main challenges is that building formal proofs for applications with millions of lines of code is extremely time consuming, if not completely impossible. As a result, programmers using proof assistants have either restricted themselves to verifying stripped-down versions of their applications, or have had to expand heroic effort to perform the proofs, spending much more time and programmer-power than would be practical.
Jang, Tatlock and Lerner speculated: What if there were ways to make the proofs easier by restricting the code that must be verified to a few hundred lines (as opposed to a few million)? The research team devised a technique, dubbed ‘formal shim verification’, for doing just this. Formal shim verification, says Lerner, consists of “creating a small browser kernel which mediates access to resources for all other browser components, and then formally verifying that this browser kernel is correct in a proof assistant.” In other words, only a small part of the application that is vulnerable to outside scrutiny and attack will be verified using a proof assistant.
Following these design parameters, the team created Quark, a Web browser that uses a kernel-based architecture similar to Google Chrome. In particular, the heart of Quark is a small kernel responsible for mediating access to the rest of the application. Unlike Chrome’s kernel, however, the Quark kernel has been verified in full formal detail using a proof assistant, allowing it to make strong guarantees about the security of the browser. As Jang explains, Quark “exploits formal shim verification and enables us to verify security properties for a million lines of code while reasoning about only a few hundred lines of code in the kernel.” This critical distinction between a verified kernel and the non-verified components allowed the researchers to incorporate a number of state-of-the-art implementations into the non-verified parts of Quark, while still maintaining strong security guarantees. For example, Quark is able to use the WebKit open-source layout engine, the same layout engine used in Safari and Chrome. Using such realistic components has made Quark into a practical and usable browser, which can successfully run complex pages like Gmail, Google Maps, Facebook and Amazon.
During the prototyping phase of Quark, one thing became clear: “When forced to choose between adding complexity to the browser kernel,” says Jang, “it was always better to keep the kernel as simple as possible.” As a result, the current version of Quark is in some cases too simplistic. For example, it does not support some standard features of the web, such as third-party cookies, and in some cases it enforces non-standard security policies. Despite these current limitations, Quark is still capable of running many complex Web applications, including Facebook and Gmail.
Tatlock, Jang and Lerner are determined that this is only the first implementation of Quark. They already have some ideas about how to include a number of standard browser features without severely complicating their kernel or having to work through a fundamental redesign. Concludes Tatlock: “Our approach will handle more standard policies given design changes to our prototype and further engineering effort.”
*Establishing Browser Security Guarantees through Formal Shim Verification, Dongseok Jang, Zachary Tatlock and Sorin Lerner, Proc. 21st USENIX Security Symposium, August 2012.
Doug Ramsey, 858-822-5825, firstname.lastname@example.org