Papers, specs & tech reports

A chronological record of work in browser security, web policy, and program verification — from grad-school proofs to deployed standards. Most pieces are co-authored; my collaborators do the heavy lifting.

2016
A Week to Remember: The Impact of Browser Warning Storage Policies

SOUPS · Joel Weinberger and Adrienne Felt

PDF

When someone decides to ignore an HTTPS error warning, how long should the browser remember that decision? If they return to the website in five minutes, an hour, a day, or a week, should the browser show them the warning again or respect their previous decision? There is no clear industry consensus, with eight major browsers exhibiting four different HTTPS error exception storage policies. Ideally, a browser would not ask someone about the same warning over and over again. If a user believes the warning is a false alarm, repeated warnings undermine the browser’s trustworthiness without providing a security benefit. However, some people might change their mind, and we do not want one security mistake to become permanent. We evaluated six storage policies with a large-scale, multimonth field experiment. We found substantial differences between the policies and that one of the storage policies achieved more of our goals than the rest. Google Chrome 45 adopted our proposal, and it has proved successful since deployed. Subsequently, we ran Mechanical Turk and Google Consumer Surveys to learn about user expectations for warnings. Respondents generally lacked knowledge about Chrome’s new storage policy, but we remain satisfied with our proposal due to the behavioral benefits we have observed in the field.
```
@inproceedings{weinberger-felt,
  author = {Joel Weinberger and Adrienne Felt},
  title = {A Week to Remember: The Impact of Browser Warning Storage Policies},
  booktitle = {Proc. of 12th Symposium on Usable Privacy and Security (SOUPS)},
  year = {2016}
}
```
2016

Subresource Integrity

W3C Recommendation · Devdatta Akhawe, Frederik Braun, François Marier, and Joel Weinberger

Specification
2013
Verifying Higher-order Programs with the Dijkstra Monad

Programming Language Design and Implementation (PLDI) · Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Ben Livshits

PDF

Modern programming languages, ranging from Haskell and ML, to JavaScript, C# and Java, all make extensive use of higher-order state. This paper advocates a new verification methodology for higher-order stateful programs, based on a new monad of predicate transformers called the Dijkstra monad. Using the Dijkstra monad has a number of benefits. First, the monad naturally yields a weakest pre-condition calculus. Second, the computed specifications are structurally simpler in several ways, e.g., single-state post-conditions are sufficient (rather than the more complex two-state post-conditions). Finally, the monad can easily be varied to handle features like exceptions and heap invariants, while retaining the same type inference algorithm. We implement the Dijkstra monad and its type inference algorithm for the F\* programming language. Our most extensive case study evaluates the Dijkstra monad and its F\* implementation by using it to verify JavaScript programs. Specifically, we describe a tool chain that translates programs in a subset of JavaScript decorated with assertions and loop invariants to F\*. Once in F\*, our type inference algorithm computes verification conditions and automatically discharges their proofs using an SMT solver. We use our tools to prove that a core model of the JavaScript runtime in F\* respects various invariants and that a suite of JavaScript source programs are free of runtime errors.
```
@inproceedings{swamy-weinberger-dijkstra,
  author = {Nikhil Swamy and Joel Weinberger and Cole Schlesinger and Juan Chen and Ben Livshits},
  title = {Verifying Higher-order Programs with the Dijkstra Monad},
  booktitle = {Proc. of 34th Programming Language Design and Implementation (PLDI)},
  year = {2013}
}
```
2012
Monadic Refinement Types for Verifying JavaScript Programs

Microsoft Research Technical Report · Nikhil Swamy, Joel Weinberger, Juan Chen, Ben Livshits, and Cole Schlesinger

PDF

Researchers have developed several special-purpose type systems and program logics to analyze JavaScript and other dynamically typed programming languages. Still, no prior system can precisely reason about both higher-order programs and mutable state; each system comes with its own delicate soundness proof (when such proofs are provided at all); and tools based on these theories (when they exist) are a significant implementation burden. This paper shows that JavaScript programs can be verified using a general-purpose verification tool---in our case, F\*, a dependently typed dialect of ML. Our methodology consists of a few steps. First, we extend prior work on LambdaJS (Guha et al.) by translating JavaScript programs to F\*. Within F\*, we type pure JavaScript terms using a refinement of the type dyn, an algebraic datatype for dynamically typed values, where the refinement recovers more precise type information. Stateful expressions are typed using the Hoare state monad. Relying on a general-purpose weakest pre-condition calculus for this monad, we obtain higher-order verification conditions for JavaScript programs that can be discharged (via a novel encoding) by an off-the-shelf automated theorem prover. Our approach enjoys a fully mechanized proof of soundness, by virtue of the soundness of F\*. We report on experiments that apply our tool chain to verify a collection of web browser extensions for the absence of JavaScript runtime errors. We conclude that, despite commonly held misgivings about JavaScript, automated verification for a sizable subset of the language is feasible. Our work opens the door to applying a wealth of research in automated program verification techniques to JavaScript programs.
```
@techreport{Swamy-Weinberger:tech2012,
  author = {Nikhil Swamy and Joel Weinberger and Juan Chen and Ben Livshits and Cole Schlesinger},
  title = {Monadic Refinement Types for Verifying JavaScript Programs},
  institution = {Microsoft Research},
  year = {2012}
}
```
2012
Thesis: Analysis and Enforcement of Web Application Security Policies

University of California, Berkeley, Thesis

PDF

Web applications are generally more exposed to untrusted user content than traditional applications. Thus, web applications face a variety of new and unique threats, especially that of content injection. One method for preventing these types of attacks is web application security policies. These policies specify the behavior or structure of the web application. The goal of this work is twofold. First, we aim to understand how security policies and their systems are currently applied to web applications. Second, we aim to advance the mechanisms used to apply policies to web applications. We focus on the first part through two studies, examining two classes of current web application security policies. We focus on the second part by studying and working towards two new ways of applying policies. These areas will advance the state of the art in understanding and building web application security policies and provide a foundation for future work in securing web applications.
```
@techreport{weinberger:thesis2012,
  author = {Joel Weinberger},
  title = {Analysis and Enforcement of Web Application Security Policies},
  institution = {University of California, Berkeley},
  year = {2012}
}
```
2011
Diesel: Applying Privilege Separation to Database Access

ACM Symposium on Information, Computer and Communications Security (ASIACCS) · Adrienne Felt, Matthew Finifter, Joel Weinberger, and David Wagner

PDF

Database-backed applications typically grant complete database access to every part of the application. In this scenario, a flaw in one module can expose data that the module never uses for legitimate purposes. Drawing parallels to traditional privilege separation, we argue that database data should be subject to limitations such that each section of code receives access to only the data it needs. We call this data separation. Data separation defends against SQL-based errors including buggy queries and SQL injection attacks and facilitates code review, since a module's policy makes the extent of its database access explicit to programmers and code reviewers. We construct a system called Diesel, which implements data separation by intercepting database queries and applying modules' restrictions to the queries. We evaluate Diesel on three widely-used applications: Drupal, JForum, and WordPress.
```
@inproceedings{felt11diesel,
  author = {Adrienne Felt and Matthew Finifter and Joel Weinberger and David Wagner},
  title = {Diesel: Applying Privilege Separation to Database Access},
  booktitle = {Proc. of ACM Symposium on Information, Computer and Communications Security (ASIACCS), 2011},
  year = {2011}
}
```
2011
Towards Client-side HTML Security Policies

the Workshop on Hot Topics in Security (HotSec) · Joel Weinberger, Adam Barth, and Dawn Song

PDF

With the proliferation of content rich web applications, content injection has become an increasing problem. Cross site scripting is the most prominent example of this. Many systems have been designed to mitigate content injection and cross site scripting. Notable examples are BEEP, BLUEPRINT, and Content Security Policy, which can be grouped as HTML security policies. We evaluate these systems, including the first empirical evaluation of Content Security Policy on real applications. We propose that HTML security policies should be the defense of choice in web applications going forward. We argue, however, that current systems are insufficient for the needs of web applications, and research needs to be done to determine the set of properties an HTML security policy system should have. We propose several ideas for research going forward in this area.
```
@inproceedings{weinberger11policies,
  author = {Joel Weinberger and Adam Barth and Dawn Song},
  title = {Towards Client-side {HTML} Security Policies},
  booktitle = {Proc. of 6th USENIX Workshop on Hot Topics in Security},
  year = {2011}
}
```
2011
A Systematic Analysis of XSS Sanitization in Web Application Frameworks

16th European Symposium on Research in Computer Security (ESORICS) · Joel Weinberger, Prateek Saxena, Devdatta Akhawe, Matthew Finifter, and Dawn Song

PDF

While most research on XSS defense has focused on techniques for securing existing applications and re-architecting browser mechanisms, sanitization remains the industry-standard defense mechanism. By streamlining and automating XSS sanitization, web application frameworks stand in a good position to stop XSS but have received little research attention. In order to drive research on web frameworks, we systematically study the security of the XSS sanitization abstractions frameworks provide. We develop a novel model of the web browser and characterize the challenges of XSS sanitization. Based on the model, we systematically evaluate the XSS abstractions in 14 major commercially-used web frameworks. We find that frameworks often do not address critical parts of the XSS conundrum. We perform an empirical analysis of 8 large web applications to extract the requirements of sanitization primitives from the perspective of real-world applications. Our study shows that there is a wide gap between the abstractions provided by frameworks and the requirements of applications.
```
@inproceedings{weinberger11sanitize,
  author = {Joel Weinberger and Prateek Saxena and Devdatta Akhawe and Matthew Finifter and Dawn Song},
  title = {A Systematic Analysis of {XSS} Sanitization in Web Application Frameworks},
  booktitle = {Proc. of 16th European Symposium on Research in Computer Security (ESORICS)},
  year = {2011}
}
```
2010
Preventing Capability Leaks in Secure JavaScript Subests

Network and Distributed System Security Symposium (NDSS) · Matthew Finifter, Joel Weinberger, and Adam Barth

PDF

Publishers wish to sandbox third-party advertisements to protect themselves from malicious advertisements. One promising approach, used by ADsafe, Dojo Secure, and Jacaranda, sandboxes advertisements by statically verifying that their JavaScript conforms to a safe subset of the language. These systems blacklist known-dangerous properties that would let advertisements escape the sandbox. Unfortunately, this approach does not prevent advertisements from accessing new methods added to the built-in prototype objects by the hosting page. In this paper, we design an algorithm to detect these methods and use our tool to determine experimentally that one-third of the Alexa US top 100 web sites would be exploitable by an ADsafe-verified advertisement. We propose an improved statically verified JavaScript subset that whitelists known-safe properties using namespaces. Our approach maintains the expressiveness and performance of static verification while improving security.
```
@inproceedings{finifter10jssafesubsets,
  author = {Matthew Finifter and Joel Weinberger and Adam Barth},
  title = {Preventing Capability Leaks in Secure {JavaScript} Subsets},
  booktitle = {Proc. of Network and Distributed System Security Symposium, 2010},
  year = {2010}
}
```
2009
Cross-Origin JavaScript Capability Leaks: Detection, Exploitation, and Defense

USENIX Security Symposium · Adam Barth, Joel Weinberger, and Dawn Song

PDF

We identify a class of Web browser implementation vulnerabilities, cross-origin JavaScript capability leaks, which occur when the browser leaks a Java Script pointer from one security origin to another. We devise an algorithm for detecting these vulnerabilities by monitoring the "points-to"; relation of the JavaScript heap. Our algorithm finds a number of new vulnerabilities in the open-source WebKit browser engine used by Safari. We propose an approach to mitigate this class of vulnerabilities by adding access control checks to browser JavaScript engines. These access control checks are backwards-compatible because they do not alter semantics of the Web platform. Through an application of the inline cache, we implement these checks with an overhead of 1–2% on industry-standard benchmarks.
```
@inproceedings{barth09heapgraph,
  author = {Adam Barth and Joel Weinberger and Dawn Song},
  title = {Cross-Origin {JavaScript} Capability Leaks: {Detection}, Exploitation, and Defense},
  booktitle = {Proc. of the 18th USENIX Security Symposium (USENIX Security 2009)},
  year = {2009}
}
```
2007
Composition with Consistent Updates for Abstract State Machines

the International ASM Workshop · Colin Gordon, Leo Meyerovich, Joel Weinberger, and Shriram Krishnamurthi

PDF

Abstract State Machines (ASMs) offer a formalism for describing state transitions over relational structures. This makes them promising for modeling system features such as access control, especially in an environment where the policy's outcome depends on the evolving state of the system. The current notions of modularity for ASMs, however, provide insufficiently strong guarantees of consistency in the face of parallel update requests. We present a real-world context that illustrates this problem, discuss desirable properties for composition in this context, describe an operator that exhibits these properties, formalize its meaning, and outline its implementation strategy.
```
@inproceedings{gordon07asm,
  author = {Colin Gordon and Leo Meyerovich and Joel Weinberger and Shriram Krishnamurthi},
  title = {Composition with Consistent Updates for Abstract State Machines},
  booktitle = {Proc. of the International ASM Workshop, 2007},
  year = {2007}
}
```
2006
ASM Relational Transducer Security Policies

Brown University Technical Report CS-06-12 · Leo Meyerovich, Joel Weinberger, Colin Gordon, and Shriram Krishnamurthi

PDF

We present a model of the security policy for the Web-based Continue conference management tool. The policy model and properties are written as ASM Relational Transducers, which we extend with a module system in order to simplify the handling of conflicting updates. We assume prior familiarity with the security policy concerns surrounding Continue. First, we review the ASM Relational Transducer modeling and property language. Then we describe the basic structure of our policy implementation and demonstrate the ability to model useful properties in the original core ASM language. We exploring the use of the unmodified modeling language in a security policy context and describe typical ASM Relational Transducer complexity concerns and how these minimally impact our implementation. Next, we discuss difficulties encountered in representing our policy and properties in the standard ASM language, including our implementation in the appendices. Following the description of adapting ASMs for use in security modeling, we introduce policy modules and a composition operator to overcome the difficulty of programming in the original language known as the consistent update problem. Finally, we describe a reduction from our extended language to the original language, and prove it satisfies our required correctness property.
```
@techreport{Meyerovich:CS-05-12,
  author = {Leo Meyerovich and Joel Weinberger and Colin Gordon and Shriram Krishnamurthi},
  title = {{ASM} Relational Transducer Security Policies},
  institution = {CS Department, Brown University},
  number = {CS-06-12},
  year = {2006}
}
```