Ph.D. Student
University of Pennsylvania
Department of Computer and Information Science
bohannon@cis.upenn.edu
I successfully defended my dissertation on Feb 7, 2012 and officially graduated in the Spring 2012 semester. However, I have left my web page intact for the time being. I now work at Google, Inc in New York City. For more recent information about me, check my personal web site.
The goal of my dissertation research has been to apply mathematical rigor to the design and enforcement of web browser information security policies. This will involve three key steps:
I have been involved in the POPLmark project at Penn and am interested in comparing techniques for representing inductive data types with binding in the Coq proof assistant.
I have worked on extending the results from the Harmony project to bi-directional transformations on relational data and string data.
My advisor is Benjamin Pierce.
I defended my dissertation on Feb 7, 2012, and I submitted the final draft to the university on Apr 16, 2012.
Abstract:
A web browser works with data and scripts from different sources, and these sources are not all trusted equally by the user of the browser. This fact requires web browser designers to take special care in order to keep information secure within the browser: data from one source should not be stolen or corrupted by a script from another source. This aspect of web browser design is what we will call web script security.
The effectiveness of security checks designed to enforce web script security must ultimately be judged in terms of their effect on the outwardly visible behavior of the browser. In light of this fact, this dissertation defines a policy for web script security to refer to a logical constraint on a browser's behavior, stated exclusively in terms of the aspects that are outwardly visible, either to the network or to the user. Such end-to-end policies are naturally appealing. However, there is a reason they are rarely used for real-world systems: it is usually very unclear how to write down precise, flexible security policies of this sort. Supposing that one could write down such policies for web script security, a second obstacle would then arise: the problem of drawing a precise connection between such end-to-end policies and the security mechanisms that one would actually implement in a browser.
This dissertation demonstrates that such information security policies for web browsers can in fact be written down—precisely and without reference to security enforcement mechanisms implemented inside the browser. Moreover, the mechanisms for enforcing those policies can be designed and formally proved correct within mathematical models of web browsers that are detailed enough to capture the inherent complexities of the domain. This dissertation supports these claims by (1) introducing mathematical tools for stating and proving end-to-end information security properties for software systems that are driven by buffered, asynchronous I/O; (2) introducing a particular mathematical model of a web browser that is accompanied by a security policy for confidentiality and is equipped with security mechanisms intended to enforce the policy; and (3) offering a proof that the security mechanisms in the model do enforce the policy, a proof which has been mechanized and verified in the Coq proof assistant.
In 1996 I graduated from high school in Emmett, Idaho. I spent two years at the College of Idaho before transferring to Northwestern University in 1998.
