Quark is an experimental, formally verified browser.
Watch it run popular sites like GMail, Facebook, and Amazon! [video 1] [video 2]

Web browsers mediate access to valuable private data in domains ranging from health care to banking. Despite this critical role, attackers routinely exploit browser vulnerabilities to exfiltrate private data and take over the underlying system. We present Quark, a browser whose kernel has been implemented and verified in the Coq proof assistant. We give a specification of our kernel, show that the implementation satisfies the specification, and finally show that the specification implies several security properties, including tab non-interference, cookie integrity and confidentiality, and address bar integrity.

Our Web browser, Quark, exploits formal verification and enables us to verify security properties for a million lines of code while reasoning about only a few hundreds. To achieve this goal, Quark is structured similarly to Google Chrome. It consists of a small browser kernel which mediates access to system resources for all other browser components. These other components run in sandboxes which only allow the component to communicate with the kernel. In this way, Quark is able to make strong guarantees about a million lines of code (e.g., the renderer, JavaScript implementation, JPEG decoders, etc.) while only using a proof assistant to reason about a few hundred lines of code for the Quark kernel. Because the underlying system is protected from Quark's untrusted components (i.e., everything other than the kernel) we were free to adopt state-of-the-art implementations and thus Quark is able to run popular, complex Web sites like Facebook and GMail.