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 [Activation]           // array of activation objects
Activation = record {global:Window,
                     subject:Principal}
Object     = record {parent:Object}       // record with parent field
Window     = record {parent:Object = null,
                     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

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

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

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

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

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

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

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

Grammar

Informal subset EBNF grammar for an XHTML-subset markup language, 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 (a, button, iframe, script).

 Document ::=                          document = new Document()
              Content                  document.close()
 
 Content  ::= (Text | Markup)*
 
 Text     ::= text                     document.appendChild(new Text(text))
 
 Markup   ::= < tagname />             document.appendChild(new Node(tagname))
            | < tagname >              document.pushChild(new Node(tagname))
                Content
              </ tagname >             document.popChild()
            | < '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 />
                                       document.appendChild(new IFrame(string))
            | < 'script' > text </ 'script' >
                                       document.appendChild(new Script(text))
                                       eval(text)