
diff -r 7f589bfecffa -r ffe5d850df62 Slides/slides01.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/slides01.tex	Mon Feb 15 21:48:57 2016 +0100
@@ -0,0 +1,836 @@
+\documentclass[dvipsnames,14pt,t, xelatex]{beamer}
+\usepackage{slides}
+\usepackage{graph}
+
+
+% 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: & S1.27 (1st floor Strand Building)\\
+  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{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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+
+\end{document}
+
+
+%%% Local Variables:  
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
+




