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 access(o) = principal(o) <= (stack[0] ^ ... ^ stack.top()).