Fully Abstract Compilation to JavaScript

Pierre-Evariste Dagand

End-of-internship presentation, based on a paper of the same title by:

Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Evariste Dagand, Pierre-Yves Strub, and Ben Livshits

Your mileage with this web-based demo may vary depending on your browser. We have tried this with IE 10, Chrome and Firefox.

Secure JavaScript?

Motivation: Cryptocat

Must satisfy:

Not so secure JavaScript...

Can't rely on obscurity:

Not so secure JavaScript...

Poisoning Object:

Not so secure JavaScript...

Abusing coercions:

Not so secure JavaScript...

Walking the call-stack:

The x86 of the Web

If you write JavaScript:

Maybe you should:

(Thanks Daan for the special FX!)

Setting the scene

This talk:

The paper:

Our (only) enemy:

Compiler correctness, on closed programs

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'}\]

Compiler correctness, in context

Motivation:

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\).

Correctness: Examples

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

Correctness: Examples

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 : () 
      

Being correct is not good enough

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

Full abstraction

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.

full abstraction = reflection + preservation

Filtering in

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:

Secure wrappers

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]

Putting full-abstraction to work

Isolated LocalStorage:

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

Bootstrapping an ML-to-JS compiler

Motivation:

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

Conclusion

Theoretical results:

Practical results:

Demo

Bootstrapping an ML-to-JS compiler


Backup slides

Wait but... you need a JavaScript semantics!

Nik says "yes":

I think "maybe, maybe not":

/