# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1416881088 0
# Node ID 54a1fbe96b14b1af3b4ba7902a904f69d9854e2d
# Parent  323e1290360b25cdd6932031475cec0d6aac8c8c
updated

diff -r 323e1290360b -r 54a1fbe96b14 slides/slides09.pdf
Binary file slides/slides09.pdf has changed
diff -r 323e1290360b -r 54a1fbe96b14 slides/slides09.tex
--- a/slides/slides09.tex	Sun Nov 23 22:32:00 2014 +0000
+++ b/slides/slides09.tex	Tue Nov 25 02:04:48 2014 +0000
@@ -1,53 +1,16 @@
 \documentclass[dvipsnames,14pt,t]{beamer}
-\usepackage{proof}
-\usepackage{beamerthemeplaincu}
-\usepackage{mathpartir}
-\usepackage{isabelle}
-\usepackage{isabellesym}
-\usepackage[absolute,overlay]{textpos}
-\usepackage{ifthen}
-\usepackage{tikz}
-\usepackage{courier}
-\usepackage{listings}
-\usetikzlibrary{arrows}
-\usetikzlibrary{positioning}
-\usetikzlibrary{calc}
-\usepackage{graphicx} 
-\usetikzlibrary{shapes}
-\usetikzlibrary{shadows}
-\usetikzlibrary{plotmarks}
-
-
-\isabellestyle{rm}
-\renewcommand{\isastyle}{\rm}%
-\renewcommand{\isastyleminor}{\rm}%
-\renewcommand{\isastylescript}{\footnotesize\rm\slshape}%
-\renewcommand{\isatagproof}{}
-\renewcommand{\endisatagproof}{}
-\renewcommand{\isamarkupcmt}[1]{#1}
-
-% Isabelle characters
-\renewcommand{\isacharunderscore}{\_}
-\renewcommand{\isacharbar}{\isamath{\mid}}
-\renewcommand{\isasymiota}{}
-\renewcommand{\isacharbraceleft}{\{}
-\renewcommand{\isacharbraceright}{\}}
-\renewcommand{\isacharless}{$\langle$}
-\renewcommand{\isachargreater}{$\rangle$}
-\renewcommand{\isasymsharp}{\isamath{\#}}
-\renewcommand{\isasymdots}{\isamath{...}}
-\renewcommand{\isasymbullet}{\act}
+\usepackage{../slides}
+\usepackage{../graphics}
+\usepackage{../langs}
 
 % beamer stuff 
-\renewcommand{\slidecaption}{APP 09, King's College London, 3 December 2013}
-\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\renewcommand{\slidecaption}{APP 09, King's College London}
 \newcommand{\bl}[1]{\textcolor{blue}{#1}}
 
 \begin{document}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}<1>[t]
+\begin{frame}[t]
 \frametitle{%
   \begin{tabular}{@ {}c@ {}}
   \\
@@ -64,468 +27,688 @@
   \end{tabular}
   \end{center}
 
-\end{frame}}
- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Review: Proofs}
+  \begin{center}
+  \includegraphics[scale=0.6]{../pics/bridge-limits.png}
+  \end{center}
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-Modify the formula
-\begin{center}
-\begin{tabular}{l}
-\bl{$P\;\textit{controls}\;\textit{Permitted}(O, \textit{write})$}\\
-\end{tabular}
-\end{center}
-using security levels so that it satisfies the {\it write rule} from the {\it
-Bell-LaPadula} access policy.\bigskip 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \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}
 
-Do the same again, but satisfy the {\it write rule}
-from the {\it Biba} access policy.
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
 
-\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)
+
+  \vfill
+  \small
+  Dijkstra: shortest path algorithm, 
+  dining philosophers problem,
+  semaphores
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
 \begin{frame}[c]
-\frametitle{Review: Proofs}
+\frametitle{\Large Proving Programs to be Correct}
 
-Assume two security levels \bl{$\textit{S}$} and \bl{$\textit{TS}$}, 
-which are ordered so that \bl{$slev(\textit{S}) < slev(\textit{TS})$}. 
-Assume further the substitution rules
-\begin{center}
-\bl{\begin{tabular}{@{}c@{}}
-$\Gamma \vdash slev(P) = l_1$ \hspace{2mm} $\Gamma \vdash slev(Q) = l_2$
-\hspace{2mm} $\Gamma \vdash l_1 < l_2$\\\hline
-$\Gamma \vdash slev(P) < slev(Q)$
-\end{tabular}}
-\end{center}
+\begin{bubble}[10cm]
+\small
+{\bf Theorem:} There are infinitely many prime 
+numbers.\medskip\\
 
-\begin{center}
-\bl{\begin{tabular}{c}
-$\Gamma \vdash slev(P) = l$ \hspace{4mm} $\Gamma \vdash slev(Q) = l$\\\hline
-$\Gamma \vdash slev(P) = slev(Q)$
-\end{tabular}}
-\end{center}
+{\bf Proof} \ldots\\
+\end{bubble}\bigskip
 
 
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+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 (protocol, OS,\ldots).
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Review: Proofs}\small
+  \begin{frame}[c]
+  \frametitle{\Large{}Mars Pathfinder Mission 1997}
 
-Let \bl{$\Gamma$} be the set containing the following six formulas
-\begin{center}
-\bl{\begin{tabular}{@{}l@{}}
-$slev(\textit{S}) < slev(\textit{TS})$\smallskip\\
-$slev(\textit{Agent}) = slev(\textit{TS})$\smallskip\\
-$slev(\textit{File}_1) = slev(\textit{S})$\smallskip\\
-$slev(\textit{File}_2) = slev(\textit{TS})$\smallskip\\
-$\forall O.\;slev(O) < slev(\textit{Agent}) \Rightarrow$\\ 
-\hspace{30mm}$(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\smallskip\\
-$\forall O.\;slev(O) = slev(\textit{Agent}) \Rightarrow$\\ 
-\hspace{30mm}$(\textit{Agent}\;\textit{controls}\;\textit{Permitted}(O, \textit{read}))$\\
-\end{tabular}}
-\end{center}
-Using the inference rules of access-control logic and the substitution rules shown above,
-give proofs for the two judgements
-\begin{center}
-\bl{\begin{tabular}{@{}l@{}}
-$\Gamma \vdash
-(\textit{Agent}\;\textit{says}\;\textit{Permitted}(\textit{File}_1,
-\textit{read})) \Rightarrow$\\
-\hspace{50mm}$\textit{Permitted}(\textit{File}_1, \textit{read})$\\
-\end{tabular}}
-\end{center}
+  \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}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[t]
-\frametitle{Checking Solutions}
+  \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}};
+  
+    
 
-How can you check somebody's solution without revealing the solution?\pause\bigskip
+  \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); 
+  }
 
-Alice and Bob solve crosswords. Alice knows the answer for 21D (folio) but doesn't 
-want to tell Bob.\medskip
+
+  \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 staved indefinitely.
+  \end{bubble}}
+  \end{textblock}
 
-You use an English  dictionary:
+  \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}};
+  
+    
 
-\begin{itemize}
-\item folio \onslide<4->{$\stackrel{1}{\rightarrow}$ individual }
-                \onslide<5->{$\stackrel{2}{\rightarrow}$ human}
-                \onslide<6->{$\stackrel{3}{\rightarrow}$ or \ldots}
-\only<3>{
-\begin{quote}
-``an \alert{individual} leaf of paper or parchment, either loose as one of a series or 
-forming part of a bound volume, which is numbered on the recto or front side only.''	
-\end{quote}}
-\only<4>{
-\begin{quote}
-``a single \alert{human} being as distinct from a group''
-\end{quote}}
-\only<5>{
-\begin{quote}
-``relating to \alert{or} characteristic of humankind''
-\end{quote}}
-\end{itemize}\bigskip\bigskip
+  \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);
+  }
 
-\only<7->{
-this is essentially a hash function...but Bob can only check once he has also found the solution
-}
+  \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{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+  \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}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Zero-Knowledge Proofs}
 
-Two remarkable properties of \alert{Zero-Knowledge Proofs}:\bigskip
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+  
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \begin{frame}[c]
+  \frametitle{\Large Priority Inheritance Scheduling}
 
-\begin{itemize}
-\item Alice only reveals the fact that she knows a secret, not the secret itself (meaning 
-she can convince Bob that she knows the secret).\bigskip
-\item Having been convinced, Bob cannot use the evidence in order to convince Carol 
-that Alice knows the secret.
-\end{itemize}
+  \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
 
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+  \small this error is already known since around 1999
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[t]
-\frametitle{\begin{tabular}{@{}c@{}}The Idea \end{tabular}}
+  \begin{frame}[c]
 
-\begin{center}
-\begin{tabular}{l@{\hspace{10mm}}r}
-\\[-10mm]
-\raisebox{10mm}{\large 1.} & \includegraphics[scale=0.1]{pics/alibaba1.png}\\
-\raisebox{10mm}{\large 2.} & \includegraphics[scale=0.1]{pics/alibaba2.png}\\
-\raisebox{10mm}{\large 3.} & \includegraphics[scale=0.1]{pics/alibaba3.png}
-\end{tabular}
-\end{center}
+  \begin{center}
+  \includegraphics[scale=0.25]{../pics/p3.jpg}
+  \end{center}
 
-\begin{textblock}{7}(1,2.5)
-The Alibaba cave:
-\end{textblock}
+   \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}
 
-\small
-\only<2>{
-\begin{textblock}{12}(2,13.3)
-Even if Bob has a hidden camera, a recording will not be convincing to anyone else 
-(Alice and Bob could have made it all up).
-\end{textblock}}
-\only<3>{
-\begin{textblock}{12}(2,13.3)
-Even worse, an observer present at the experiment would not be convinced.
-\end{textblock}}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  
+     
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Applications of ZKPs}
+  \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}
 
-\begin{itemize}
-\item authentication, where one party wants to prove its identity to a 
-second party via some secret information,  but doesn't want the second 
-party to learn anything about this secret\bigskip
-\item to enforce honest behaviour while maintaining privacy: the idea is to 
-force a user to prove, using a zero-knowledge proof, that its behaviour is 
-correct according to the protocol
-\end{itemize}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+  \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}
+
+  \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 (PhD-student)
+
+  \end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Central Properties}
+  \begin{frame}[c]
+  \frametitle{Testing Policies}
 
-Zero-knowledge proof protocols should satisfy:\bigskip
+  \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);
 
-\begin{itemize}
-\item \alert{\bf Completeness} If Alice knows the secret, Bob accepts Alice ``proof'' for sure.\bigskip
-\item \alert{\bf Soundness} If Alice does not know the secret, Bob accepts her ``proof'' with a very 
-small probability.
-\end{itemize}
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+  \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};}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Graph Isomorphism}
+  \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}}
 
-\begin{center}
-\begin{tabular}{l@{\hspace{10mm}}r}
-\includegraphics[scale=0.8]{pics/graphs.png}\\
-\end{tabular}
-\end{center}
+  \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}}
 
-Finding an isomorphism between two graphs is an NP complete problem.
-\end{frame}}
+  \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}
+
+  \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Graph Isomorphism Protocol}
-
-Alice starts with knowing an isomorphism \bl{$\sigma$} between graphs \bl{$G_1$} and \bl{$G_2$}\medskip
-
-\begin{enumerate}
-\item Alice generates an isomorphic graph \bl{$H$} which she sends to Bob 
-\item Bob asks either for an isomorphism between \bl{$G_1$} and \bl{$H$}, or
-\bl{$G_2$} and \bl{$H$}	
-\item Alice and Bob repeat this procedure \bl{$n$} times	
-\end{enumerate}\pause
-
-these are called commitment algorithms
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
-   
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Graph Isomorphism Protocol (2)}
+  \begin{frame}[c]
+  \frametitle{A Sound and Complete Test}
 
-If Alice knows the isomorphism, she can always calculate \bl{$\sigma$}.\bigskip
-
- If she doesn't, she can only correctly respond if Bob's 
- choice of index is the same as the one she used to form \bl{$H$}. The probability 
- of this happening is \bl{$\frac{1}{2}$}, so after \bl{$n$} rounds the probability of her 
- always responding correctly is only \bl{$\frac{1}{2}^n$}.
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Graph Isomorphism Protocol (3)}
-
-Why is the GI-protocol zero-knowledge?\bigskip\pause
-
-A: We can generate a fake transcript of a conversation, which 
-cannot be distinguished from a ``real'' conversation.\bigskip
-
-Anything Bob can compute using the information obtained from 
-the transcript can be computed using only a forged transcript and 
-therefore participation in such a communication does not increase 
-Bob's capability  to perform any computation.
+  \begin{itemize}
+  \item working purely in the \emph{dynamic world} does not work -\!-\!- infinite state space\bigskip
 
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%    
-   
-   
-   
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Non-Interactive ZKPs}
-
-
-\bigskip
-This is amazing: Alison can publish some data that contains no data about her secret,
-but this data can be used to convince anyone of the secret's existence.
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Non-Interactive ZKPs (2)}
-
-Alice starts with knowing an isomorphism \bl{$\sigma$} between graphs \bl{$G_1$} and \bl{$G_2$}\medskip
+  \item working purely on \emph{static} policies also does not\\ work -\!-\!- because of over approximation
+  \smallskip
+  \begin{itemize}
+  \item suppose a tainted file has type \emph{bin} and
+  \item there is a role \bl{$r$} which can both read and write \emph{bin}-files\pause
+  \item then we would conclude that this tainted file can spread\medskip\pause
+  \item but if there is no process with role \bl{$r$} and it will never been
+  created, then the file actually does not spread
+  \end{itemize}\bigskip\pause
 
-\begin{enumerate}
-\item Alice generates \bl{$n$} isomorphic graphs \bl{$H_{1..n}$} which she makes public 
-\item she feeds the \bl{$H_{1..n}$} into a hashing function (she has no control over what
-	the output will be)
-\item Alice takes the first \bl{$n$} bits of the output: whenever output is \bl{$0$}, she shows 
-an isomorphism with \bl{$G_1$} ; for \bl{$1$} she shows an isomorphism with \bl{$G_2$}
-\end{enumerate}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+  \item \alert{our solution:} take a middle ground and record precisely the information
+  of the initial state, but be less precise about every newly created object.
+  \end{itemize}
 
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Problems of ZKPs}
-
-\begin{itemize}
-\item ``grand chess master problem''\\ 
-(person in the middle)\bigskip
-
-\item Alice can have multiple identities; once she committed a fraud she stops using one
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+  \end{frame}}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Other Methods for ZKPs}
-
-Essentially every NP-problem can be used for ZKPs
-
-\begin{itemize}
-\item modular logarithms: Alice chooses public \bl{$A$},  \bl{$B$}, \bl{$p$}; and private \bl{$x$}
-
-\begin{center}
-\bl{$A^x \equiv B\; mod\; p$}
-\end{center} 
-\end{itemize}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Commitment Stage}
-
-\begin{enumerate}
-\item Alice generates \bl{$z$} random numbers \bl{$r_1$}, ..., \bl{$r_z$}, all less than \bl{$p - 1$}.
-\item Alice sends Bob for all \bl{$1..z$} 
-\begin{center}
-\bl{$h_i = A^{r_i} \;mod\; p$}
-\end{center}
-\item Bob generates random bits   \bl{$b_1$}, ..., \bl{$b_z$} by flipping a coin
-\item For each bit \bl{$b_i$}, Alice sends Bob an \bl{$s_i$} where
-
-\begin{center}
-\begin{tabular}{ll}
-\bl{$b_i = 0$}: & \bl{$s_i = r_i$}\\
-\bl{$b_i = 1$}: & \bl{$s_i = (r_i - r_j) \;mod\; (p -1)$}\\
-\end{tabular}
-\end{center}
-where \bl{$r_j$} is the lowest \bl{$j$} where \bl{$b_j = 1$}
- 
-\end{enumerate}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Confirmation Stage}
-
-\begin{enumerate}
-\item For each \bl{$b_i$} Bob checks whether \bl{$s_i$} conforms to the protocol
-
-\begin{center}
-\begin{tabular}{ll}
-\bl{$b_i = 0$}: & \bl{$A^{s_i} \equiv B\;mod\;p$}\\
-\bl{$b_i = 1$}: & \bl{$A^{s_i}  \equiv h_i * h_j^{-1}  \;mod\; p$}\\
-\end{tabular}
-\end{center}\bigskip
-
-Bob was send 
-
-\begin{center}
-\bl{$r_j - r _j$},  \bl{$r_m - r _j$}, \ldots, \bl{$r_p - r _j$ \;mod \;p} 
-\end{center}
-
-where the corresponding bits were 
-\bl{$1$}; Bob does not know \bl{$r_j$}, he does not know any \bl{$r_i$} where the bit was \bl{$1$}
-\end{enumerate}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
-\begin{frame}[c]
-\frametitle{Proving Stage}
-
-\begin{enumerate}
-\item Alice proves she knows \bl{$x$}, the discrete log of \bl{$B$}\\
-she sends
-
-\begin{center}
-\bl{$s_{z+1} = (x - r_j)$}
-\end{center}
-
-\item Bob confirms
-
-\begin{center}
-\bl{$A^{s_{z+1}} \equiv B * h_j^{-1} \;mod \; p$}
-\end{center}
-\end{enumerate}\bigskip\pause
-
-In order to cheat, Alice has to guess all bits in advance. She has only \bl{$1$} to \bl{$2^z$}
-chance. \\
-\small\hspace{7mm}\textcolor{gray}{(explanation $\rightarrow$ \url{http://goo.gl/irL9GK})}
-
-\end{frame}}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
-
- 
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\mode<presentation>{
 \begin{frame}[c]
 \frametitle{Random Number Generators}
 
-\begin{itemize}
-\item Computers are deterministic. How do they generate random numbers?\bigskip\pause
-
-\item The most popular method to generate random numbers between \bl{$0$} and \bl{$m$} is: choose
-three integers
-
-\begin{center}
-\begin{tabular}{ll}
-\bl{$a$} & multiplier\\
-\bl{$c$} & increment\\
-\bl{$X_0$} & start value
-\end{tabular}
-\end{center}
-
-and calculate
-
-\begin{center}
-\bl{$X_{n+1} = (a * X_n + c) \;mod\; m$}
-\end{center}
-\end{itemize}
-
-\only<3->{
-\begin{textblock}{7}(10,2)
-\begin{tikzpicture}
-\draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
-{\begin{minipage}{3.8cm}
-\begin{tabular}{ll|l}
-\bl{$m =$}    & \bl{$16$} & \bl{$16$}\\
-\bl{$X_0 =$} &  \bl{$1$} & \bl{$1$}\\
-\bl{$a = $}    & \bl{$5$} & \bl{$5$}\\
-\bl{$c =$}     & \bl{$1$} & \bl{$0$}\\
-\end{tabular} 
-\end{minipage}};
-\end{tikzpicture}
-\end{textblock}}
-
-\end{frame}}
+\end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
 \end{document}