--- /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:
+