Security:Strawman Model

Notes

The goal is to write down formal semantics for JavaScript security in Mozilla. This is ambitious, and it may end up taking a long time (e.g. to write operational semantics). I'm starting with semi-formal scribblings.

The hard cases we want to handle include pseudo-URLs such as javascript:, loaded via static markup and dynamic script. Also we need to model the allAccess (and others?) policy available via the capability.policy... preferences. Finally, we must model the system principal, since that's what chrome: uses.

In order to avoid unsound assumptions and contradictions in the current code, I'm not modeling the detailed control stack walking rules implemented by caps. And to avoid modeling JS execution fully, I've simplified the control stack to track window objects. So if a chain of functions in one window's scope calls across windows into another global scope, the model stack grows by one item, a reference to the second global.

The goal is to prove that this model enforces the access control policies we claim to support: same origin sandboxing for web content, and least privilege for mixtures of chrome and content functions on the control stack.

Types

Principal  = (System, Origins, Unknown)       // disjoint type union
System     = {system}                         // system principal singleton
Origin     = {origin1, ..., originN}          // set of N origin principals
Origins    = powerset(Origin) - {}
Unknown    = {unknown}                        // unknown principal singleton
Request    = {get, set, call}                 // principal requests of objects

Stack      = array [Window]                   // array of Window objects
             where top() = this[this.length-1]

Object     = record {parent:Object}           // record with parent field

Document   = record {children:Array = [],
                     parent:Object = null}
             where appendChild(c) = (c.parent = this, this.children.push(c))

Link       = record {href:String,
                     text:String,
                     parent:Object = null}

Button     = record {onclick:String,
                     text:String,
                     parent:Object = null}

IFrame     = record {src:String,
                     content:Window = null,
                     parent:Object = null}

Script     = record {content:String,
                     parent:Object = null}

Window     = record {location:String,
                     principal:Principal = urlPrincipal(location),
                     opener:Window = null,
                     document:Document = null,
                     parent:Object = null}

Definitions

Let P be the set of all principals.

Let <= be a binary relation by which P is partially ordered.

For all p in P, p <= system.

For all Origin principals p and q in P, !(p <= q) && !(q <= p).

For all p in P, unknown <= p.

For all principals p and q, there exists in P the greatest lower bound (p ^ q), the meet of p and q, defined by <=. (P, <=) is a meet semi-lattice.

For all p in P, (p ^ system) == p.

For all p in P, (p ^ unknown) == unknown.

Let stack:Stack = new Stack.

Let d:Document, o:Object, r:Request, s:String, w:Window, x:* in the following.

Functions

(The matches operator takes either a string right operand to prefix-match, or a `-quoted template, informally connoting a pattern to match. The result of matches is either the empty string on failure, which converts to false; or the matching prefix string on success.)

Let origin(s) = (s matches `scheme://hostpart`) || unknown.

Let pseudo(s) = !s || s matches 'about:' || s matches 'data:' || s matches 'javascript:'.

Let global() = stack.top().

Let subject() = stack.top().principal.

Let urlString(s) = s || 'about:blank'

Let urlPrincipal(s) = pseudo(s) ? subject() : origin(s).

Let parse(w, s) = parse string s in scope of w according to the Grammar.

Let load(w, s) = stack.push(w), w.location = urlString(s), w.principal = urlPrincipal(s), parse(w, fetch(w, w.location)), stack.pop()

Let open(s) = (let w = new Window('about:blank', urlPrincipal(s), global()), !s || load(w, s), w).

Let principal(x) = (x is Window) ? x.principal : principal(x.parent).

Let mapMeet(a) = a[0].principal ^ ... ^ a.top().principal.

Let canAccess(o, r) = allAccess(o, r) || principal(o) <= mapMeet(stack).

Grammar

Informal EBNF grammar for an XHTML-subset markup language, with embedded semantics, capitalized non-terminals, and quoted or lowercase terminals.

 Document ::=                          document = new Document()
              Content
 
 Content  ::= (Text | Markup)*
 
 Text     ::= text                     document.appendChild(new Text(text))
 
 Markup   ::= < 'a' 'href' '=' string '>' text '</' 'a' '>'
                                       document.appendChild(new Link(string, text))
            | < 'button' 'onclick' '=' string > text </ 'button' >
                                       document.appendChild(new Button(string, text))
            | < 'iframe' 'src' '=' string />
                                       let frame:IFrame = new IFrame(string)
                                       document.appendChild(frame)
                                       frame.content = new Window("about:blank")
                                       load(frame.content, string)
            | < 'script' > text </ 'script' >
                                       document.appendChild(new Script(text))
                                       eval(text)