Security:Strawman Model

Types

Principal  = (System, Origin, Unknown)  // disjoint type union
System     = {system}                   // system principal singleton
Origin     = {origin1, ..., originN}    // set of N origin principals
Unknown    = {unknown}                  // unknown principal singleton
Stack      = array [Activation]         // array of activation objects
Activation = record {global:Window,
                     subject:Principal}
Object     = record {parent:Object}     // record with parent field
Window     = record {parent:Object,
                     location:String,
                     principal:Principal,
                     opener:Window,
                     document:Object}

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.

Functions

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

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

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

Let open(s) = new Window(null, s, urlPrincipal(s), global()).

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

Let canAccess(o) = (principal(o) <= (stack[0] ^ ... ^ stack.top())).

Grammar

Informal HTML subset EBNF grammar with embedded semantics, capitalized non-terminals, and quoted or lowercase terminals. Unquoted terminals stand for the obvious lexical nonterminals, e.g. tagname is any valid HTML tag name other than those quoted tagnames used in the grammar (button, iframe).

Document ::= Content

Content ::= (text | Markup)*

Markup ::= < tagname />
         | < tagname > Content </ tagname >
         | < 'button' 'onclick' '=' string > text </ 'button' >
         | < 'iframe' 'src' '=' string />