The near ubiquity of Internet access has put a wealth of information and ever-increasing opportunities for social interaction at the fingertips of users. Driving this revolution is the modern web browser, which has evolved from a relatively simple client application designed to display static data into a complex networked operating system tasked with managing many facets of a users online experience. Support for dynamic content, multimedia data, and third-party plug-ins has greatly enriched users experiences at the cost of increasing the complexity of the browser itself. As a result, current web browsers are plagued with security vulnerabilities that provide hackers with easy access to end-user systems via browser-based attacks. Browser security efforts to date are essentially retrofits for existing web browsers and have enjoyed only limited success, as the design of modern web browsers is fundamentally flawed. To address the root of this problem, this research will develop an inherently more secure design methodology for any network-facing user application, which will be validated through the design and implementation of a new secure web browser called OP. The overall design approach combines separation and safety principles from the operating system community with validation and monitoring techniques developed by the formal methods community. By partitioning the browser into smaller subsystems and making all communication between subsystems simple and explicit, this research effort can leverage techniques from both of these communities to elicit formal guarantees about OP's correctness and ability to limit the effects of compromised subsystems.
