Quark: A Web Browser with a Formally Verified Kernel

Quark 0.1 is a web browser whose kernel is formally verified using Coq proof assitant. Quark was originally announced at goto.ucsd.edu/quark, with a link to a source code tarball. However, there didn't seem to be a public version control repository anywhere, and sometimes academic code has a tendency to drop off the Net or at least disappear from its original publication site. This copy is meant to make sure Quark is preserved in a place where people can easily get it, fork it if they need to, etc. If Quark ever gets a home on a real public development site, then this copy can go away.

So please remember that this copy is not the official home of Quark, and check the original site for updates (goto.ucsd.edu/quark). See also the 2012 Usenix Security tech report by Dongseok Jang, Zachary Tatlock, and Sorin Lerner: Establishing Browser Security Guarantees through Formal Shim Verification.

Original README from Quark 0.1 (08/07/2012)

Quark: A Secure Web Browser with A Verified Kernel

A research browser built with a verified kernel to ensure that the kernel completely impervious to certain classes of attack following its formal security properties.

http://goto.ucsd.edu/quark