How to start a secure browser: Quark

Ran across this paper today about a pretty cool new browser, Quark:

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.

Let’s put this into more simple terms. Unlike standard programming practice with unit tests, which essentially test cases that the developer defines, these go one step further and prove that the base kernel of the system will do precisely what is specified and nothing else, if all of the assumptions are valid about the OS-base, etc.

This is to programming what mathematical proofs are to mathematics. A unit test suite is similar to doing scientific experiments and deducing your system matches the specs perfectly, a proof in programming is precisely the same as a proof in mathematics. It stops being a theory and starting being absolute fact.

This is pretty cool, especially since the code is all there to work with; proven (literally), and entirely open for review. Perhaps this will inspire some security types to do the same with cryptographic kernels.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s