\documentclass[dvipsnames,14pt,t]{beamer}+
−
\usepackage{../slides}+
−
\usepackage{../langs}+
−
\usepackage{../data}+
−
\usepackage{../graphics}+
−
\usepackage{../grammar}+
−
\usepackage{soul}+
−
\usepackage{mathpartir}+
−
+
−
% 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: & N\liningnums{7.07} (North Wing, Bush House)\\+
−
  Slides: & KEATS (also homework is there)\\+
−
  \end{tabular}+
−
  \end{center}+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
+
−
 +
−
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[t]+
−
\frametitle{While Language}+
−
  +
−
\begin{center}+
−
\bl{\begin{tabular}{@{}lcl@{}}+
−
\\[-12mm]        +
−
\meta{Stmt} & $::=$ &  $\texttt{skip}$\\+
−
              & $|$ & \textit{Id}\;\texttt{:=}\;\meta{AExp}\\+
−
              & $|$ & \texttt{if}\; \meta{BExp} \;\texttt{then}\; \meta{Block} \;\texttt{else}\; \meta{Block}\\+
−
              & $|$ & \texttt{while}\; \meta{BExp} \;\texttt{do}\; \meta{Block}\\+
−
              & $|$ & \texttt{read}\;\textit{Id}\\+
−
              & $|$ & \texttt{write}\;\textit{Id}\\+
−
              & $|$ & \texttt{write}\;\textit{String}\medskip\\+
−
\meta{Stmts} & $::=$ &  \meta{Stmt} \;\texttt{;}\; \meta{Stmts} $|$  \meta{Stmt}\medskip\\+
−
\meta{Block} & $::=$ &  \texttt{\{}\,\meta{Stmts}\,\texttt{\}} $|$ \meta{Stmt}\medskip\\+
−
\meta{AExp} & $::=$ & \ldots\\+
−
\meta{BExp} & $::=$ & \ldots\\+
−
\end{tabular}}+
−
\end{center}+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c]+
−
\frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}}+
−
+
−
\mbox{}\\[-18mm]\mbox{}+
−
+
−
{\lstset{language=While}\fontsize{10}{12}\selectfont+
−
\texttt{\lstinputlisting{../progs/fib.while}}}+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c,fragile]+
−
\frametitle{BF***}+
−
+
−
some big array, say \texttt{a}; 7 (8) instructions:+
−
+
−
\begin{itemize}+
−
\item \texttt{>} move \texttt{ptr++}+
−
\item \texttt{<} move \texttt{ptr-{}-}+
−
\item \texttt{+} add \texttt{a[ptr]++}+
−
\item \texttt{-} subtract \texttt{a[ptr]-{}-}+
−
\item \texttt{.} print out \texttt{a[ptr]} as ASCII+
−
\item \texttt{[} if \texttt{a[ptr] == 0} jump just after the corresponding \texttt{]}; otherwise \texttt{ptr++}+
−
\item \texttt{]} if \texttt{a[ptr] != 0} jump just after the corresponding \texttt{[}; otherwise \texttt{ptr++}+
−
+
−
\end{itemize}  +
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c,fragile]+
−
\frametitle{Arrays in While}+
−
+
−
\begin{itemize}+
−
\item \texttt{new arr[15000]}\medskip +
−
\item \texttt{x := 3 + arr[3 + y]}\medskip +
−
\item \texttt{arr[42 * n] := ...}+
−
\end{itemize}  +
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c,fragile]+
−
\frametitle{New Arrays}+
−
+
−
\begin{lstlisting}[mathescape,numbers=none,language=While]+
−
  new arr[number]+
−
\end{lstlisting}\bigskip\bigskip+
−
+
−
\begin{lstlisting}[mathescape,numbers=none,language=While]+
−
  ldc number+
−
  newarray int+
−
  astore loc_var+
−
\end{lstlisting}+
−
+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c,fragile]+
−
\frametitle{Array Update}+
−
+
−
\begin{lstlisting}[mathescape,numbers=none,language=While]+
−
  arr[...] := +
−
\end{lstlisting}\bigskip\bigskip+
−
+
−
\begin{lstlisting}[mathescape,numbers=none,language=While]+
−
  aload loc_var+
−
  index_aexp+
−
  value_aexp+
−
  iastore+
−
\end{lstlisting}+
−
+
−
+
−
\end{frame}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
\begin{frame}[c,fragile]+
−
\frametitle{Array Lookup in AExp}+
−
+
−
\begin{lstlisting}[mathescape,numbers=none,language=While]+
−
  ...arr[...]... +
−
\end{lstlisting}\bigskip\bigskip+
−
+
−
\begin{lstlisting}[mathescape,numbers=none,language=While]+
−
  aload loc_var+
−
  index_aexp+
−
  iaload+
−
\end{lstlisting}+
−
+
−
+
−
\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\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}+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  +
−
+
−
+
−
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%+
−
  \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: +
−
+
−