Confirmed users, Bureaucrats and Sysops emeriti
419
edits
Security:Strawman Model: Difference between revisions
→Notes
(→Notes) |
|||
| (50 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
=== Notes === | |||
The goal is to write down formal semantics for JavaScript security in Mozilla. This is ambitious, and it may end up taking a long time (e.g. to write operational semantics). I'm starting with semi-formal scribblings. | |||
The hard cases we want to handle include pseudo-URLs such as about:, data:, and javascript:, loaded via static markup and dynamic script. The newborn state of a window created by window.open, where properties can be preset by the opener that will not be erased by a new document loaded into the window (or equivalently, written by document.write), should be handled correctly. Also we need to model the allAccess policy available via the <code>capability.policy...</code> preferences. Finally, we must model the system principal, since that's what chrome: uses. | |||
In order to avoid unsound assumptions and contradictions in the current code, I'm not modeling the detailed control stack walking rules implemented by caps. And to avoid modeling JS execution fully, I've simplified the control stack to track window objects. So if a chain of functions in one window's scope calls across windows into another global scope, the model stack grows by one item, a reference to the second global. | |||
The main goal is to prove that this model enforces the access control policies we claim to support: same origin sandboxing for web content, and least privilege for mixtures of chrome and content functions on the control stack. | |||
A further goal is to handle mixtures of origins, at first by mapping their greatest lower bound to a new nonce (null) principal, but eventually with policy that allows origins to join their trust domains and collaborate safely. Think browser-based mashups here. | |||
=== Types === | === Types === | ||
<pre> | <pre> | ||
Principal = (System, Origins, Unknown) // disjoint type union | Principal = (System, Origins, Unknown) // disjoint type union | ||
System = {system} | System = {system} // system principal singleton | ||
Origin = {origin1, ..., originN} | Origin = {origin1, ..., originN} // set of N origin principals | ||
Origins = powerset(Origin) - {} | Origins = powerset(Origin) - {} | ||
Unknown = {unknown} | Unknown = {unknown} // unknown principal singleton | ||
Request = {get, set, call} | Request = {get, set, call} // principal requests of objects | ||
Stack = array [ | |||
Stack = array [Window] // array of Window objects | |||
where top() = this[this.length-1] | |||
Object = record {parent:Object} | |||
Object = record {parent:Object} // record with parent field | |||
principal:Principal, | Document = record {children:Array = [], | ||
opener:Window, | parent:Object = null} | ||
document:Object} | where appendChild(c) = (c.parent = this, this.children.push(c)) | ||
Link = record {href:String, | |||
text:String, | |||
parent:Object = null} | |||
Button = record {onclick:String, | |||
text:String, | |||
parent:Object = null} | |||
IFrame = record {src:String, | |||
content:Window = null, | |||
parent:Object = null} | |||
Script = record {content:String, | |||
parent:Object = null} | |||
Window = record {location:String, | |||
principal:Principal = urlPrincipal(location), | |||
opener:Window = null, | |||
document:Document = null, | |||
parent:Object = null} | |||
</pre> | </pre> | ||
| Line 22: | Line 55: | ||
Let P be the set of all principals. | Let P be the set of all principals. | ||
Let <= be a binary relation by which P is partially ordered. | Let <= be a "trust bound" binary relation by which P is partially ordered. | ||
For all p in P, p <= system. | For all p in P, p <= system. | ||
| Line 36: | Line 69: | ||
For all p in P, (p ^ unknown) == unknown. | 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 === | === Functions === | ||
| Line 43: | Line 80: | ||
Let origin(s) = (s matches `scheme://hostpart`) || unknown. | Let origin(s) = (s matches `scheme://hostpart`) || unknown. | ||
Let pseudo(s) = | Let pseudo(s) = !s || s matches 'about:' || s matches 'data:' || s matches 'javascript:'. | ||
Let global() = stack.top() | Let global() = stack.top(). | ||
Let subject() = stack.top(). | Let subject() = stack.top().principal. | ||
Let urlString(s) = | Let urlString(s) = s || 'about:blank' | ||
Let urlPrincipal(s) = pseudo(s) ? subject() : origin(s). | Let urlPrincipal(s) = pseudo(s) ? subject() : origin(s). | ||
Let | 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 principal(x) = (x is Window) ? x.principal : principal(x.parent). | ||
Let | Let mapMeet(a) = a[0].principal ^ ... ^ a.top().principal. | ||
Let canAccess(o, r) = allAccess(o, r) || principal(o) <= mapMeet(stack). | |||
=== Grammar === | === Grammar === | ||
Informal | Informal EBNF grammar for an XHTML-subset markup language, with embedded <i>semantics</i>, capitalized non-terminals, and quoted or lowercase terminals. | ||
Document ::= <i>document = new Document()</i> | Document ::= <i>document = new Document()</i> | ||
Content | Content | ||
Content ::= (Text | Markup)* | Content ::= (Text | Markup)* | ||
| Line 70: | Line 114: | ||
Text ::= text <i>document.appendChild(new Text(text))</i> | Text ::= text <i>document.appendChild(new Text(text))</i> | ||
Markup ::= | Markup ::= < 'a' 'href' '=' string '>' text '</' 'a' '>' | ||
<i>document.appendChild(new Link(string, text))</i> | <i>document.appendChild(new Link(string, text))</i> | ||
| < 'button' 'onclick' '=' string > text </ 'button' > | | < 'button' 'onclick' '=' string > text </ 'button' > | ||
<i>document.appendChild(new Button(string, text))</i> | <i>document.appendChild(new Button(string, text))</i> | ||
| < 'iframe' 'src' '=' string /> | | < 'iframe' 'src' '=' string /> | ||
<i>document.appendChild(new | <i>let frame:IFrame = new IFrame(string) | ||
document.appendChild(frame) | |||
frame.content = new Window("about:blank") | |||
load(frame.content, string)</i> | |||
| < 'script' > text </ 'script' > | | < 'script' > text </ 'script' > | ||
<i>document.appendChild(new Script(text)) | <i>document.appendChild(new Script(text)) | ||
eval(text)</i> | eval(text)</i> | ||