--- 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