162 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   163 \mode<presentation>{

   164 \begin{frame}[c]

   165 

   166 \large\bf

   167 Using a compiler, \\how can you mount the\\ perfect attack against a system?

   168 

   169 \end{frame}}

   170 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   171 

   172 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   173 \mode<presentation>{

   174 \begin{frame}[c]

   175 

   176 {\large\bf

   177 What is a \alert{perfect} attack?}\bigskip

   178 

   179 \begin{enumerate}

   180 \item you can potentially completely take over a target system

   181 \item your attack is (nearly) undetectable

   182 \item the victim has (almost) no chance to recover

   183 \end{enumerate}

   184 

   185 \end{frame}}

   186 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   187 

   188 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   189 \mode<presentation>{

   190 \begin{frame}[c]

   191 

   192 

   193   \begin{center}

   194   \begin{tikzpicture}[scale=1]

   195   

   196   \onslide<1->{

   197   \node (A) at (0,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=17mm] {};

   198   \node [below right] at (A.north west) {\footnotesize\begin{tabular}{@{}l@{}}

   199   \only<1,2>{clean}\only<3->{\alert{hacked}}\\compiler\end{tabular}};}

   200 

   201 

   202   \onslide<2->{

   203   \node (B) at (-2,2)  [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};

   204   \node [below right] at (B.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(src)\end{tabular}};

   205   

   206   \node (C) at (2,2)  [draw=black, rectangle, very thick, minimum height=10mm, minimum width=12mm] {};

   207   \node [below right] at (C.north west) {\footnotesize\begin{tabular}{@{}l@{}}login\\(bin)\end{tabular}};

   208 

   209   \draw[->, line width=2mm] (B) -- (C);

   210   }

   211   

   212  \onslide<3->{\node [above left=-1.5mm] at (C.south east) {\footnotesize \alert{$\blacksquare$}};}

   213 

   214   \end{tikzpicture}

   215   \end{center}

   216 

   217 \end{frame}}

   218 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   219 

   220 

   221 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   222 \mode<presentation>{

   223 \begin{frame}[c]

   224 

   225   \begin{center}

   226   \begin{tikzpicture}[scale=1]

   227   

   228   \onslide<1->{

   229   \node (A) at (0,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};

   230   \node [below right] at (A.north west) {\small V0.01};

   231   \node [below right] (A1) at (A.south west) {\small Scala};

   232   \node [below right] (A1) at (A1.south west) {\small\textcolor{gray}{host language}};

   233   \node [above right] at (A.north west) {my compiler (src)};}

   234 

   235   \onslide<2->{

   236   \node (B) at (1.8,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};

   237   \node [below right] at (B.north west) {\small V0.02};

   238   \node [below right] at (B.south west) {\small Scala};

   239   \node at (3,0) {\ldots};

   240 

   241   \node (C) at (5,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};

   242   \node [below right] at (C.north west) {\small V1.00};

   243   \node [below right] at (C.south west) {\small Scala};}

   244 

   245   \onslide<3->{

   246   \node (D) at (6.8,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};

   247   \node [below right] at (D.north west) {\small V1.00};

   248 

   249   \node (E) at (6.8,2)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};

   250   \node [below right] at (E.north west) {\small V1.01};}

   251   

   252   \onslide<4->{

   253   \node (F) at (8.6,0)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};

   254   \node [below right] at (F.north west) {\small V1.01};

   255 

   256   \node (G) at (8.6,2)  [draw=black, rectangle, very thick, minimum height=18mm, minimum width=14mm] {};

   257   \node [below right] at (G.north west) {\small V1.02};

   258   \node at (9.8,0) {\ldots};

   259   \node at (9.8,2) {\ldots};

   260   \node at (8,-2) {\textcolor{gray}{\begin{tabular}{@{}l@{}}no host language\\needed\end{tabular}}};

   261   }

   262   

   263   \end{tikzpicture}

   264   \end{center}

   265 

   266 \end{frame}}

   267 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

   268 

   269 

   270   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   271   \mode<presentation>{

   272   \begin{frame}<1-3>

   273   \frametitle{\LARGE\begin{tabular}{c}Hacking Compilers 

   274   \end{tabular}}

   275   

   276   %Why is it so paramount to have a small trusted code base (TCB)?

   277   \bigskip\bigskip

   278 

   279   \begin{columns}

   280   \begin{column}{2.7cm}

   281   \begin{minipage}{2.5cm}%

   282   \begin{tabular}{c@ {}}

   283   \includegraphics[scale=0.2]{../pics/ken-thompson.jpg}\\[-1.8mm]

   284   \footnotesize Ken Thompson\\[-1.8mm]

   285   \footnotesize Turing Award, 1983\\

   286   \end{tabular}

   287   \end{minipage}

   288   \end{column}

   289   \begin{column}{9cm}

   290   \begin{tabular}{l@ {\hspace{1mm}}p{8cm}}

   291  

   292   & Ken Thompson showed how to hide a Trojan Horse in a 

   293   compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm]

   294   

   295   & No amount of source level verification will protect 

   296   you from such Thompson-hacks.\\[2mm]

   297 

   298   \end{tabular}

   299   \end{column}

   300   \end{columns}

   301 

   302   \only<2>{

   303   \begin{textblock}{6}(4,2)

   304   \begin{tikzpicture}

   305   \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   306   {\normalsize

   307   \begin{minipage}{8cm}

   308   \begin{quote}

   309   \includegraphics[scale=0.05]{../pics/evil.png}

   310   \begin{enumerate}

   311   \item[1)] Assume you ship the compiler as binary and also with sources.

   312   \item[2)] Make the compiler aware when it compiles itself.

   313   \item[3)] Add the Trojan horse.

   314   \item[4)] Compile.

   315   \item[5)] Delete Trojan horse from the sources of the compiler.

   316   \item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{}

   317   \end{enumerate}

   318   \end{quote}

   319   \end{minipage}};

   320   \end{tikzpicture}

   321   \end{textblock}}

   322 

   323   \end{frame}}

   324   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   325 

   326 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   327   \begin{frame}[c]

   328 

   329   \begin{center}

   330   \includegraphics[scale=0.6]{../pics/bridge-limits.png}

   331   \end{center}

   332 

   333   \end{frame}

   334 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   335 

   336 

   337 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   338 \begin{frame}[c]

   339 \frametitle{Compilers \& Boeings 777}

   340 

   341 First flight in 1994. They want to achieve triple redundancy in hardware

   342 faults.\bigskip

   343 

   344 They compile 1 Ada program to\medskip

   345 

   346 \begin{itemize}

   347 \item Intel 80486

   348 \item Motorola 68040 (old Macintosh's)

   349 \item AMD 29050 (RISC chips used often in laser printers)

   350 \end{itemize}\medskip

   351 

   352 using 3 independent compilers.\bigskip\pause

   353 

   354 \small Airbus uses C and static analysers. Recently started using CompCert.

   355 

   356 \end{frame}

   357 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   358 

   359 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   360 \begin{frame}[c]

   361 \frametitle{Goal}

   362 

   363 Remember the Bridges example?

   364 

   365 \begin{itemize}

   366 \item Can we look at our programs and somehow ensure

   367 they are bug free/correct?\pause\bigskip

   368 

   369 \item Very hard: Anything interesting about programs is equivalent

   370 to the Halting Problem, which is undecidable.\pause\bigskip

   371 

   372 \item \alert{Solution:} We avoid this ``minor'' obstacle by

   373       being as close as possible of deciding the halting

   374       problem, without actually deciding the halting problem.

   375       \small$\quad\Rightarrow$ yes, no, don't know (static analysis)

   376 \end{itemize}

   377 

   378 \end{frame}

   379 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

   380 

   381 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   382   \begin{frame}[c]

   383   \frametitle{What is Static Analysis?}

   384 

   385   \begin{center}

   386   \includegraphics[scale=0.4]{../pics/state.png}

   387   \end{center}

   388   

   389   \begin{itemize}

   390   \item depending on some initial input, a program 

   391   (behaviour) will ``develop'' over time.

   392   \end{itemize}

   393 

   394   \end{frame}

   395 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   396 

   397 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   398   \begin{frame}[c]

   399   \frametitle{What is Static Analysis?}

   400 

   401   \begin{center}

   402   \includegraphics[scale=0.4]{../pics/state2.png}

   403   \end{center}

   404 

   405   \end{frame}

   406 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   407 

   408 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   409   \begin{frame}[c]

   410   \frametitle{What is Static Analysis?}

   411 

   412   \begin{center}

   413   \includegraphics[scale=0.4]{../pics/state3.jpg}

   414   \end{center}

   415 

   416   \end{frame}

   417 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   418 

   419 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   420   \begin{frame}[c]

   421   \frametitle{What is Static Analysis?}

   422 

   423   \begin{center}

   424   \includegraphics[scale=0.4]{../pics/state4.jpg}

   425   \end{center}

   426 

   427   \begin{itemize}

   428   \item to be avoided

   429   \end{itemize}

   430 

   431   \end{frame}

   432 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   433 

   434 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   435   \begin{frame}[c]

   436   \frametitle{What is Static Analysis?}

   437 

   438   \begin{center}

   439   \includegraphics[scale=0.4]{../pics/state5.png}

   440   \end{center}

   441   

   442   \begin{itemize}

   443   \item this needs more work

   444   \end{itemize}

   445 

   446   \end{frame}

   447 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   448 

   449 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   450   \begin{frame}[c]

   451   \frametitle{What is Static Analysis?}

   452 

   453   \begin{center}

   454   \includegraphics[scale=0.4]{../pics/state6.png}

   455   \end{center}

   456   

   457   \end{frame}

   458 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   459 

   460 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   461   \begin{frame}[c,fragile]

   462     \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]

   463                   Are Vars Definitely Initialised?\end{tabular}}

   464 

   465 Assuming \texttt{x} is initialised, what about \texttt{y}?\bigskip

   466 

   467 Prog.~1:\\

   468 \begin{lstlisting}[numbers=none,

   469                    basicstyle=\ttfamily,

   470                    language=While,xleftmargin=3mm]

   471 if x < 1 then y := x else y := x + 1;

   472 y := y + 1

   473 \end{lstlisting}\medskip     

   474 

   475 Prog.~2:\\

   476 \begin{lstlisting}[numbers=none,

   477                    basicstyle=\ttfamily,

   478                    language=While,xleftmargin=3mm]

   479 if x < x then y := y + 1 else y := x;

   480 y := y + 1

   481 \end{lstlisting}            

   482 

   483   \end{frame}

   484 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   485 

   486 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   487   \begin{frame}[c,fragile]

   488     \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]

   489                   Are Vars Definitely Initialised?\end{tabular}}

   490 

   491               What should the rules be for deciding when a

   492               variable is initialised?\bigskip\pause

   493 

   494 \begin{itemize}

   495 \item variable \texttt{x} is definitely initialized after

   496   \texttt{skip}\\

   497   iff \texttt{x} is definitely initialized before \texttt{skip}.

   498 \end{itemize}

   499   

   500 \end{frame}

   501 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   502 

   503 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   504   \begin{frame}[c,fragile]

   505 %    \frametitle{\Large\begin{tabular}{c}Concrete Example:\\[-1mm]

   506 %                  Are Vars Definitely Initialised?\end{tabular}}

   507 

   508 $\bl{A}$ is the set of definitely defined variables:

   509               

   510 \begin{center}

   511 \begin{tabular}{c}

   512   \bl{\infer{\mbox{}}{A\;\texttt{skip}\;A}}\qquad

   513   \bl{\infer{vars(a) \subseteq A}{A\;\;(\texttt{x\,:=\,a})\;\;\{x\}\cup A}}

   514   \medskip\\\pause

   515 

   516   \bl{\infer{A_1\;s_1\;A_2\quad A_2\;s_2\;A_3}{A_1\;(s_1 ; s_2)\;A_3}}

   517   \medskip\\\pause

   518   

   519   \bl{\infer{vars(b)\subseteq A\quad A\;s_1\;A_1\quad A\;s_2\;A_2}

   520   {A\;(\texttt{if}\;b\;\texttt{then}\;s_1\;\texttt{else}\;s_2)\;A_1\cap A_2}}

   521   \medskip\\\pause

   522 

   523   \bl{\infer{vars(b)\subseteq A\quad A\;s\;A'}

   524   {A\;(\texttt{while}\;b\;\texttt{do}\;s)\;A}}\pause

   525 \end{tabular}  

   526 \end{center}

   527 

   528 \hfill we start with $\bl{A = \{\}}$

   529 \end{frame}

   530 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

   531