diff -r e33545bb2eba -r 7ec1bdb670ba slides/slides09.tex
--- a/slides/slides09.tex	Tue Nov 27 00:45:26 2018 +0000
+++ b/slides/slides09.tex	Tue Nov 27 01:15:54 2018 +0000
@@ -5,7 +5,7 @@
 \usepackage{../graphics}
 \usepackage{../grammar}
 \usepackage{soul}
-
+\usepackage{mathpartir}
 
 % beamer stuff
 \renewcommand{\slidecaption}{CFL 09, King's College London}
@@ -159,6 +159,376 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\mode<presentation>{
+\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]
+
+  \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\;\texttt{skip}\;A}}\qquad
+  \bl{\infer{vars(a) \subseteq A}{A\;\;(\texttt{x\,:=\,a})\;\;\{x\}\cup A}}
+  \medskip\\\pause
+
+  \bl{\infer{A_1\;s_1\;A_2\quad A_2\;s_2\;A_3}{A_1\;(s_1 ; s_2)\;A_3}}
+  \medskip\\\pause
+  
+  \bl{\infer{vars(b)\subseteq A\quad A\;s_1\;A_1\quad A\;s_2\;A_2}
+  {A\;(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\;A_1\cap A_2}}
+  \medskip\\\pause
+
+  \bl{\infer{vars(b)\subseteq A\quad A\;s\;A'}
+  {A\;(\texttt{while}\;b\;\texttt{do}\;s)\;A}}\pause
+\end{tabular}  
+\end{center}
+
+\hfill we start with $\bl{A = \{\}}$
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \begin{frame}[c]
@@ -229,7 +599,7 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-\begin{frame}[c]
+\begin{frame}[t]
 \frametitle{Fuzzy Testing C-Compilers}
 
 \begin{itemize}
@@ -239,7 +609,7 @@
 many in LLVM (some of them highest-level critical)\bigskip
 \item about CompCert:
 
-\begin{bubble}[10cm]\small ``The striking thing about our 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