--- 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}