% !TEX program = xelatex+ −
\documentclass[dvipsnames,14pt,t]{beamer}+ −
\usepackage{../slides}+ −
\usepackage{../langs}+ −
\usepackage{../data}+ −
\usepackage{../graphics}+ −
\usepackage{../grammar}+ −
\usepackage{soul}+ −
\usepackage{mathpartir}+ −
\usetikzlibrary{shapes,arrows,shadows}+ −
+ −
% beamer stuff+ −
\renewcommand{\slidecaption}{CFL 09, King's College London}+ −
\newcommand{\bl}[1]{\textcolor{blue}{#1}} + −
+ −
+ −
\begin{document}+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[t]+ −
\frametitle{%+ −
\begin{tabular}{@ {}c@ {}}+ −
\\[-3mm]+ −
\LARGE Compilers and \\[-2mm] + −
\LARGE Formal Languages (9)\\[3mm] + −
\end{tabular}}+ −
+ −
\normalsize+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
Email: & christian.urban at kcl.ac.uk\\+ −
Office Hours: & Thursdays 12 -- 14\\+ −
Location: & N7.07 (North Wing, Bush House)\\+ −
Slides \& Progs: & KEATS (also homework is there)\\ + −
\end{tabular}+ −
\end{center}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c,fragile]+ −
\frametitle{The Fun Language}+ −
+ −
\footnotesize+ −
\begin{textblock}{13}(0.9,3)+ −
\begin{lstlisting}[]numbers=none]+ −
def fib(n) = if n == 0 then 0 + −
else if n == 1 then 1 + −
else fib(n - 1) + fib(n - 2);+ −
+ −
def fact(n) = if n == 0 then 1 else n * fact(n - 1);+ −
+ −
def ack(m, n) = if m == 0 then n + 1+ −
else if n == 0 then ack(m - 1, 1)+ −
else ack(m - 1, ack(m, n - 1));+ −
+ −
def gcd(a, b) = if b == 0 then a else gcd(b, a % b); + −
\end{lstlisting}+ −
\end{textblock}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c,fragile]+ −
\frametitle{Factorial Funct.~on the JVM}+ −
+ −
\begin{textblock}{7}(1,1.8)\footnotesize+ −
\begin{minipage}{6cm}+ −
\begin{lstlisting}[language=JVMIS,basicstyle=\ttfamily, numbers=none]+ −
.method public static facT(II)I + −
.limit locals 2+ −
.limit stack 6+ −
iload 0+ −
ldc 0+ −
if_icmpne If_else_2+ −
iload 1+ −
goto If_end_3+ −
If_else_2:+ −
iload 0+ −
ldc 1+ −
isub+ −
iload 0+ −
iload 1+ −
imul+ −
invokestatic fact/fact/facT(II)I+ −
If_end_3:+ −
ireturn+ −
.end method + −
\end{lstlisting}+ −
\end{minipage}+ −
\end{textblock}+ −
+ −
\begin{textblock}{7}(6,7)+ −
\begin{bubble}[7cm]\small+ −
\begin{lstlisting}[language=Lisp,+ −
basicstyle=\ttfamily, + −
numbers=none,+ −
xleftmargin=1mm,linebackgroundcolor=\color{cream}]+ −
def facT(n, acc) = + −
if n == 0 then acc + −
else facT(n - 1, n * acc);+ −
\end{lstlisting}+ −
\end{bubble}+ −
\end{textblock}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{LLVM}+ −
+ −
\begin{itemize}+ −
\item Chris Lattner, Vikram Adve (started in 2000)+ −
\item Apple hired Lattner in 2006+ −
\item modular architecture, LLVM-IR+ −
\item \texttt{lli} and \texttt{llc} + −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\tikzstyle{sensor}=[draw, fill=blue!20, text width=3.8em, line width=1mm,+ −
text centered, minimum height=2em,drop shadow]+ −
\tikzstyle{ann} = [above, text width=4em, text centered]+ −
\tikzstyle{sc} = [sensor, text width=7em, fill=red!20, + −
minimum height=6em, rounded corners, drop shadow,line width=1mm]+ −
+ −
\begin{frame}[fragile,c]+ −
\frametitle{LLVM: Overview}+ −
+ −
\begin{tikzpicture}+ −
% Validation Layer is the same except that there are a set of nodes and links which are added+ −
+ −
\path (0,0) node (IR) [sc] {\textbf{LLVM-IR}\\ Optimisations};+ −
\path (IR.west)+(-2.2,1.7) node (sou1) [sensor] {C++};+ −
\path (IR.west)+(-2.2,0.5) node (sou2)[sensor] {C};+ −
\path (IR.west)+(-2.2,-1.0) node (dots)[ann] {$\vdots$}; + −
\path (IR.west)+(-2.2,-1.8) node (sou3)[sensor] {Haskell}; + −
+ −
\path [draw,->,line width=1mm] (sou1.east) -- node [above] {} (IR.160);+ −
\path [draw,->,line width=1mm] (sou2.east) -- node [above] {} (IR.180);+ −
\path [draw,->,line width=1mm] (sou3.east) -- node [above] {} (IR.200);+ −
+ −
\path (IR.east)+(2.2,2.0) node (tar1)[sensor] {x86};+ −
\path (IR.east)+(2.2,0.8) node (tar2)[sensor] {ARM};+ −
\path (IR.east)+(2.2,-0.4) node (tar3)[sensor] {MIPS}; + −
\path (IR.east)+(2.2,-1.6) node (tar4)[sensor] {RISC}; + −
\path (IR.east)+(2.2,-2.8) node (tar5)[sensor] {Power PC};+ −
\path (IR.east)+(2.2,-4.2) node (dots2)[ann] {$\vdots$};+ −
+ −
\path [draw,<-,line width=1mm] (tar1.west) -- node [above] {} (IR.10);+ −
\path [draw,<-,line width=1mm] (tar2.west) -- node [above] {} (IR.5);+ −
\path [draw,<-,line width=1mm] (tar3.west) -- node [above] {} (IR.0);+ −
\path [draw,<-,line width=1mm] (tar4.west) -- node [above] {} (IR.-5);+ −
\path [draw,<-,line width=1mm] (tar5.west) -- node [above] {} (IR.-10);+ −
+ −
\end{tikzpicture}+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,t]+ −
\frametitle{LLVM-IR}+ −
\small+ −
+ −
\begin{textblock}{7.7}(8,11.4)+ −
\begin{bubble}[5cm]\small+ −
\begin{lstlisting}[language=Lisp,+ −
numbers=none,+ −
xleftmargin=1mm,linebackgroundcolor=\color{cream}]+ −
def fact(n) =+ −
if n == 0 then 1 + −
else n * fact(n - 1)+ −
\end{lstlisting}+ −
\end{bubble}+ −
\end{textblock}+ −
+ −
\begin{lstlisting}[language=LLVM,xleftmargin=-7mm]+ −
define i32 @fact (i32 %n) {+ −
%tmp_19 = icmp eq i32 %n, 0+ −
br i1 %tmp_19, label %if_br_23, label %else_br_24+ −
+ −
if_br_23:+ −
ret i32 1+ −
+ −
else_br_24:+ −
%tmp_21 = sub i32 %n, 1+ −
%tmp_22 = call i32 @fact (i32 %tmp_21)+ −
%tmp_20 = mul i32 %n, %tmp_22+ −
ret i32 %tmp_20+ −
}+ −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{LLVM Types}+ −
+ −
\tt+ −
\begin{center}+ −
\begin{tabular}{ll}+ −
boolean & i1 \\+ −
byte & i8 \\+ −
short & i16\\+ −
char & i16\\+ −
integer & i32\\+ −
long & i64\\+ −
float & float\\+ −
double & double\\+ −
*\_ & pointer to \\+ −
**\_ & pointer to a pointer to\\+ −
\mbox{}[\_] & arrays of\\+ −
\end{tabular}+ −
\end{center}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{LLVM-IR Instructions}+ −
\small+ −
+ −
\begin{lstlisting}[language=LLVM,xleftmargin=0mm]+ −
br i1 %var, label %if_br, label %else_br+ −
+ −
icmp eq i32 %x, %y ; for equal+ −
icmp sle i32 %x, %y ; signed less or equal+ −
icmp slt i32 %x, %y ; signed less than+ −
icmp ult i32 %x, %y ; unsigned less than + −
+ −
%var = call i32 @foo(...args...)+ −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{SSA Format}+ −
+ −
\bl{$(1 + a) + (3 + (b * 5))$}\bigskip\bigskip+ −
+ −
\begin{lstlisting}[language=LLVM]+ −
tmp0 = add 1 a + −
tmp1 = mul b 5 + −
tmp2 = add 3 tmp1 + −
tmp3 = add tmp0 tmp2 + −
\end{lstlisting}\bigskip\bigskip+ −
+ −
\hfill Static Single Assignment+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{Abstract Syntax Trees}+ −
\footnotesize+ −
+ −
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]+ −
// Fun language (expressions)+ −
abstract class Exp + −
abstract class BExp + −
+ −
case class Call(name: String, args: List[Exp]) extends Exp+ −
case class If(a: BExp, e1: Exp, e2: Exp) extends Exp+ −
case class Write(e: Exp) extends Exp+ −
case class Var(s: String) extends Exp+ −
case class Num(i: Int) extends Exp+ −
case class Aop(o: String, a1: Exp, a2: Exp) extends Exp+ −
case class Sequence(e1: Exp, e2: Exp) extends Exp+ −
case class Bop(o: String, a1: Exp, a2: Exp) extends BExp + −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{K-(Intermediate)Language}+ −
\footnotesize+ −
+ −
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]+ −
abstract class KExp+ −
abstract class KVal+ −
+ −
// K-Values+ −
case class KVar(s: String) extends KVal+ −
case class KNum(i: Int) extends KVal+ −
case class Kop(o: String, v1: KVal, v2: KVal) extends KVal+ −
case class KCall(o: String, vrs: List[KVal]) extends KVal+ −
case class KWrite(v: KVal) extends KVal+ −
+ −
// K-Expressions+ −
case class KIf(x1: String, e1: KExp, e2: KExp) extends KExp+ −
case class KLet(x: String, v: KVal, e: KExp) extends KExp+ −
case class KReturn(v: KVal) extends KExp+ −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{CPS-Translation}+ −
\small+ −
+ −
\begin{lstlisting}[language=Scala,numbers=none]+ −
def CPS(e: Exp)(k: KVal => KExp) : KExp = + −
e match { ... }+ −
\end{lstlisting}+ −
\bigskip\bigskip+ −
+ −
the continuation \texttt{k} can be thought of:\medskip+ −
+ −
\small+ −
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]+ −
let tmp0 = add 1 a in + −
let tmp1 = mul (*@$\Box$@*) 5 in + −
let tmp2 = add 3 tmp1 in + −
let tmp3 = add tmp0 tmp2 in+ −
KReturn tmp3 + −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{CPS-Translation}+ −
\small+ −
+ −
\begin{lstlisting}[language=Scala,numbers=none]+ −
def CPS(e: Exp)(k: KVal => KExp) : KExp = + −
e match { + −
case Var(s) => k(KVar(s)) + −
case Num(i) => k(KNum(i))+ −
...+ −
}+ −
\end{lstlisting}+ −
\bigskip\bigskip+ −
+ −
\small+ −
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]+ −
let tmp0 = add 1 a in + −
let tmp1 = mul (*@$\Box$@*) 5 in + −
let tmp2 = add 3 tmp1 in + −
let tmp3 = add tmp0 tmp2 in+ −
KReturn tmp3 + −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{CPS-Translation}+ −
\small+ −
+ −
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]+ −
def CPS(e: Exp)(k: KVal => KExp) : KExp = e match { + −
case Aop(o, e1, e2) => {+ −
val z = Fresh("tmp")+ −
CPS(e1)(y1 => + −
CPS(e2)(y2 => + −
KLet(z, Kop(o, y1, y2), k(KVar(z)))))+ −
} ...+ −
}+ −
\end{lstlisting}+ −
\mbox{}\\[-8mm]%+ −
%+ −
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]+ −
...+ −
let z = op (*@$\Box_{y_1}$@*) (*@$\Box_{y_2}$@*)+ −
let tmp0 = add 1 a in + −
let tmp1 = mul (*@$\Box\!\!\!\!\raisebox{0.6mm}{\alert{\texttt{z}}}$@*) 5 in + −
let tmp2 = add 3 tmp1 in + −
let tmp3 = add tmp0 tmp2 in+ −
KReturn tmp3 + −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{CPS-Translation}+ −
\small+ −
+ −
\begin{lstlisting}[language=Scala,numbers=none]+ −
def CPS(e: Exp)(k: KVal => KExp) : KExp = + −
e match { + −
case Sequence(e1, e2) => + −
CPS(e1)(_ => CPS(e2)(y2 => k(y2)))+ −
...+ −
}+ −
\end{lstlisting}+ −
\bigskip+ −
+ −
\small+ −
\begin{lstlisting}[language=LLVMIR,numbers=none,xleftmargin=30mm,escapeinside={(*@}{@*)}]+ −
let tmp0 = add 1 a in + −
let tmp1 = mul (*@$\Box$@*) 5 in + −
let tmp2 = add 3 tmp1 in + −
let tmp3 = add tmp0 tmp2 in+ −
KReturn tmp3 + −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[fragile,c]+ −
\frametitle{CPS-Translation}+ −
\small+ −
+ −
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-3mm]+ −
def CPS(e: Exp)(k: KVal => KExp) : KExp = + −
e match { + −
...+ −
case If(Bop(o, b1, b2), e1, e2) => {+ −
val z = Fresh("tmp")+ −
CPS(b1)(y1 => + −
CPS(b2)(y2 => + −
KLet(z, Kop(o, y1, y2), + −
KIf(z, CPS(e1)(k), CPS(e2)(k)))))+ −
}+ −
...+ −
}+ −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c,fragile]+ −
\frametitle{The Basic Language, 1980+}+ −
+ −
\begin{lstlisting}[language={[Visual]Basic},numbers=none]+ −
5 LET S = 0+ −
10 INPUT V + −
20 PRINT "Input number"+ −
30 IF N = 0 THEN GOTO 99 + −
40 FOR I = 1 TO N + −
45 LET S = S + V(I) + −
50 NEXT I + −
60 PRINT S/N + −
70 GOTO 5 + −
99 END+ −
\end{lstlisting}+ −
+ −
\hfill ``Spaghetti Code''+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c,fragile]+ −
\frametitle{Target Specific ASM}+ −
+ −
\begin{lstlisting}[language={},numbers=none]+ −
llc -march=x86-64 fact.ll + −
llc -march=arm fact.ll+ −
+ −
+ −
Intel: xorl %eax, %eax+ −
ARM: mov pc, lr+ −
\end{lstlisting}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
+ −
\large\bf+ −
Using a compiler, \\+ −
how can you mount the\\ + −
perfect attack against a system?+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}[c]+ −
+ −
{\large\bf+ −
What is a \alert{perfect} attack?}\bigskip+ −
+ −
\begin{enumerate}+ −
\item you can potentially completely take over a target system+ −
\item your attack is (nearly) undetectable+ −
\item the victim has (almost) no chance to recover+ −
\end{enumerate}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}[c]+ −
+ −
+ −
\begin{center}+ −
\begin{tikzpicture}[scale=1]+ −
+ −
\onslide<1->{+ −
\node (A) at (0,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=17mm] {};+ −
\node [below right] at (A.north west) {\footnotesize\begin{tabular}{@{}l@{}}+ −
\only<1,2>{clean}\only<3->{\alert{hacked}}\\compiler\end{tabular}};}+ −
+ −
+ −
\onslide<2->{+ −
\node (B) at (-2,2) [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};+ −
\node [below right] at (B.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(src)\end{tabular}};+ −
+ −
\node (C) at (2,2) [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};+ −
\node [below right] at (C.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(bin)\end{tabular}};+ −
+ −
\draw[->, line width=2mm] (B) -- (C);+ −
}+ −
+ −
\onslide<3->{\node [above left=-1.5mm] at (C.south east) {\footnotesize \alert{$\blacksquare$}};}+ −
+ −
\end{tikzpicture}+ −
\end{center}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}[c]+ −
+ −
\begin{center}+ −
\begin{tikzpicture}[scale=1]+ −
+ −
\onslide<1->{+ −
\node (A) at (0,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};+ −
\node [below right] at (A.north west) {\small V0.01};+ −
\node [below right] (A1) at (A.south west) {\small Scala};+ −
\node [below right] (A1) at (A1.south west) {\small\textcolor{gray}{host language}};+ −
\node [above right] at (A.north west) {my compiler (src)};}+ −
+ −
\onslide<2->{+ −
\node (B) at (1.8,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};+ −
\node [below right] at (B.north west) {\small V0.02};+ −
\node [below right] at (B.south west) {\small Scala};+ −
\node at (3,0) {\ldots};+ −
+ −
\node (C) at (5,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};+ −
\node [below right] at (C.north west) {\small V1.00};+ −
\node [below right] at (C.south west) {\small Scala};}+ −
+ −
\onslide<3->{+ −
\node (D) at (6.8,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};+ −
\node [below right] at (D.north west) {\small V1.00};+ −
+ −
\node (E) at (6.8,2) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};+ −
\node [below right] at (E.north west) {\small V1.01};}+ −
+ −
\onslide<4->{+ −
\node (F) at (8.6,0) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};+ −
\node [below right] at (F.north west) {\small V1.01};+ −
+ −
\node (G) at (8.6,2) [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};+ −
\node [below right] at (G.north west) {\small V1.02};+ −
\node at (9.8,0) {\ldots};+ −
\node at (9.8,2) {\ldots};+ −
\node at (8,-2) {\textcolor{gray}{\begin{tabular}{@{}l@{}}no host language\\needed\end{tabular}}};+ −
}+ −
+ −
\end{tikzpicture}+ −
\end{center}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\mode<presentation>{+ −
\begin{frame}<1-3>+ −
\frametitle{\LARGE\begin{tabular}{c}Hacking Compilers + −
\end{tabular}}+ −
+ −
%Why is it so paramount to have a small trusted code base (TCB)?+ −
\bigskip\bigskip+ −
+ −
\begin{columns}+ −
\begin{column}{2.7cm}+ −
\begin{minipage}{2.5cm}%+ −
\begin{tabular}{c@ {}}+ −
\includegraphics[scale=0.2]{../pics/ken-thompson.jpg}\\[-1.8mm]+ −
\footnotesize Ken Thompson\\[-1.8mm]+ −
\footnotesize Turing Award, 1983\\+ −
\end{tabular}+ −
\end{minipage}+ −
\end{column}+ −
\begin{column}{9cm}+ −
\begin{tabular}{l@ {\hspace{1mm}}p{8cm}}+ −
+ −
& Ken Thompson showed how to hide a Trojan Horse in a + −
compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm]+ −
+ −
& No amount of source level verification will protect + −
you from such Thompson-hacks.\\[2mm]+ −
+ −
\end{tabular}+ −
\end{column}+ −
\end{columns}+ −
+ −
\only<2>{+ −
\begin{textblock}{6}(4,2)+ −
\begin{tikzpicture}+ −
\draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] + −
{\normalsize+ −
\begin{minipage}{8cm}+ −
\begin{quote}+ −
\includegraphics[scale=0.05]{../pics/evil.png}+ −
\begin{enumerate}+ −
\item[1)] Assume you ship the compiler as binary and also with sources.+ −
\item[2)] Make the compiler aware when it compiles itself.+ −
\item[3)] Add the Trojan horse.+ −
\item[4)] Compile.+ −
\item[5)] Delete Trojan horse from the sources of the compiler.+ −
\item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{}+ −
\end{enumerate}+ −
\end{quote}+ −
\end{minipage}};+ −
\end{tikzpicture}+ −
\end{textblock}}+ −
+ −
\end{frame}}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Dijkstra on Testing}+ −
+ −
\begin{bubble}[10cm]+ −
``Program testing can be a very effective way to show the+ −
presence of bugs, but it is hopelessly inadequate for showing+ −
their absence.''+ −
\end{bubble}\bigskip+ −
+ −
\small+ −
What is good about compilers: the either seem to work,+ −
or go horribly wrong (most of the time).+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{\Large Proving Programs to be Correct}+ −
+ −
\begin{bubble}[10cm]+ −
\small+ −
{\bf Theorem:} There are infinitely many prime + −
numbers.\medskip\\+ −
+ −
{\bf Proof} \ldots\\+ −
\end{bubble}\bigskip+ −
+ −
+ −
similarly\bigskip+ −
+ −
\begin{bubble}[10cm]+ −
\small+ −
{\bf Theorem:} The program is doing what + −
it is supposed to be doing.\medskip+ −
+ −
{\bf Long, long proof} \ldots\\+ −
\end{bubble}\bigskip\medskip+ −
+ −
\small This can be a gigantic proof. The only hope is to have+ −
help from the computer. `Program' is here to be understood to be+ −
quite general (compiler, OS, \ldots).+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
\begin{frame}[c]+ −
\frametitle{Can This Be Done?}+ −
+ −
\begin{itemize}+ −
\item in 2008, verification of a small C-compiler+ −
\begin{itemize}+ −
\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''+ −
\item is as good as \texttt{gcc -O1}, but much, much less buggy + −
\end{itemize}+ −
\end{itemize}+ −
+ −
\begin{center}+ −
\includegraphics[scale=0.12]{../pics/compcert.png}+ −
\end{center}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
\begin{frame}[t]+ −
\frametitle{Fuzzy Testing C-Compilers}+ −
+ −
\begin{itemize}+ −
\item tested GCC, LLVM and others by randomly generating + −
C-programs+ −
\item found more than 300 bugs in GCC and also+ −
many in LLVM (some of them highest-level critical)\bigskip+ −
\item about CompCert:+ −
+ −
\begin{bubble}[10.7cm]\small ``The striking thing about our CompCert+ −
results is that the middle-end bugs we found in all other+ −
compilers are absent. As of early 2011, the under-development+ −
version of CompCert is the only compiler we have tested for+ −
which Csmith cannot find wrong-code errors. This is not for+ −
lack of trying: we have devoted about six CPU-years to the+ −
task.'' + −
\end{bubble} + −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
\begin{frame}[c]+ −
\frametitle{Next Week}+ −
+ −
\begin{itemize}+ −
\item Revision Lecture\medskip+ −
\item How many strings are in $\bl{L(a^*)}$?\pause\medskip+ −
\item How many strings are in $\bl{L((a + b)^*)}$?\\ Are there more than+ −
in $\bl{L(a^*)}$?+ −
\end{itemize}+ −
+ −
+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
+ −
+ −
\end{document}+ −
+ −
%%% Local Variables: + −
%%% mode: latex+ −
%%% TeX-master: t+ −
%%% End: + −
+ −
+ −
+ −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
+ −
\begin{center}+ −
\includegraphics[scale=0.6]{../pics/bridge-limits.png}+ −
\end{center}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Compilers \& Boeings 777}+ −
+ −
First flight in 1994. They want to achieve triple redundancy in hardware+ −
faults.\bigskip+ −
+ −
They compile 1 Ada program to\medskip+ −
+ −
\begin{itemize}+ −
\item Intel 80486+ −
\item Motorola 68040 (old Macintosh's)+ −
\item AMD 29050 (RISC chips used often in laser printers)+ −
\end{itemize}\medskip+ −
+ −
using 3 independent compilers.\bigskip\pause+ −
+ −
\small Airbus uses C and static analysers. Recently started using CompCert.+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{Goal}+ −
+ −
Remember the Bridges example?+ −
+ −
\begin{itemize}+ −
\item Can we look at our programs and somehow ensure+ −
they are bug free/correct?\pause\bigskip+ −
+ −
\item Very hard: Anything interesting about programs is equivalent+ −
to the Halting Problem, which is undecidable.\pause\bigskip+ −
+ −
\item \alert{Solution:} We avoid this ``minor'' obstacle by+ −
being as close as possible of deciding the halting+ −
problem, without actually deciding the halting problem.+ −
\small$\quad\Rightarrow$ yes, no, don't know (static analysis)+ −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{What is Static Analysis?}+ −
+ −
\begin{center}+ −
\includegraphics[scale=0.4]{../pics/state.png}+ −
\end{center}+ −
+ −
\begin{itemize}+ −
\item depending on some initial input, a program + −
(behaviour) will ``develop'' over time.+ −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{What is Static Analysis?}+ −
+ −
\begin{center}+ −
\includegraphics[scale=0.4]{../pics/state2.png}+ −
\end{center}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{What is Static Analysis?}+ −
+ −
\begin{center}+ −
\includegraphics[scale=0.4]{../pics/state3.jpg}+ −
\end{center}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{What is Static Analysis?}+ −
+ −
\begin{center}+ −
\includegraphics[scale=0.4]{../pics/state4.jpg}+ −
\end{center}+ −
+ −
\begin{itemize}+ −
\item to be avoided+ −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{What is Static Analysis?}+ −
+ −
\begin{center}+ −
\includegraphics[scale=0.4]{../pics/state5.png}+ −
\end{center}+ −
+ −
\begin{itemize}+ −
\item this needs more work+ −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c]+ −
\frametitle{What is Static Analysis?}+ −
+ −
\begin{center}+ −
\includegraphics[scale=0.4]{../pics/state6.png}+ −
\end{center}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c,fragile]+ −
\frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]+ −
Are Vars Definitely Initialised?\end{tabular}}+ −
+ −
Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskip+ −
+ −
Prog.~1:\\+ −
\begin{lstlisting}[numbers=none,+ −
basicstyle=\ttfamily,+ −
language=While,xleftmargin=3mm]+ −
if x < 1 then y := x else y := x + 1;+ −
y := y + 1+ −
\end{lstlisting}\medskip + −
+ −
Prog.~2:\\+ −
\begin{lstlisting}[numbers=none,+ −
basicstyle=\ttfamily,+ −
language=While,xleftmargin=3mm]+ −
if x < x then y := y + 1 else y := x;+ −
y := y + 1+ −
\end{lstlisting} + −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c,fragile]+ −
\frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]+ −
Are Vars Definitely Initialised?\end{tabular}}+ −
+ −
What should the rules be for deciding when a+ −
variable is initialised?\bigskip\pause+ −
+ −
\begin{itemize}+ −
\item variable \texttt{x} is definitely initialized after+ −
\texttt{skip}\\+ −
iff \texttt{x} is definitely initialized before \texttt{skip}.+ −
\end{itemize}+ −
+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+ −
\begin{frame}[c,fragile]+ −
% \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]+ −
% Are Vars Definitely Initialised?\end{tabular}}+ −
+ −
$\bl{A}$ is the set of definitely defined variables:+ −
+ −
\begin{center}+ −
\begin{tabular}{c}+ −
\bl{\infer{\mbox{}}{A\triangleright\texttt{skip}\triangleright{}A}}\qquad+ −
\bl{\infer{vars(a) \subseteq A}{A\triangleright+ −
(\texttt{x\,:=\,a})\triangleright\{x\}\cup A}}+ −
\medskip\\\pause+ −
+ −
\bl{\infer{A_1\triangleright{}s_1\triangleright{}A_2+ −
\quad A_2\triangleright{}s_2\triangleright{}A_3}+ −
{A_1\triangleright{}(s_1 ; s_2)\triangleright{}A_3}}+ −
\medskip\\\pause+ −
+ −
\bl{\infer{vars(b)\subseteq A\quad A\triangleright{}s_1\triangleright{}A_1+ −
\quad A\triangleright{}s_2\triangleright{}A_2}+ −
{A\triangleright(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\triangleright{}A_1\cap A_2}}+ −
\medskip\\\pause+ −
+ −
\bl{\infer{vars(b)\subseteq A\quad A\triangleright{}s\triangleright{}A'}+ −
{A\triangleright(\texttt{while}\;b\;\texttt{do}\;s)\triangleright{}A}}\pause+ −
\end{tabular} + −
\end{center}+ −
+ −
\hfill we start with $\bl{A = \{\}}$+ −
\end{frame}+ −
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + −
+ −