Communications of the ACM
c San Diego Computer Scientists Explore Secure Browser Design
University of California, San Diego (UCSD) researchers say they have developed a new approach to secure browsing design.
They say previous verification techniques operate on a model of the browser and not its actual implementation, which creates a discrepancy between what is verified and what is implemented and enables hackers to infiltrate a browser even if it has been verified using strong formal methods.
Although computer scientists have solved this problem by using formal proofs, the proofs have millions of lines of code and are difficult to create. The UCSD researchers have developed a technique, called formal shim verification, which consists of creating a small browser kernel that mediates access to resources for all other browser components and then formally verifies that the browser kernel is correct in a proof assistant.
Using their design, the researchers created Quark, a Web browser that users a kernel-based architecture. The Quark kernel has been verified in full formal detail using a proof assistant, enabling it to make strong guarantees about the security of the browser. 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," says UCSD's Dongseok Jang.
From UCSD News (CA)
View Full Article
Abstracts Copyright © 2012 Information Inc., Bethesda, Maryland, USA
No entries found