Quark : A Web Browser with a Formally Verified Kernel

Eugen Leitl eugen@leitl.org
Mon Sep 9 01:42:47 PDT 2013


http://goto.ucsd.edu/quark/

Quark : A Web Browser with a Formally Verified Kernel

University of California, San Diego

Computer Science and Engineering

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.

Publications

Establishing Browser Security Guarantees through Formal Shim Verification
[Tech Report] 

USENIX Security 2012 

Dongseok Jang, Zachary Tatlock, Sorin Lerner 

Downloads

Source code(.tar.gz) (Version 0.1, 08/07/2012, 1.3MB)

Contributors


Dongseok Jang	

Zachary Tatlock	

Sorin Lerner



More information about the cypherpunks mailing list