% !TEX program = xelatex\documentclass[dvipsnames,14pt,t,xelatex,aspectratio=169,xcolor={table}]{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\\[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} \begin{center} \begin{tikzpicture} \node[drop shadow,fill=white,inner sep=0pt] {\footnotesize\rowcolors{1}{capri!10}{white} \begin{tabular}{|p{4.8cm}|p{4.8cm}|}\hline 1 Introduction, Languages & 6 While-Language \\ 2 Regular Expressions, Derivatives & 7 Compilation, JVM \\ 3 Automata, Regular Languages & 8 Compiling Functional Languages \\ 4 Lexing, Tokenising & \cellcolor{blue!50} 9 Optimisations \\ 5 Grammars, Parsing & 10 LLVM \\ \hline \end{tabular}% }; \end{tikzpicture} \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_3If_else_2: iload 0 ldc 1 isub iload 0 iload 1 imul invokestatic fact/fact/facT(II)IIf_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_24if_br_23: ret i32 1else_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_bricmp eq i32 %x, %y ; for equalicmp sle i32 %x, %y ; signed less or equalicmp slt i32 %x, %y ; signed less thanicmp 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 Expcase class If(a: BExp, e1: Exp, e2: Exp) extends Expcase class Write(e: Exp) extends Expcase class Var(s: String) extends Expcase class Num(i: Int) extends Expcase class Aop(o: String, a1: Exp, a2: Exp) extends Expcase class Sequence(e1: Exp, e2: Exp) extends Expcase 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 KExpabstract class KVal// K-Valuescase class KVar(s: String) extends KValcase class KNum(i: Int) extends KValcase class Kop(o: String, v1: KVal, v2: KVal) extends KValcase class KCall(o: String, vrs: List[KVal]) extends KValcase class KWrite(v: KVal) extends KVal// K-Expressionscase class KIf(x1: String, e1: KExp, e2: KExp) extends KExpcase class KLet(x: String, v: KVal, e: KExp) extends KExpcase class KReturn(v: KVal) extends KExp\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile,c]\frametitle{KLet}\begin{lstlisting}[language=LLVM]tmp0 = add 1 a tmp1 = mul b 5 tmp2 = add 3 tmp1 tmp3 = add tmp0 tmp2 \end{lstlisting}\begin{lstlisting}[language=LLVMIR] KLet tmp0 , add 1 a in KLet tmp1 , mul b 5 in KLet tmp2 , add 3 tmp1 in KLet tmp3 , add tmp0 tmp2 in ...\end{lstlisting}\begin{lstlisting}[language=Scala,numbers=none]case class KLet(x: String, e1: KVal, e2: KExp)\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[fragile,c]\frametitle{KLet}\begin{lstlisting}[language=LLVM]tmp0 = add 1 a tmp1 = mul b 5 tmp2 = add 3 tmp1 tmp3 = add tmp0 tmp2 \end{lstlisting}\begin{lstlisting}[language=LLVMIR] let tmp0 = add 1 a in let tmp1 = mul b 5 in let tmp2 = add 3 tmp1 in let tmp3 = add tmp0 tmp2 in ...\end{lstlisting}\begin{lstlisting}[language=Scala,numbers=none]case class KLet(x: String, e1: KVal, e2: 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\bigskipthe 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 = 010 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.llIntel: xorl %eax, %eaxARM: mov pc, lr\end{lstlisting}\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\begin{frame}[c]\large\bfUsing a compiler, \\how can you mount the\\ perfect attack against a system?\end{frame}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\mode<presentation>{\begin{frame}[c]{\large\bfWhat 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}\bigskipsimilarly\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 havehelp from the computer. `Program' is here to be understood to bequite 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 alsomany in LLVM (some of them highest-level critical)\bigskip\item about CompCert:\begin{bubble}[10.7cm]\small ``The striking thing about our CompCertresults is that the middle-end bugs we found in all othercompilers are absent. As of early 2011, the under-developmentversion of CompCert is the only compiler we have tested forwhich Csmith cannot find wrong-code errors. This is not forlack of trying: we have devoted about six CPU-years to thetask.'' \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 hardwarefaults.\bigskipThey 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}\medskipusing 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 ensurethey are bug free/correct?\pause\bigskip\item Very hard: Anything interesting about programs is equivalentto 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}?\bigskipProg.~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}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%