\[ \newcommand{\V}[1]{{{\tt{#1}}}} \newcommand{\E}[1]{{{\tt{#1}}}} \newcommand{\T}[1]{{{\textsc{#1}}}} \newcommand{\List}{\E{Ls}} \newcommand{\Lista}{\List_1} \newcommand{\Listb}{\List_2} \newcommand{\command}[1]{{\tt{#1}}} \newcommand{\cmd}{\command{C}} \newcommand{\pointsto}{\mapsto} \newcommand{\str}[1]{\text{``#1''}} \newcommand{\sep}{\mathbin{*}} \newcommand{\sepish}{\mathbin{\sqcup\mkern-21mu*}} \newcommand{\bigsep}{\mathop{\Huge \mathlarger{\mathlarger{*}}}} \newcommand{\wand}{\mathbin{-\mkern-6mu *}} \newcommand{\wandish}{\mathbin{-\mkern-4mu\sepish}} \newcommand{\st}{\mathpunct{.}} \newcommand{\false}{\text{False}} \newcommand{\true}{\text{True}} \newcommand{\none}{{\tt\text{NONE}}} \newcommand{\nan}{{\tt{NaN}}} \newcommand{\infinity}{{\tt{Infinity}}} \newcommand{\nil}{{\tt{null}}} \newcommand{\undefined}{{\tt{undefined}}} \newcommand{\emp}{{\tt{emp}}} \newcommand{\ls}{\textbf{l}} \newcommand{\rv}{\textbf{r}} \newcommand{\dotin}{\inplus} \newcommand{\scope}{\command{scope}} \newcommand{\notscope}{\command{notscope}} \newcommand{\notscopeg}{\command{notscopeglobal}} \newcommand{\Scope}{\command{Scope}} \newcommand{\proto}{\command{proto}} \newcommand{\protog}{\command{protoglobal}} \newcommand{\Proto}{\command{Prototype}} \newcommand{\getValue}{\command{getValue}} \newcommand{\get}{\command{get}} \newcommand{\newobj}{\textrm{newobj}} \newcommand{\store}{\textrm{store}} \newcommand{\obj}{\textrm{obj}} \newcommand{\js}[1]{{{\tt{#1}}}} \newcommand{\sv}{\cdot} \newcommand{\thischain}{\command{thischain}} \newcommand{\cons}{{:}} \newcommand\lgo{l_g} \newcommand{\stateaxiom}[2]{\textrm{#1: }#2} \newcommand{\staterule}[3]{\textrm{#1: }\frac{#2}{#3}} \newcommand\tr[3]{\{#1\}#2\{#3\}} \newcommand\lemp{\oslash} \newcommand{\und}{\mbox{$\bot$}} \newcommand\this{\js{this}} \newcommand\thisp{\text{@this}} \newcommand\fscopep{\textrm{@scope}} \newcommand\bodyp{\textrm{@body}} \newcommand\protop{\textrm{@proto}} \newcommand\emptystr{\text{``\,''}} \newcommand\defs{\command{defs}} \newcommand\meth{\command{This}} \newcommand{\rsep}{\qquad} \newcommand{\gap}{5pt} \newcommand\fundef{\command{new\_fun}} \newcommand{\lop}{l_{op}} \newcommand{\red}[1]{{\color{red}{#1}}} \newcommand{\blue}[1]{{\color{blue}{#1}}} \newcommand{\pink}[1]{\color{magenta}{#1}} \newcommand{\yellow}[1]{\color{green}{#1}} \]

        Reasoning about JavaScript

     
Gareth Smith    Philippa Gardner    Sergio Maffeis

Imperial College London

http://www.doc.ic.ac.uk/~gds/JSTalks/Mozilla.html

Who Are These Separation Logic People?

Peter O'Hearn John Reynolds Hongseok Yang
Queen Mary, London CMU Oxford

Who Are These Separation Logic People?

US

Harvard
Greg Morrisett
Princeton
Andrew Appel
Yale
Zhong Shao
...

Europe

UK
Queen Mary, Imperial, Microsoft Cambridge, Birmingham, Monoidics, ...
Germany
Max Planck Institute, ...
Spain
Madrid Institute for Advanced Studies, ...
...

Asia

China
University of Science and Technology of China, ...
Singapore
National University of Singapore
...

Show me the code...

Space Invader (Queen Mary and Imperial)
Memory Safety of Windows and Linux Device Drivers ~10K LOC
SLAyer (MS Research Cambridge)
Memory Safety of Systems Code ~100K LOC
Infer (Monoidics)
...can analyze and verify programs of any size.
Many others...
Smallfoot, JStar, Verifast, HeapHop...
\[\{x=0 \land y=0 \}\]
x := 4
\[\{x=4 \land y=0 \}\]
y := 5
\[\{x=4 \land y=5\}\]
x:= x + y
\[\{x=9 \land y=5\}\]
\[\{\ I\ \}\]
while(B) {
\[\{\ I \land B\ \}\]
        // Do Stuff 
\[\{\ I\ \}\]
}
\[\{\ I \land \neg B\ \}\]
\[\left\{\begin{array}{c} \text{list}(x) \land \text{list}(y) \end{array}\right\}\]
destroy(x)
\[\left\{\begin{array}{c} \text{list}(y) \end{array}\right\}\]
\[\left\{\begin{array}{c} \text{list}(x) \land \text{list}(y)\\ \land \forall l\in\text{list}(x) . l\not\in\text{list}(y) \end{array}\right\}\]
destroy(x)
\[\left\{ \begin{array}{c} \text{list}(y) \end{array} \right\}\]
\[\left\{\begin{array}{c} \text{list}(x) \land \text{list}(y)\\ \land\text{list}(z) \\ \land \forall l\in\text{list}(y) . l\not\in\text{list}(x)\\ \land \forall l\in\text{list}(z) . l\not\in\text{list}(x)\\ \land \forall l\in\text{list}(y) . l\not\in\text{list}(z)\\ \end{array}\right\}\]
destroy(x)
\[\left\{ \begin{array}{c} \text{list}(y) \land \text{list}(z)\\ \land \forall l\in\text{list}(y) . l\not\in\text{list}(z)\\ \end{array} \right\}\]
\[\left\{\begin{array}{c} \text{list}(x) \land \text{list}(y)\\ \land\text{list}(z) \land \text{list}(x2)\\ \land \forall l\in\text{list}(y) . l\not\in\text{list}(x)\\ \land \forall l\in\text{list}(z) . l\not\in\text{list}(x)\\ \land \forall l\in\text{list}(y) . l\not\in\text{list}(z)\\ \land \forall l\in\text{list}(x2) . l\not\in\text{list}(x)\\ \land \forall l\in\text{list}(x2) . l\not\in\text{list}(y)\\ \land \forall l\in\text{list}(x2) . l\not\in\text{list}(z)\\ \end{array}\right\}\]
destroy(x)
\[\left\{ \begin{array}{c} \text{list}(y) \land \text{list}(z) \\ \land\text{list}(x2)\\ \land \forall l\in\text{list}(y) . l\not\in\text{list}(z)\\ \land \forall l\in\text{list}(x2) . l\not\in\text{list}(y)\\ \land \forall l\in\text{list}(x2) . l\not\in\text{list}(z)\\ \end{array} \right\}\]
\[\left\{\begin{array}{c} \text{list}(x) \land \text{list}(y) \end{array}\right\}\]
destroy(x)
\[\left\{\begin{array}{c} \text{list}(y) \end{array}\right\}\]
\[\left\{\begin{array}{c} \text{list}(x) \sep \text{list}(y) \end{array}\right\}\]
destroy(x)
\[\left\{\begin{array}{c} \text{list}(y) \end{array}\right\}\]
\[\left\{\begin{array}{c} \text{list}(x) \end{array}\right\}\]
destroy(x)
\[\left\{\begin{array}{c} \emp \end{array}\right\}\]

The Frame Rule

\[\frac{\{\ P\ \}\ \cmd\ \{\ Q\ \}} {\{\ P \sep R\ \}\ \cmd\ \{\ Q \sep R\ \}}\]
\[\left\{\begin{array}{c} \text{list}(x) \end{array}\right\}\]
revlist(x)
\[\left\{\begin{array}{c} \text{list}(x) \end{array}\right\}\]

The Story So Far...


Reasoning about programs
Tony Hoare: 1969
Reasoning about C programs: Separation Logic
O'Hearn, Reynolds, Yang: POPL/LNCS 2001
Reasoning about DOM programs: Context Logic
Gardner, Smith, Zarfaty: PODS 2008
JavaScript Security: Operational Semantics
Maffeis, Mitchell, Tally: APLAS 2008
Reasoning about JavaScript: Variation of Separation Logic
Gardner, Maffeis, Smith: POPL 2012

Emulated Variable Store

x = 5 ; y = 6 ; a = {x:1}

Emulated Variable Store

 y = 6 ; a = {x:1}

Emulated Variable Store

 a = {x:1}

Emulated Variable Store

Two Variables, One Expression

 x = y; 
 x = y
 x = y
 x = y

Abstract Specification for Assignment

\[\{ \store_{\ls}(|\js{x}:\_,\js{y}:\V{V}) \}\]
x = y; 
\[\{ \store_{\ls}(|\js{x}:\V{V},\js{y}:\V{V}) \sep \true \}\]

A Simple Example

x = null;
y = null;
z = null;
f = function(w) {
    x = v;
    v = 4;
    var v;
    y = v;
};
v = 5;
f(null);
z = v; 
Let's try it.
\[\{ \store_{\V{LS}}(\js{x},\js{y},\js{z},\js{f},\js{v}|) \sep \ls\doteq\V{LS} \}\]
x = null;
y = null;
z = null;
f = function(w) {
    x = v;
    v = 4;
    var v;
    y = v;
};
v = 5;
f(null);
z = v; 
\[\left\{\begin{array}{c} \exists\V{L}\st\ \store_{\V{LS}}(|\js{x}:\undefined,\js{y}:4,\js{z}:5,\js{f}:\V{L},\js{v}:5)\sep {}\\ \ls\doteq\V{LS} \sep \true \end{array}\right\} \]
\[\{ \store_{\V{LS}}(\js{x},\js{y},\js{z},\js{f},\js{v}|)\sep\ls\doteq\V{LS} \}\]
x = null;
y = null;
z = null; 
\[\{ \store_{\V{LS}}(\js{f},\js{v}|\red{\js{x}:\nil},\red{\js{y}:\nil},\red{\js{z}:\nil})\sep\ls\doteq\V{LS}\sep\true \}\]
f = function(w) {
    x = v;
    v = 4;
    var v;
    y = v;
};
v = 5;
f(null);
z = v; 
\[\{ \exists\V{L}\st\ \store_{\V{LS}}(|\js{x}:\undefined,\js{y}:4,\js{z}:5,\js{f}:\V{L},\js{v}:5)\sep\ls\doteq\V{L} \sep \true \} \]
\[\{ \store_{\V{LS}}(\js{x},\js{y},\js{z},\js{f},\js{v}|)\sep\ls\doteq\V{LS} \}\]
x = null;
y = null;
z = null; 
\[\{ \store_{\V{LS}}(\js{f},\js{v}|\js{x}:\nil,\js{y}:\nil,\js{z}:\nil)\sep\ls\doteq\V{LS}\sep\true \}\]
f = function(w) {
    x = v;
    v = 4;
    var v;
    y = v;
}; 
\[\left\{\begin{array}{c} \exists\V{L}\st\ \store_{\V{LS}}(\js{v}|\js{x}:\nil,\js{y}:\nil,\js{z}:\nil,\red{\js{f}:\V{L}})\sep{}\\ \ls\doteq\V{LS}\sep\true\sep \red{\obj_{\V{L}}(|\bodyp:\lambda\js{w}\st\js{e},\fscopep:\V{LS})} \end{array}\right\}\]
v = 5; 
\[\left\{\begin{array}{c} \exists\V{L}\st\ \store_{\V{LS}}(|\js{x}:\nil,\js{y}:\nil,\js{z}:\nil,{\js{f}:\V{L}},\red{\js{v}:5})\sep{}\\ \ls\doteq\V{LS}\sep\true\sep {\obj_{\V{L}}(|\bodyp:\lambda\js{w}\st\js{e},\fscopep:\V{LS})} \end{array}\right\}\]
f(null);
z = v; 
\[\{ \exists\V{L}\st\ \store_{\V{LS}}(|\js{x}:\undefined,\js{y}:4,\js{z}:5,\js{f}:\V{L},\js{v}:5)\sep\ls\doteq\V{LS} \sep \true \} \]
(where \(\js{e} = \)
x=v; v=4; var v; y=v;
)

The Function Body (Reasoning)

\[ \left\{\begin{array}{c} \exists \V{L},\blue{\V{LOC}} \st\\ \store_{{\V{LS}}}(|{\js{x}:\nil},\js{y}:\nil,\js{z}:\nil,\red{\js{f}:\V{L}},\js{v}:5) \sep{}\\ \red{\obj_{\V{L}}(|\bodyp:\lambda\js{w}\st\js{e},\fscopep:\V{LS})} \sep\\ \blue{\obj_{\V{LOC}}(\js{x},\js{y}|\protop:\nil,\js{w}:\nil,\js{v}:\undefined)}\\ \sep \ls\doteq\blue{\V{LOC}}:\V{LS}\\ \end{array}\right\} \]
x = v;
v = 4;
var v;
y = v; 
\[ \left\{ \begin{array}{c} \exists \V{L},\V{LOC} \st\\ \store_{{\V{LS}}}(|\js{x}:\undefined,{\js{y}:4},\js{z}:\nil,\js{f}:\V{L},\js{v}:5) \sep{}\\ {\obj_{\V{L}}(|\bodyp:\lambda\js{w}\st\js{e},\fscopep:\V{LS})}\sep\\ {\obj_{\V{LOC}}(\js{x},{\js{y}}|\protop:\nil,\js{w}:\nil,{\js{v}:4})}\\ \sep\ls\doteq\V{LOC}:\V{LS} \sep \true\\ \end{array}\right\} \]

The Function Body (Reasoning)

\[ \left\{\begin{array}{c} \exists \V{L},\blue{\V{LOC}} \st\\ \store_{{\V{LS}}}(|\red{\js{x}:\nil},\js{y}:\nil,\js{z}:\nil,\js{f}:\V{L},\js{v}:5) \sep{}\\ \blue{\obj_{\V{LOC}}(\js{x},\js{y}|\protop:\nil,\js{w}:\nil,\js{v}:\undefined)}\\ \sep \ls\doteq\blue{\V{LOC}}:\V{LS}\\ \end{array}\right\} \]
x = v; 
\[ \left\{ \begin{array}{c} \exists \V{L},\V{LOC} \st\\ \store_{\V{LS}}(|\red{\js{x}:\undefined},\js{y}:\nil,\js{z}:\nil,\js{f}:\V{L},\js{v}:5) \sep{}\\ {\obj_{\V{LOC}}(\blue{\js{x}},\js{y}|\protop:\nil,\js{w}:\nil,\blue{\js{v}:\undefined})}\\ \sep\ls\doteq\V{LOC}:\V{LS}\sep \true \\ \end{array}\right\} \]
v = 4; 
\[ \left\{ \begin{array}{c} \exists \V{L},\V{LOC} \st\\ \store_{\V{LS}}(|\js{x}:\undefined,\js{y}:\nil,\js{z}:\nil,\js{f}:\V{L},\js{v}:5) \sep{}\\ {\obj_{\V{LOC}}(\js{x},\js{y}|\protop:\nil,\js{w}:\nil,\blue{\js{v}:4})}\\ \sep\ls\doteq\V{LOC}:\V{LS}\sep \true \\ \end{array}\right\} \]
var v; 
\[ \{ \dots \} \]
y = v; 
\[ \left\{ \begin{array}{c} \exists \V{L},\V{LOC} \st\\ \store_{{\V{LS}}}(|\js{x}:\undefined,\red{\js{y}:4},\js{z}:\nil,\js{f}:\V{L},\js{v}:5) \sep{}\\ {\obj_{\V{LOC}}(\js{x},\blue{\js{y}}|\protop:\nil,\js{w}:\nil,\blue{\js{v}:4})}\\ \sep\ls\doteq\V{LOC}:\V{LS} \sep \true\\ \end{array}\right\} \]

Popping The Stack

\[\{ \store_{\V{LS}}(\js{x},\js{y},\js{z},\js{f},\js{v}|)\sep\ls\doteq\V{LS} \}\]
x = null;
y = null;
z = null;
f = function(w) {
    x = v;
    v = 4;
    var v;
    y = v;
};
v = 5; 
\[\{ \exists\V{L}\st\ \store_{\V{LS}}(|\js{x}:\nil,\js{y}:\nil,\js{z}:\nil,\js{f}:\V{L},\js{v}:5)\sep\ls\doteq\V{LS} \sep \true\}\]
f(null); 
\[ \left\{ \begin{array}{c} \exists\V{L},\V{LOC}\st\\ \store_{\V{LS}}(|\red{\js{x}:\undefined},\red{\js{y}:4},\js{z}:\nil,\js{f}:\V{L},\red{\js{v}:5}) \sep{}\\ {\obj_{\V{L}}(|\bodyp:\lambda\js{w}\st\js{e},\fscopep:\V{LS})}\sep\\ {\obj_{\V{LOC}}(\js{x},\blue{\js{y}}|\protop:\nil,\js{w}:\nil,\blue{\js{v}:4})}\\ \sep\red{\ls\doteq\V{LS}}\sep \true \end{array}\right\} \]
z = v; 
\[ \left\{ \begin{array}{c} \exists\V{L},\V{LOC}\st\\ \store_{\V{LS}}(|\js{x}:\undefined,\js{y}:4,\red{\js{z}:5},\js{f}:\V{L},\red{\js{v:5}}) \sep{}\\ {\obj_{\V{L}}(|\bodyp:\lambda\js{w}\st\js{e},\fscopep:\V{LS})}\sep\\ {\obj_{\V{LOC}}(\js{x},{\js{y}}|\protop:\nil,\js{w}:\nil,{\js{v}:4})}\\ \sep\ls\doteq\V{LS}\sep \true \end{array}\right\} \]
\[\{ \exists\V{L}\st\store_{\V{LS}}(|\js{x}:\undefined,\js{y}:4,\js{z}:5,\js{f}:\V{L},\js{v}:5) \sep\ls\doteq\V{LS}\sep \true \} \]

Another Example

a = {x:1};
with(a){ f = function(y){ return x } };
a = {x:2};
f(); 

What does the f() return?

Let's try it.
\[ \left\{ \begin{array}{c} \store_{\V{LS}}(|\js{a}:\_,\js{f}:\_) \sep\ls\doteq\V{LS} \end{array} \right\} \]
a = {x:1};
with(a){ f = function(y){ return x } };
a = {x:2};
f(); 
\[\left\{\begin{array}{c}\exists\V{L},\V{L2}\st\ \store_{\V{LS}}(|\js{a}:\V{L},\js{f}:\V{L2})\\ \sep \ls\doteq\V{LS} \sep \rv\doteq 1 \sep \true \end{array}\right\}\]
Object.prototype.f = function() { 
    return "Iz in your code, "+
	   "eatin your cheez" };
a = {x:1};
with(a){ f = function(y){ 
	    return x } };
a = {x:2};
f(); 
Try it?
\[ \left\{\begin{array}{c}\store_{\V{LS}}(|\js{a}:\_,\js{f}:\_)\sepish\\ \red{\obj_{\lop}(\js{f}|\protop:\nil)}\\ \sep\ls\doteq\V{LS}\end{array}\right\} \]
a = {x:1};
with(a){ f = function(y){ return x } };
a = {x:2};
f(); 
\[\left\{\begin{array}{c}\exists\V{L},\V{L2}\st\ \store_{\V{LS}}(\js{a}:\V{L},\js{f}:\V{L2})\\ \sep\ls\doteq\V{LS} \sep \rv\doteq 1 \sep \true \end{array}\right\}\]

Reasoning about JavaScript

We have:
robust reasoning about the emulated variable store
a strong soundness result using Maffeis et al.'s operational semantics
abstraction layers and simple examples
similar results about DOM Core Level 1
To Come:
reasoning about higher-order functions and complex eval (working with Charlton and Reus)
reasoning about automatic type conversion (depends on higher-order functions)
verification tools (Naudziuniene)
substantial examples

One last thing...

Remember this?

\[\left\{\begin{array}{c} \text{list}(x) \end{array}\right\}\]
revlist(x)
\[\left\{\begin{array}{c} \text{list}(x) \end{array}\right\}\]

Remember this?

\[ \left\{\begin{array}{c} \exists\V{L}\st \store_\ls(|\js{x}:L) \sep \text{list}(\V{L}) \\ \end{array}\right\} \]
revlist{x} 
\[ \left\{\begin{array}{c} \exists\V{L}\st \store_\ls(|\js{x}:L) \sep \text{list}(\V{L}) \\ \end{array}\right\} \]

Our Mantra

Easy to reason about simple code,
possible to reason about hard code.