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)