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

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

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 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 (button, iframe, script).

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