Security:Strawman Model

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 {parent:Object,
                     children:Array = []}
             where appendChild(c) = (c.parent = this, this.children.push(c))

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

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

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

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

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

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)

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).