Understanding the Challenges in Browser Logic Correctness
Shuo Chen, Microsoft Research
Abstract: There is no doubt that security issues in browsers are serious, as people use browsers for serious matters on a daily basis, such as banking, shopping and communication. The scope of browser security is very broad—it includes topics in multiple aspects: security policy design, policy enforcement, browser interactions with OS/web server/network, as well as security usability considerations. In this talk, I only focus on logic correctness of browsers: in the past two years, my colleagues and I realize that due to the intrinsic complexity of browser logic, implementing correct logic to achieve even the most basic security requirements are challenging, although these requirements seem disguisingly simple. In the first half of this talk, I will analyze a number of security bugs, most discovered by us, to demonstrate such challenges. These bugs allow pages to be misidentified by arbitrary URLs on the address bar, documents to be accessed by scripts from a different domain, and HTTPS communications to be accessed by a network man-in-the-middle machine. These are by no means "stupid" bugs, but some natural by-products of the browser's logic complexity. In the second half of the talk, I exemplify two approaches to tackle the logic correctness challenges: (1) static formal verification to examine the logic that we can extract and model; (2) runtime instrumentation to guard against complex and unknown logic. I will conclude by arguing that more research efforts should be invested on the methodologies to analyze and ensure browser logic correctness.