\documentclass[dvipsnames,14pt,t]{beamer}
\usepackage{../slides}
\usepackage{../langs}
\usepackage{../graphics}
\usepackage{../grammar}
\usepackage{soul}

% beamer stuff 
\renewcommand{\slidecaption}{SEN 09, King's College London}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[t]
\frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \\
  \LARGE Security Engineering (9)\\[-3mm] 
  \end{tabular}}\bigskip\bigskip\bigskip

  \normalsize
  \begin{center}
  \begin{tabular}{ll}
  Email:  & christian.urban at kcl.ac.uk\\
  Office: & N7.07 (North Wing, Bush House)\\
  Slides: & KEATS (also homework is there)\\
  \end{tabular}
  \end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

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

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Old-Fashioned Eng.~vs.~CS}
  
  \begin{center}
  \begin{tabular}{@{}cc@{}}
  \begin{tabular}{@{}p{5.2cm}} 
  \includegraphics[scale=0.058]{../pics/towerbridge.jpg}\\ 
  {\bf bridges}: \\
  \raggedright\small
  engineers can ``look'' at a bridge and have a pretty good
  intuition about whether it will hold up or not\\ 
  (redundancy; predictive theory)
  \end{tabular} &
  \begin{tabular}{p{5cm}} 
  \includegraphics[scale=0.265]{../pics/code.jpg}\\
  \raggedright
  {\bf code}: \\
  \raggedright\small
  programmers have very little intuition about their code; 
  often it is too expensive to have redundancy;
  not ``continuous'' 
  \end{tabular}
  \end{tabular}
  \end{center}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[c]
\frametitle{Trusting Computing Base}
  
When considering whether a system meets some security
objectives, it is important to consider which parts of that
system are trusted in order to meet that objective (TCB).
\bigskip\pause

The smaller the TCB, the less effort it takes to get
some confidence that it is trustworthy, by doing a code 
review or by performing some (penetration) testing.
\bigskip

\footnotesize
CPU, compiler, libraries, OS, NP $\not=$ P,
random number generator, \ldots
\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
  
  unfortunately attackers exploit bugs (Satan's computer vs 
  Murphy's)

  \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 (protocols, OS, \ldots).

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{\Large{}Mars Pathfinder Mission 1997}

  \begin{center}
  \includegraphics[scale=0.15]{../pics/marspath1.png}
  \includegraphics[scale=0.16]{../pics/marspath3.png}
  \includegraphics[scale=0.3]{../pics/marsrover.png}
  \end{center}
  
  \begin{itemize}
  \item despite NASA's famous testing procedures, the lander crashed frequently on Mars
  \item a scheduling algorithm was not used in the OS
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  

  \begin{textblock}{11}(1,3)
  \begin{tabular}{@{\hspace{-10mm}}l}
  \begin{tikzpicture}[scale=1.1]
  \node at (-2.5,-1.5) {\textcolor{white}{a}};
  \node at (8,4) {\textcolor{white}{a}};
  
    

  \only<1>{
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
  }
  \only<2>{
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[fill, blue!50] (3,0) rectangle (5,0.6);
   \draw[fill, blue!100] (2,3) rectangle (3,3.6);
  }
  \only<3>{
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[fill, blue!50] (3,0) rectangle (4.5,0.6);
   \draw[fill, blue!50] (5.5,0) rectangle (6,0.6);
   \draw[fill, blue!100] (2,3) rectangle (3,3.6);
   \draw[fill, blue!100] (4.5,3) rectangle (5.5,3.6);
  }
  \only<4>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<5>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (4,0.6);
   \draw[blue!100, fill] (4,3) rectangle (5, 3.6);
  }
  \only<6>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<7>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
  }
  \only<8>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (2.5,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
   \draw[blue!100, very thick] (2.5,3) rectangle (3.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
  }
  \only<9>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
   \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
  }
  \only<10>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (3.5,0) rectangle (5,0.6);
   \draw[blue!100, very thick] (3.5,3) rectangle (4.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
   \draw[red, <-, line width = 2mm] (3.5,-0.1) -- (3.5, -1);
  }
  \only<11>{
   \node at (2.5,0.9) {\small locked a resource};
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (4.5,0) rectangle (6,0.6);
   \draw[blue!100, very thick] (4.5,3) rectangle (5.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
   \draw[red, <-, line width = 2mm] (4.5,-0.1) -- (4.5, -1);
  }
  \only<12>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2.5,0.6);
   \draw[blue!50, very thick] (5.5,0) rectangle (7,0.6);
   \draw[blue!100, very thick] (5.5,3) rectangle (6.5, 3.6);
   \draw[red, fill] (2.5,1.5) rectangle (3.5,2.1);
   \draw[red, fill] (3.55,1.5) rectangle (4.5,2.1);
   \draw[red, fill] (4.55,1.5) rectangle (5.5,2.1);
   \draw[red, <-, line width = 2mm] (5.5,-0.1) -- (5.5, -1);
   \node [anchor=base] at (6.3, 1.8) {\Large\ldots};
  }
  \only<13>{
   \node at (2.5,0.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, very thick] (2,0) rectangle (4,0.6);
   \draw[blue!100, very thick] (2,3) rectangle (3, 3.6);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<14>{
   \node at (2.5,3.9) {\small locked a resource}; 
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, fill] (2,3) rectangle (4,3.6);
   \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
   \draw[blue!50, ->, line width = 2mm] (2,1) -- (2, 2.5);
   \draw[red, <-, line width = 2mm] (2,-0.1) -- (2, -1);
  }
  \only<15>{
   \node at (2.5,3.9) {\small locked a resource};  
   \draw[fill, blue!50] (1,0) rectangle (2,0.6);
   \draw[blue!50, fill] (2,3) rectangle (4,3.6);
   \draw[blue!100, very thick] (4,3) rectangle (5, 3.6);
   \draw[red, <-, line width = 2mm] (2.5,-0.1) -- (2.5, -1);
   \draw[red, very thick] (2.5,1.5) rectangle (3.5,2.1); 
  }


  \draw[very thick,->](0,0) -- (8,0);
  \node [anchor=base] at (8, -0.3) {\scriptsize time};
  \node [anchor=base] at (0, -0.3) {\scriptsize 0};
  \node [anchor=base] at (-1.2, 0.2) {\small low priority};
  \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
  \only<8->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

  \end{tikzpicture}
  \end{tabular}
  \end{textblock}

  \begin{textblock}{0}(2.5,13)%
  \small
  \onslide<3->{
  \begin{bubble}[8cm]%
  Scheduling: You want to avoid that a high 
  priority process is starved indefinitely.
  \end{bubble}}
  \end{textblock}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{\Large Priority Inheritance Scheduling}

  \begin{itemize}
  \item Let a low priority process $L$ temporarily inherit 
    the high priority of $H$ until $L$ leaves the critical 
    section unlocking the resource.\bigskip
  \item Once the resource is unlocked $L$ returns to its original 
    priority level.
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  
  \begin{textblock}{11}(1,3)
  \begin{tabular}{@{\hspace{-10mm}}l}
  \begin{tikzpicture}[scale=1.1]
  \node at (-2.5,-1.5) {\textcolor{white}{a}};
  \node at (8,4) {\textcolor{white}{a}};
  
  \only<1>{
    \draw[fill, blue!50] (1,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
  }
  \only<2>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
  }
  \only<3>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
    \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
    \node at (3.5,3.3) {\small $A$};
  }
  \only<4>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,0.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,0) -- (3.5,0.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
    \draw[very thick,blue!100] (3,3) rectangle (4,3.6);
    \node at (3.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (4,3) rectangle (5,3.6);
    \node at (4.5,3.3) {\small $B$};
  }
  \only<5>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[very thick, blue!50] (3,3) rectangle (6,3.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (5.7,3.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
    \node at (6.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};
    \draw[blue!50, ->, line width = 2mm] (3,1) -- (3, 2.5);
  }
  \only<6>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[very thick, blue!50] (3.5,3) rectangle (6,3.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (5.7,3.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (5.7,3) -- (5.7,3.6);
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
    \node at (6.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$}; 
  }
  \only<7>{
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[very thick, blue!50] (3.5,0) rectangle (6,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (5.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (5.7,0) -- (5.7,0.6);
    \draw[very thick,blue!100] (6,3) rectangle (7,3.6);
    \node at (6.5,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
    \draw[blue!50, <-, line width = 2mm] (3.5,1) -- (3.5, 2.5);
    \draw[blue!50, <-, line width = 2mm] (4,3.3) -- (5.5,3.3);
  }
  \only<8>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[very thick, blue!50] (4.5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
  }
  \only<9>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
  }
  \only<10>{
    \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
    \draw[red, fill] (5,1.5) rectangle (6,2.1);
    \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
  }
  \only<11>{
   \draw[fill, blue!50] (1,0) rectangle (3,0.6);
    \draw[fill, blue!50] (3,3) rectangle (3.5,3.6);
    \draw[fill, blue!50] (4.5,0) rectangle (5,0.6);
    \draw[very thick, blue!50] (5,0) rectangle (7,0.6);
    \node at (1.5,0.9) {\small $A_L$};
    \node at (2.0,0.9) {\small $B_L$};
    \node at (3.5,3.9) {\small $A_R$};
    \node at (6.7,0.9) {\small $B_R$};
    \draw[very thick,blue!100] (1.5,0) -- (1.5,0.6);
    \draw[very thick,blue!100] (2.0,0) -- (2.0,0.6);
    \draw[very thick,blue!100] (3.5,3) -- (3.5,3.6);
    \draw[very thick,blue!100] (6.7,0) -- (6.7,0.6);
    \draw[fill,blue!100] (3.5,3) rectangle (4.5,3.6);
    \node at (4,3.3) {\small $A$};
    \draw[very thick,blue!100] (7,3) rectangle (8,3.6);
    \node at (7.5,3.3) {\small $B$};  
    \draw[red, fill] (5,1.5) rectangle (6,2.1);
    \draw[red, fill] (6.05,1.5) rectangle (7,2.1);
    \draw[blue!50, ->, line width = 2mm] (7.1,0.4) -- (8, 0.4);
    \draw[blue!50, ->, line width = 2mm] (7.1,4) -- (8,4);
  }

  \draw[very thick,->](0,0) -- (8,0);
  \node [anchor=base] at (8, -0.3) {\scriptsize time};
  \node [anchor=base] at (0, -0.3) {\scriptsize 0};
  \node [anchor=base] at (-1.2, 0.2) {\small low priority};
  \only<2->{\node [anchor=base] at (-1.2, 3.2) {\small high priority};}
  \only<10->{\node [anchor=base] at (-1.5, 1.7) {\small medium pr.};}

  \end{tikzpicture}
  \end{tabular}
  \end{textblock}
  
  \begin{textblock}{0}(2.5,13)%
  \small
  \onslide<11>{
  \begin{bubble}[8cm]%
  Scheduling: You want to avoid that a high 
  priority process is staved indefinitely.
  \end{bubble}}
  \end{textblock}


  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{\Large Priority Inheritance Scheduling}

  \begin{itemize}
  \item Let a low priority process $L$ temporarily inherit 
    the high priority of $H$ until $L$ leaves the critical 
    section unlocking the resource.\bigskip
  \item Once the resource is unlocked $L$ returns to its original 
    priority level. \alert{\bf BOGUS}\pause\bigskip
  \item \ldots $L$ needs to switch to the highest 
    \alert{remaining} priority of the threads that it blocks.
  \end{itemize}\bigskip

  \small this error is already known since around 1999

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.25]{../pics/p3.jpg}
  \end{center}

   \begin{itemize}
  \item by Rajkumar, 1991
  \item \it ``it resumes the priority it had at the point of entry into the critical 
  section''
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.25]{../pics/p2.jpg}
  \end{center}

   \begin{itemize}
  \item by Jane Liu, 2000
  \item {\it ``The job $J_l$ executes at its inherited 
    priority until it releases $R$; at that time, the 
    priority of $J_l$ returns to its priority 
    at the time when it acquires the resource $R$.''}\medskip
  \item \small gives pseudo code and totally bogus data structures  
  \item \small interesting part ``{\it left as an exercise}''
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
     
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.15]{../pics/p1.pdf}
  \end{center}

  \begin{itemize}
  \item by Laplante and Ovaska, 2011 (\$113.76)
  \item \it ``when $[$the task$]$ exits the critical section that
        caused the block, it reverts to the priority it had
        when it entered that section'' 
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]

  \begin{center}
  \includegraphics[scale=0.25]{../pics/p4.jpg}
  \end{center}

  \begin{itemize}
  \item by Silberschatz, Galvin, and Gagne, 2013 (OS-bible)
  \item \it ``Upon releasing the lock, the 
  $[$low-priority$]$ thread will revert to 
  its original priority.''
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
   
  
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Priority Scheduling}

  \begin{itemize}
  \item a scheduling algorithm that is widely used in real-time operating systems
  \item has been ``proved'' correct by hand in a paper in 1983
  \item but this algorithm turned out to be incorrect, despite its ``proof''\bigskip\pause
  
  \item we corrected the algorithm and then {\bf really} proved that it is correct	
  \item we implemented this algorithm in a small OS called PINTOS (used for teaching at Stanford)
  \item our implementation was much more efficient than their reference implementation
  \end{itemize}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
   
   
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Design of AC-Policies}

  Imagine you set up an access policy (root, lpd, users, staff, etc)
  \bigskip\pause

  \Large
  \begin{quote}
  ``what you specify is what you get but not necessarily what you want\ldots''
  \end{quote}\bigskip\bigskip\bigskip
  
  \normalsize main work by Chunhan Wu (a PhD-student in Nanjing)

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Testing Policies}

  \begin{center}
  \begin{tikzpicture}[scale=1]
  %\draw[black!10,step=2mm] (-5,-3) grid (5,4);
  %\draw[black!10,thick,step=10mm] (-5,-3) grid (5,4);
  \draw[white,thick,step=10mm] (-5,-3) grid (5,4);

  \draw [black!20, line width=1mm] (0,0) circle (1cm);
  \draw [line width=1mm] (0,0) circle (3cm);
  \node [black!20] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}};
  
  \draw [red, line width=2mm, <-] (-2.1,2.1) -- (-3.5,3.2);
  \node at (-3.5,3.6) {your system};
  \node at (-4.8,0) {\Large policy $+$};

  
  \only<2>{
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm);
  \draw [red, line width=2mm, <-] (2.3,1.2) -- (3.5,2);
  \node at (3.8,2.6) {\begin{tabular}{l}a seed\\[-1mm] \footnotesize virus, Trojan\end{tabular}};}

  \only<3>{
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm);
  \node[white] at (2,1) {\small tainted};}

  \only<4>{
  \begin{scope}
  \draw [clip] (0,0) circle (2.955cm);
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (9mm);
  \node[white] at (2,1) {\small tainted};
  \end{scope}}

  \only<5->{
  \begin{scope}
  \draw [clip] (0,0) circle (2.955cm);
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (13mm);
  \node[white] at (2,1) {\small tainted};
  \end{scope}}

  \only<6->{
  \draw[fill=white, line width=1mm] (1.265,2.665) arc (-35:183:5mm);
  \draw[fill=white, line width=1mm] (1.25,3.25) arc (-35:183:3mm);
  \node[black, rotate=10] at (1.9,3.6) {\LARGE\ldots};
  }

  \end{tikzpicture}
  \end{center}
  
  \only<7->{
  \begin{textblock}{4}(1,12)
  \small
  reduced the problem to a finite problem; gave a proof
  \end{textblock}} 

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c]
\frametitle{Big Proofs in CS (1)}

Formal proofs in CS sound like science fiction? Completely
irrelevant! Lecturer gone mad?\pause

\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 less buggy 
\end{itemize}
\end{itemize}

\begin{center}
  \includegraphics[scale=0.12]{../pics/compcert.png}
\end{center}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
\begin{frame}[c]
\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}[10cm]\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{Big Proofs in CS (2)}

\begin{itemize}
\item in 2010, verification of a micro-kernel operating system (approximately 8700 loc)
  \begin{itemize}
  \item used in helicopters and mobile phones
  \item 200k loc of proof
  \item 25 - 30 person years
  \item found 160 bugs in the C code (144 by the proof)
  \end{itemize}
\end{itemize}

\begin{bubble}[10cm]\small
``Real-world operating-system kernel with an end-to-end proof
of implementation correctness and security enforcement''
\end{bubble}\bigskip\pause

unhackable kernel (New Scientists, September 2015)
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
\begin{frame}[c]
\frametitle{Big Proofs in CS (3)}

\begin{itemize}
\item verified TLS implementation\medskip
\item verified compilers (CompCert, CakeML)\medskip
\item verified distributed systems (Verdi)\medskip
\item verified OSes or OS components\\
(seL4, CertiKOS, Ironclad Apps, \ldots)\medskip
\item verified cryptography
\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
\begin{frame}[c]
\frametitle{How Did This Happen?}

Lots of ways!

\begin{itemize}
\item better programming languages
  \begin{itemize}
  \item basic safety guarantees built in
  \item powerful mechanisms for abstraction and modularity
  \end{itemize}
\item better software development methodology
\item stable platforms and frameworks
\item better use of specifications\medskip\\
  \small If you want to build software that works or is secure, 
    it is helpful to know what you mean by ``works'' and by ``is secure''!
\end{itemize}

\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 secure/bug free/correct?\pause\bigskip

\item Very hard: Anything interesting about programs is equivalent
to 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}
  
  for example no key is leaked

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{\large Concrete Example: Sign-Analysis}
\mbox{}\\[-20mm]\mbox{}

\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
         | \meta{Exp} * \meta{Exp}
         | \meta{Exp} = \meta{Exp} 
         | \meta{num}
         | \meta{var}\\
: \meta{Stmt} ::= \meta{label} :
         | \meta{var} := \meta{Exp}
         | \pcode{jmp?} \meta{Exp} \meta{label}
         | \pcode{goto} \meta{label}\\
: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
\end{plstx}}

\begin{textblock}{0}(7.8,2.5)
\small
\begin{bubble}[5.6cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=3mm]
      a := 1
      n := 5 
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{textblock}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{\large Concrete Example: Sign-Analysis}
\mbox{}\\[-20mm]\mbox{}

\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
         | \meta{Exp} * \meta{Exp}
         | \meta{Exp} = \meta{Exp} 
         | \meta{num}
         | \meta{var}\\
: \meta{Stmt} ::= \meta{label} :
         | \meta{var} := \meta{Exp}
         | \pcode{jmp?} \meta{Exp} \meta{label}
         | \pcode{goto} \meta{label}\\
: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
\end{plstx}}

\begin{textblock}{0}(7.8,3.5)
\small
\begin{bubble}[5.6cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=3mm]
      n := 6
      m1 := 0
      m2 := 1
top:  jmp? n = 0 done
      tmp := m2
      m2 := m1 + m2
      m1 := tmp
      n := n + -1
      goto top
done:
\end{lstlisting}
\end{bubble}
\end{textblock}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{\large Concrete Example: Sign-Analysis}
\mbox{}\\[-20mm]\mbox{}

\bl{\begin{plstx}[rhs style=,one per line]
: \meta{Exp} ::= \meta{Exp} + \meta{Exp}
         | \meta{Exp} * \meta{Exp}
         | \meta{Exp} = \meta{Exp} 
         | \meta{num}
         | \meta{var}\\
: \meta{Stmt} ::= \meta{label} :
         | \meta{var} := \meta{Exp}
         | \pcode{jmp?} \meta{Exp} \meta{label}
         | \pcode{goto} \meta{label}\\
: \meta{Prog} ::= \meta{Stmt} \ldots{} \meta{Stmt}\\
\end{plstx}}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{Eval: An Interpreter}
\mbox{}\\[-14mm]\mbox{}

\small
\begin{center}
\bl{\begin{tabular}{lcl}
$[n]_{env}$ & $\dn$ & $n$\\
$[x]_{env}$ & $\dn$ & $env(x)$\\
$[e_1 + e_2]_{env}$ & $\dn$ & $[e_1]_{env} + [e_2]_{env}$\\
$[e_1 * e_2]_{env}$ & $\dn$ & $[e_1]_{env} * [e_2]_{env}$\\
$[e_1 = e_2]_{env}$ & $\dn$ & 
$\begin{cases}
1 & \text{if}\quad[e_1]_{env} = [e_2]_{env}\\
0 & \text{otherwise}
\end{cases}$\\
\end{tabular}}
\end{center}

\footnotesize
\begin{lstlisting}[numbers=none,xleftmargin=-5mm]
def eval_exp(e: Exp, env: Env) : Int = e match {
  case Num(n) => n
  case Var(x) => env(x)
  case Plus(e1, e2) => eval_exp(e1, env) + eval_exp(e2, env)
  case Times(e1, e2) => eval_exp(e1, env) * eval_exp(e2, env)
  case Equ(e1, e2) => 
    if (eval_exp(e1, env) == eval_exp(e2, env)) 1 else 0
}
\end{lstlisting}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\small
A program
\begin{bubble}[6cm]\footnotesize
\begin{lstlisting}[numbers=none,
                   language={},
                   basicstyle=\ttfamily,
                   xleftmargin=1mm]
      a := 1
      n := 5 
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}

The \emph{snippets} of the program:

\footnotesize
\begin{columns}
\begin{column}[t]{5cm}
\begin{bubble}[4.5cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=1mm]
""    a := 1
      n := 5 
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{column}
\begin{column}[t]{5cm}
\begin{bubble}[4.5cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=1mm]
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{column}
\begin{column}[t]{2cm}
\begin{bubble}[1.1cm]
\begin{lstlisting}[numbers=none,
                   basicstyle=\ttfamily,
                   language={},xleftmargin=1mm]
done:
\end{lstlisting}
\end{bubble}
\end{column}
\end{columns}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{Eval for Stmts}
\mbox{}\\[-12mm]\mbox{}

Let \bl{$sn$} be the snippets of a program

\small
\begin{center}
\bl{\begin{tabular}{lcl}
$[\texttt{nil}]_{env}$ & $\dn$ & $env$\medskip\\
$[\texttt{Label}(l:)::rest]_{env}$ & $\dn$ & $[rest]_{env}$\medskip\\
$[x \,\texttt{:=}\, e::rest]_{env}$ & $\dn$ & 
$[rest]_{(env[x:= [e]_{env}])}$\medskip\\
$[\texttt{jmp?}\;e\;l::rest]_{env}$ & $\dn$ & 
$\begin{cases}
[sn(l)]_{env} & \text{if}\quad[e]_{env} = 1\\
[rest]_{env}  & \text{otherwise}
\end{cases}$\medskip\\
$[\texttt{goto}\;l::rest]_{env}$ & $\dn$ & $[sn(l)]_{env}$\\
\end{tabular}}
\end{center}\bigskip

Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{Eval in Code}

\footnotesize
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
def eval(sn: Snips) : Env = {
  def eval_stmts(sts: Stmts, env: Env) : Env = sts match {
    case Nil => env
    case Label(l)::rest => eval_stmts(rest, env)
    case Assign(x, e)::rest => 
      eval_stmts(rest, env + (x -> eval_exp(e, env)))
    case Jmp(b, l)::rest => 
      if (eval_exp(b, env) == 1) eval_stmts(sn(l), env) 
      else eval_stmts(rest, env)
    case Goto(l)::rest => eval_stmts(sn(l), env)
  }

  eval_stmts(sn(""), Map())
}
\end{lstlisting}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{The Idea of Static Analysis}
\small
\mbox{}\bigskip\\

\begin{columns}
\begin{column}{5cm}
\begin{bubble}[4.5cm]\footnotesize
\begin{lstlisting}[numbers=none,
                   language={},
                   basicstyle=\ttfamily,
                   xleftmargin=1mm]
      a := 1
      n := 5 
top:  jmp? n = 0 done 
      a := a * n 
      n := n + -1 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{column}

\begin{column}{1cm}
\raisebox{-20mm}{\LARGE\bf$\Rightarrow$}
\end{column}
\begin{column}{6cm}
\begin{bubble}[4.7cm]\footnotesize
\begin{lstlisting}[numbers=none,
                   language={},
                   basicstyle=\ttfamily,
                   xleftmargin=1mm,
                   escapeinside={(*}{*)}]
      a := (*\hl{'+'}*)
      n := (*\hl{'+'}*) 
top:  jmp? n = (*\hl{'0'}*) done 
      a := a * n 
      n := n + (*\hl{'-'}*) 
      goto top 
done:
\end{lstlisting}
\end{bubble}
\end{column}
\end{columns}\bigskip\bigskip

Replace all constants and variables by either 
\pcode{+}, \pcode{-} or \pcode{0}. What we want to find out
is what the sign of \texttt{a} and \texttt{n} is (they should 
always positive).

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Sign Analysis?}

  
  \begin{columns}
  \begin{column}{3cm}
  \begin{tabular}{cc|l}
  $e_1$ & $e_2$ & $e_1 + e_2$\\\hline{}
  - & - & -\\
  - & 0 & -\\
  - & + & -, 0, +\\
  0 & $x$ & $x$\\
  + & - & -, 0, +\\
  + & 0 & +\\
  + & + & +\\
  \end{tabular}
  \end{column}

  \begin{column}{3cm}
  \begin{tabular}{cc|l}
  $e_1$ & $e_2$ & $e_1 * e_2$\\\hline{}
  - & - & +\\
  - & 0 & 0\\
  - & + & -\\
  0 & $x$ & 0\\
  + & - & -\\
  + & 0 & 0\\
  + & + & +\\
  \end{tabular}
  \end{column}
  \end{columns}

  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\mbox{}\\[-13mm]\mbox{}

\small
\begin{center}
\bl{\begin{tabular}{lcl}
$[n]_{aenv}$ & $\dn$ & 
$\begin{cases}
\{+\} & \text{if}\; n > 0\\
\{-\} & \text{if}\; n < 0\\
\{0\} & \text{if}\; n = 0
\end{cases}$\\
$[x]_{aenv}$ & $\dn$ & $aenv(x)$\\
$[e_1 + e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \oplus [e_2]_{aenv}$\\
$[e_1 * e_2]_{aenv}$ & $\dn$ & $[e_1]_{aenv} \otimes [e_2]_{aenv}$\\
$[e_1 = e_2]_{aenv}$ & $\dn$ & $\{0, +\}$\\
\end{tabular}}
\end{center}

\scriptsize
\begin{lstlisting}[language=Scala,numbers=none,xleftmargin=-5mm]
def aeval_exp(e: Exp, aenv: AEnv) : Set[Abst] = e match {
  case Num(0) => Set(Zero)
  case Num(n) if (n < 0) => Set(Neg)
  case Num(n) if (n > 0) => Set(Pos)
  case Var(x) => aenv(x)
  case Plus(e1, e2) => 
    aplus(aeval_exp(e1, aenv), aeval_exp(e2, aenv))
  case Times(e1, e2) => 
    atimes(aeval_exp(e1, aenv), aeval_exp(e2, aenv))
  case Equ(e1, e2) => Set(Zero, Pos)
}
\end{lstlisting}

\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{frame}[fragile]
\frametitle{AEval for Stmts}
\mbox{}\\[-12mm]\mbox{}

Let \bl{$sn$} be the snippets of a program

\small
\begin{center}
\bl{\begin{tabular}{lcl}
$[\texttt{nil}]_{aenv}$ & $\to$ & $(\texttt{nil},aenv)$\medskip\\
$[\texttt{Label}(l:)::rest]_{aenv}$ & $\to$ & $(rest, aenv)$\medskip\\
$[x \,\texttt{:=}\, e::rest]_{aenv}$ & $\to$ & 
$(rest, aenv[x:= [e]_{aenv}])$\medskip\\
$[\texttt{jmp?}\;e\;l::rest]_{aenv}$ & $\to$ & 
$(sn(l),aenv)$ \textcolor{black}{and} $(rest, aenv)$\medskip\\
$[\texttt{goto}\;l::rest]_{aenv}$ & $\to$ & $(sn(l), aenv)$\\
\end{tabular}}
\end{center}\bigskip

Start with \bl{$[sn(\mbox{\code{""}})]_{\varnothing}$}, try to 
reach all \emph{states} you can find (until a fix point is reached).

Check whether there are only $aenv$ in the final states that have 
your property.
\end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Sign Analysis}

  \begin{itemize}
  \item We want to find out whether \texttt{a} and \texttt{n}
  are always positive?\medskip
  \item After a few optimisations, we can indeed find this out.
  \begin{itemize}
  \item \texttt{equations} return \texttt{+} or \texttt{0}
  \item branch into only one dircection if you know
  \item if $x$ is \texttt{+}, then $x + \texttt{-1}$ 
  cannot be negative 
  \end{itemize}\bigskip
  
  \item What is this good for? Well, you do not need 
  underflow checks (in order to prevent buffer-overflow
  attacks). In general this technique is used to make sure 
  keys stay secret.
  \end{itemize}
  
  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Take Home Points}

  \begin{itemize}
  \item While testing is important, it does not show the 
    absence of bugs/vulnerabilities.\medskip
  \item More and more we need (formal) proofs that show
    a program is bug free.
  \end{itemize}
  
  \end{frame}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%



\end{document}


%%% Local Variables:  
%%% mode: latex
%%% TeX-master: t
%%% End: 

