Secure ECMAScript

Gareth Smith

gds@doc.ic.ac.uk

Previously at FMATS…

trustDiagramFuture.png

Untrusted Code

tsunamimap.png

Untrusted Code

tsunamiform.png

iframes

iframes.png

iframes

This section describes a security model that is underdefined, imperfect, and does not match implementations. Work is ongoing to attempt to resolve this, but in the meantime, please do not rely on this section for precision. Implementors are urged to send their feedback on how cross-origin cross-global access to Window and Location objects should work. See bug 20701.

Google Caja

…a tool for making third party HTML, CSS and JavaScript safe to embed in your website.

Caja uses an object-capability security model to allow for a wide range of flexible security policies

OCap Language

  • Memory safe:
    • unforgeable references
    • encapsulation
  • Effects only though references
  • No (powerful) references by default

Untrusted Code

eval(EVIL)
evilcloud.png
feqevalpre.png
f = eval(EVIL)
feqevalpre.png
f = eval(EVIL)
feqevalpost.png
feqevalpost.png
f()
feqevalpost.png
f()
feqevalpost.png
feqevalpost.png
f(A)
feqevalpost.png
f(A)
unprotected.png

Membranes

membstart.png
membbarrier.png
membbarrier.png
f(protect(A))
membAProtected.png
membAProtected.png
var foo = ob.foo;
membAProtected.png
var foo = ob("foo");
membBprotected.png
membKillSwitch.png
membKillSwitch.png
kill();
membPostKill.png
var Membrane = function(ref) {
  var killed = false;

  var Guard = function(ref) {
    var access = function(field) {
      if(!killed) return Guard(ref[field]); }
    if(primitive(ref)) { return ref; } else { return access; }
  }
  var access = Guard(ref);
  var kill = function() { killed = true; }
  return {access: access, kill: kill};
}

Reasoning

membstart.png

\begin{displaymath}
\obj_A(\js{foo}:B) \sep \obj_B() \sep {\textrm{\color{red}UNTRUSTED}}
\end{displaymath}

frame1.png

\begin{displaymath}
\obj_A(\js{foo}:B) \sep \obj_B() \sep {\textrm{\color{red}UNTRUSTED}}
\end{displaymath}

frame2.png

\begin{displaymath}
\obj_A(\js{foo}:B) \sep \obj_B() \sep {\textrm{\color{red}UNTRUSTED}}
\end{displaymath}

framebroken.png

\begin{displaymath}
\obj_A(\js{foo}:B) \sep \obj_B() \sep {\textrm{\color{red}UNTRUSTED}}
\end{displaymath}

membstart.png

\begin{displaymath}
\begin{array}{l}
\obj_A(\js{foo}:B) \sep \obj_B() \sep {\textrm{\color{red}UNTRUSTED}}\\
{} \sep {\color{green}A\bp\{A,B\}} \sep {\color{green}B\bp\{A,B\}}
\end{array}
\end{displaymath}

framefixed.png

\begin{displaymath}
\begin{array}{l}
\obj_A(\js{foo}:B) \sep \obj_B() \sep {\textrm{\color{red}UNTRUSTED}}\\
{} \sep {\color{green}A\bp\{A,B\}} \sep {\color{green}B\bp\{A,B\}}
\end{array}
\end{displaymath}

membKillSwitch.png

\begin{displaymath}
\begin{array}{l}
  \obj_A(\js{foo}:B) \sep \obj_B() \sep {\textrm{\color{red}UNTRUSTED}}\\
  \\
  {}\sep{\color{teal}\newfun_{F_K}(\dots)} \sep {} \\
  \LiveMembrane_{M}({\color{teal}F_K},{\color{gray}\{G1,G2\}}) \sep {}\\
  {\color{blue}Guard_{G1}(M,A,{\color{green}\{A,B\}},{\color{gray}\{G1,G2\}})} \sep {}\\
  {\color{blue}Guard_{G2}(M,B,{\color{green}\{A,B\}},{\color{gray}\{G1,G2\}})} \\
\end{array}
\end{displaymath}

\begin{displaymath}
\begin{array}{l}
  \MembraneInstance_{M}({\color{teal}F_K}, {\color{blue}GS})  \triangleq\\
  \begin{array}{@{\qquad}l}
   \obj_M({\color{blue}\js{Guard}: F_{MG}}, {\color{teal}\js{kill}: F_{K}},\dots) \sep {} \\
      \newfun_{\color{blue}F_{MG}}(M:\_, \dots) \sep {}\\
      {\color{gray}M\bp({\color{gray}GS}\cup\{{\color{gray}F_{MG}},{\color{gray}F_{K}}\})
      \sep {\color{gray}F_{MG}}\bp\{M\}}
  \end{array}\\
  \\
  \LiveMembrane_M(F_K,GS)  \triangleq\\
  \qquad {\color{gray}\MembraneInstance_{M}(F_K,GS)} \sep (M, killed) \pointsto \false \\
  \DeadMembrane_M(F_K,GS)  \triangleq \\
  \qquad {\color{gray}\MembraneInstance_{M}(F_K,GS)} \sep (M, killed) \pointsto \true \\
  \\
  {\color{blue}\Guard_{G}({\color{black}M,r,}{\color{green}TS},{\color{gray}GS})} \triangleq \\
  \begin{array}{@{\qquad}{l}}
    \newfun_{\color{blue}G}(\dots M, r, \dots) \sep r \bp ({\color{green}TS} \cup {\color{gray}GS}) \sep G\bp\_
  \end{array}
\end{array}
\end{displaymath}

membKillSwitch.png

\begin{displaymath}
  \begin{array}{c}
    \logic{
      \obj_A() \sep
      A \bp {\color{green}TS} \sep \mathit{Membrane}
    } \\
    \js{Membrane(A);} \\
    \logic{
      \obj_A() \sep
      \mathit{Membrane} \sep {}\\
      \\
      \LiveMembrane_M({\color{teal}F_K},\{G1\}) \sep {}\\
      {\color{teal}\newfun_{F_K}(\dots)} \sep {\color{teal}F_K\bp\{\rv\}} \sep{}\\
      {\color{blue}Guard_{G1}(M,A,{\color{green}TS},\{G1\})} \sep {}\\
      \obj_{\rv}({\color{teal}kill:F_K},{\color{blue}access:G1})
    }
  \end{array}
\end{displaymath}

membKillSwitch.png

\begin{displaymath}
  \begin{array}{c}
    \logic{
      \LiveMembrane_M({\color{teal}F_K},GS) \sep {}\\
      {\color{blue}Guard_{G1}(M,A,{\color{green}TS},GS)} \sep {}\\
      \obj_A(foo:B) \sep \obj_B() \sep B\bp{\color{green}TS}
    } \\
    \js{G1(A);} \\
    \logic{
      \LiveMembrane_M({\color{teal}F_K},(GS\cup\{G2\})) \sep {}\\
      {\color{blue}Guard_{G1}(M,A,{\color{green}TS},(GS\cup\{G2\}))} \sep {}\\
      {\color{blue}Guard_{G2}(M,B,{\color{green}TS},(GS\cup\{G2\}))} \sep {}\\
      \obj_A(foo:B) \sep \obj_B()
    }
  \end{array}
\end{displaymath}

\begin{displaymath}
  \begin{array}{c}
    \logic{
      \LiveMembrane_M({\color{teal}F_K},GS) \sep {}\\
      {\color{teal}\newfun_{F_K}(\dots)}
    } \\
    F_K\js{();} \\
    \logic{
      \DeadMembrane_M({\color{teal}F_K},GS) \sep {}\\
      {\color{teal}\newfun_{F_K}(\dots)}
    }
  \end{array}
\end{displaymath}

Possible Future work

Mutually Untrusted Code

humblebundle.png

Mutually Untrusted Code

paypal.png

Thanks

membKillSwitch.png trustDiagramFuture.png