Authors:

• Eunsuk Kang ([email protected])
• Santiago Perez De Rosso ([email protected])
• Daniel Jackson ([email protected])

The same-origin policy (SOP) is a cornerstone of browser security. Despite its widespread adoption by modern browsers, many developers have trouble understanding exactly what the SOP provides, how to bypass it when necessary, and what its security implications are.

This chapter is somewhat different from other chapters in this book. Instead of building a working implementation of a browser with the same origin policy, our goal is to construct a concrete, executable model that serves as a simple yet precise documentation of the SOP. Like an implementation, this model can be executed to explore dynamic behaviors of the system; but unlike an implementation, the model omits low-level details that can get in the way of understanding what SOP is really about.

To construct this model, we use Alloy, a language for modeling and analyzing software design. The latest version of the Alloy Analyzer, required to run the models in this chapter, can be downloaded here.