
diff -r cfd4b8219c87 -r c3517b281164 Slides/Slides1.thy
--- a/Slides/Slides1.thy	Fri Dec 13 10:37:25 2013 +1100
+++ b/Slides/Slides1.thy	Fri Dec 13 11:05:50 2013 +1100
@@ -143,10 +143,9 @@
   \frametitle{Access Control}
 
 \only<1>{
-  Perhaps most known are
-
   \begin{itemize}
-  \item Unix-style access control systems\\ 
+  \item perhaps most known are
+  Unix-style access control systems 
   (root super-user, setuid mechanism)\bigskip
 
   \begin{center}\footnotesize
@@ -167,7 +166,7 @@
 \end{itemize}}
 
 \only<2->{
-More fine-grained access control is provided by\medskip
+more fine-grained access control is provided by\medskip
 
 \begin{itemize}
   \item SELinux\\ (security enhanced Linux devloped by the NSA;\\ mandatory access control system)\bigskip 
@@ -314,7 +313,7 @@
   \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.3) {a seed};}
+  \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);
@@ -373,7 +372,7 @@
   \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 the tainted file can spread\medskip\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
@@ -401,7 +400,7 @@
   \colorbox{cream}{
   \begin{minipage}{10.5cm}
   {\bf Thm (Soundness)}\\ If our test says an object is taintable, then 
-  it is taintable, and we produce a sequence of events that show how it can
+  it is taintable in the OS, and we produce a sequence of events that show how it can
   be tainted.
   \end{minipage}}\bigskip\pause
 
@@ -428,8 +427,9 @@
 
   \begin{itemize}
   \item assume a process with \bl{\emph{ID}} is tainted but gets killed by another process
-  \item after that a proces with \bl{\emph{ID}} gets \emph{re-created} by cloning an untainted process\medskip
-  \item clearly the new process should be considered untainted\pause
+  \item after that a proces with the same 
+  \bl{\emph{ID}} gets \emph{re-created} by cloning an untainted process\medskip
+  \item clearly the new process should be considered \emph{un}tainted\pause
   \end{itemize}
 
   unfortunately our test will not be able to detect the difference (we are 
@@ -479,15 +479,17 @@
   \frametitle{Conclusion}
 
   \begin{itemize}
-  \item we considered Role-Compatibility Model for the Apache Server\medskip \\
+  \item we considered the Role-Compatibility Model used for securing the Apache Server\medskip \\
   13 events, 13 rules for OS admisibility, 14 rules for RC-granting, 10 rules for 
   tainted
-  \end{itemize}\bigskip
+  \end{itemize}\medskip
 
   \begin{itemize}
   \item we can scale this to SELinux\medskip\\
   more fine-grainded OS events (inodes, hard-links, shared memory, \ldots)
-  \end{itemize}\pause\bigskip
+  \end{itemize}\smallskip
+  22 events, 22 admisibility, 22 granting, 15 taintable
+  \pause\bigskip
 
   \begin{itemize}
   \item hard sell to Ott (who designed the RC-model)




