Must satisfy:

• Call sendProxy only on whitelisted domains
• Must not leak sendProxy
• Must not leak the encrypted text

Can't rely on obscurity:

Poisoning Object:

Abusing coercions:

Walking the call-stack:

If you write JavaScript:

• Context is everything
• Security is difficult
• Semantics, anyone?

Maybe you should:

• Use a sane language
• Compile to JavaScript
• Reason up to the source language's semantics

(Thanks Daan for the special FX!)

This talk:

• JavaScript modeled by lambda-calculus
• Extended with objects
• Including implicit coercions

The paper:

• The whole shebang
• Including coercions, stack walk, prototypes
• Same ideas at work, but more work

Our (only) enemy:

A correct ML-to-JS compiler:

\begin{align*} C\langle \_ \rangle &: ML \to JS \\ C\langle \mathtt{fun}~x \rightarrow b \rangle &\mapsto \mathtt{function}(x) \{ \mathtt{return}~ C\langle b \rangle; \} \\ C\langle x \rangle &\mapsto x \\ C\langle f~s \rangle &\mapsto C\langle f \rangle(C\langle s \rangle) \\ C\langle (x,y) \rangle &\mapsto \{\mathtt{tag}: \mathtt{"Pair"}, 0: C\langle x \rangle, 1: C\langle y \rangle \}\\ C\langle \mathtt{let}~x~=~e_1~\mathtt{in}~e_2 \rangle &\mapsto (x= C\langle e_1 \rangle, C\langle e_2 \rangle) \end{align*}

Simulation theorem (simplified)

For any ML reduction step: \[e \rightarrow_{ML} e'\] and any compilation: \[\vdash e : t \leadsto \hat{e}\] The compiled JavaScript takes some steps: \[\hat{e} \rightarrow^{+}_{JS} \hat{e'}\] and reaches a valid compilation of \(e'\): \[\vdash e' : t \leadsto \hat{e'}\]

Motivation:

• Scripts rarely run in isolation (mash-up, ads, extensions, ...)
• Do you trust your context?
• This slide: at least 5 libraries, an ML compiler, countless eval

Equivalence reflection:

Let \(e_1, e_2\) two ML programs.

If there exists an ML context that distinguishes \(e_1\) from \(e_2\),
Then there exists a JavaScript context that distinguishes \(C\langle e_1 \rangle\) from \(C\langle e_2 \rangle\).

Non example:

\begin{align*} C\langle \mathtt{true} \rangle &\mapsto \mathtt{true} \\ C\langle \mathtt{false} \rangle &\mapsto \mathtt{true} \\ \end{align*}

In ML:

	if true then diverge else () 
	    $\not\approx$ 
	if false then diverge else ()
      

In JavaScript, for any context J[-]:

	J[$C\langle true \rangle$]
	    $\approx$ 
	J[$C\langle false \rangle$]
      

Example:

\begin{align*} C\langle \mathtt{true} \rangle &\mapsto \mathtt{"yes"} \\ C\langle \mathtt{false} \rangle &\mapsto \mathtt{undefined} \\ \end{align*}

In ML:

	if true then diverge else () 
	    $\not\approx$
	if false then diverge else ()
      

In JavaScript:

	$C\langle true \rangle$ ? diverge : ()
	    $\not\approx$
	$C\langle false \rangle$ ? diverge : () 
      

Example:

In ML, for any context E[-]:

	E[fun b -> b]
	    $\approx$
	E[fun b -> if b then true else false]
      

In JavaScript:

	

	  

	    print((function(b){return b;})("foo"))
	  
	
	

	  $\not\approx$
	
	

	print((function(b){return (b ? true : false);})("foo"))
	
	

      

Equivalence preservation:

Let \(e_1, e_2\) two ML programs.

If \(e_1\) and \(e_2\) are equivalent in all ML contexts,
Then \(C\langle e_1 \rangle\) and \(C\langle e_2 \rangle\) are equivalent in all JavaScript contexts.

Non example:

In JavaScript, for any context J[-]:

	

	J[function(un){ return (function(b){return b;})($\uparrow_{\mathtt{bool}}\langle un \rangle$); }]
	
	

	  $\approx$  
	
	

	J[function(un){ return (function(b){return (b ? true : false);})($\uparrow_{\mathtt{bool}}\langle un \rangle$);}]
	
      

Intuition:

• Build the secure compiler by wrapping the naive translation
• Game between (compiled) program and (JavaScript) context
• Claim: enough to work at exposed boundaries

From Context to Program:

Objective: no junk comes in

\begin{align*} \uparrow_{\mathtt{bool}}\langle b \rangle &\mapsto b~?~\mathtt{true}~:~\mathtt{false} \\ \uparrow_{\mathtt{string}}\langle s \rangle &\mapsto \mathtt{""}~+~s \\ \uparrow_{a \to b}\langle f \rangle &\mapsto \mathtt{function}~(a)\{ \mathtt{return}~\uparrow_{b}\langle f( \downarrow_{a}\langle a \rangle )\rangle; \}\\ \uparrow_{a \times b}\langle p \rangle &\mapsto \{\mathtt{tag}: \mathtt{"Pair"}, 0: \uparrow_{a}\langle p[0] \rangle, 1: \uparrow_{b}\langle p[1] \rangle \} \end{align*}

From Program to Context:

Objective: no private name leaks

\begin{align*} \downarrow_{\mathtt{bool}}\langle b \rangle &\mapsto b \\ \downarrow_{\mathtt{string}}\langle s \rangle &\mapsto s \\ \downarrow_{a \to b}\langle f \rangle &\mapsto \mathtt{function}~(a)\{ \mathtt{return}~\downarrow_{b}\langle f( \uparrow_{a}\langle a \rangle )\rangle; \}\\ \downarrow_{a \times b}\langle p \rangle &\mapsto \{\mathtt{fst}: \downarrow_{a}\langle p[0] \rangle, \mathtt{snd}: \downarrow_{b}\langle p[1] \rangle \} \end{align*}

Example:

In ML, for any context E[-]:

      
E[fun f -> let x = (0,1) in f x; fst x]
      
$\approx$
      
E[fun f -> let x = (0,1) in let y = fst x in f x; y]
    

Isolated LocalStorage:

• Browser exports global key-value store
• Make it available to mutually distrusting scripts
• Guarantee isolation

Stating isolation:

In ML, for any context E[-]:

      

	E[let (set1, get1, rm1) = mkSafeLocalStorage () in

	  let (set2, get2, rm2) = mkSafeLocalStorage () in

	  set1 key value1;
	  set2 key value2;

	  (get1 key, get2 key);]
      
      

	$\approx$
      
      

	E[(value1, value2)]
      
    

Motivation:

• Reasonable macro-benchmark
• Who could resist <script type="text/ml">? (Click on the link to try!)
• First step toward F* in the browser

Strategy:

1. Implement an ML-to-JS compiler in ML
2. Compile the compiler to JavaScript
3. ????
4. Run ML in your browser!

Caveat:

1. The bootstrapped compiler is a proof-of-concept: it does not yet implement secure wrappers. The full F* to JavaScript compiler does, but that has yet to be boostrapped entirely within JavaScript

Theoretical results:

• Compiler correctness (equivalence reflecting)
• Compiler fully-abstract (equivalence preserving)
• Working on boundaries is enough!

Practical results:

• Secure JavaScript back-end for F* (Nik, Pierre-Yves)
• Reasonable performance
• Bootstrapped ML compiler, more to come!

Nik says "yes":

• Extension of LambdaJS
• Embedded in F*
• Executable model (in theory)

I think "maybe, maybe not":

• Semantics inspired by Dolev-Yao models
• State upfront our expectations (private names, execution flow, ...)
• Check against implementations, formal models