Slides/Slides1.thy
changeset 19 c3517b281164
parent 18 cfd4b8219c87
child 20 928c015eb03e
equal deleted inserted replaced
18:cfd4b8219c87 19:c3517b281164
   141   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   141   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   142   \begin{frame}[c]
   142   \begin{frame}[c]
   143   \frametitle{Access Control}
   143   \frametitle{Access Control}
   144 
   144 
   145 \only<1>{
   145 \only<1>{
   146   Perhaps most known are
   146   \begin{itemize}
   147 
   147   \item perhaps most known are
   148   \begin{itemize}
   148   Unix-style access control systems 
   149   \item Unix-style access control systems\\ 
       
   150   (root super-user, setuid mechanism)\bigskip
   149   (root super-user, setuid mechanism)\bigskip
   151 
   150 
   152   \begin{center}\footnotesize
   151   \begin{center}\footnotesize
   153   \begin{semiverbatim}
   152   \begin{semiverbatim}
   154 > ls -ld . * */*
   153 > ls -ld . * */*
   165 \end{semiverbatim}
   164 \end{semiverbatim}
   166   \end{center}
   165   \end{center}
   167 \end{itemize}}
   166 \end{itemize}}
   168 
   167 
   169 \only<2->{
   168 \only<2->{
   170 More fine-grained access control is provided by\medskip
   169 more fine-grained access control is provided by\medskip
   171 
   170 
   172 \begin{itemize}
   171 \begin{itemize}
   173   \item SELinux\\ (security enhanced Linux devloped by the NSA;\\ mandatory access control system)\bigskip 
   172   \item SELinux\\ (security enhanced Linux devloped by the NSA;\\ mandatory access control system)\bigskip 
   174   \item Role-Compatibility Model\\ (developed by Amon Ott;\\ main application in the
   173   \item Role-Compatibility Model\\ (developed by Amon Ott;\\ main application in the
   175   Apache server) 
   174   Apache server) 
   312 
   311 
   313   
   312   
   314   \only<2>{
   313   \only<2>{
   315   \draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm);
   314   \draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm);
   316   \draw [red, line width=2mm, <-] (2.3,1.2) -- (3.5,2);
   315   \draw [red, line width=2mm, <-] (2.3,1.2) -- (3.5,2);
   317   \node at (3.8,2.3) {a seed};}
   316   \node at (3.8,2.6) {\begin{tabular}{l}a seed\\[-1mm] \footnotesize virus, Trojan\end{tabular}};}
   318 
   317 
   319   \only<3>{
   318   \only<3>{
   320   \draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm);
   319   \draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm);
   321   \node[white] at (2,1) {\small tainted};}
   320   \node[white] at (2,1) {\small tainted};}
   322 
   321 
   371   \item working purely on \emph{static} policies also does not\\ work -\!-\!- because of over approximation
   370   \item working purely on \emph{static} policies also does not\\ work -\!-\!- because of over approximation
   372   \smallskip
   371   \smallskip
   373   \begin{itemize}
   372   \begin{itemize}
   374   \item suppose a tainted file has type \emph{bin} and
   373   \item suppose a tainted file has type \emph{bin} and
   375   \item there is a role \bl{$r$} which can both read and write \emph{bin}-files\pause
   374   \item there is a role \bl{$r$} which can both read and write \emph{bin}-files\pause
   376   \item then we would conclude that the tainted file can spread\medskip\pause
   375   \item then we would conclude that this tainted file can spread\medskip\pause
   377   \item but if there is no process with role \bl{$r$} and it will never been
   376   \item but if there is no process with role \bl{$r$} and it will never been
   378   created, then the file actually does not spread
   377   created, then the file actually does not spread
   379   \end{itemize}\bigskip\pause
   378   \end{itemize}\bigskip\pause
   380 
   379 
   381   \item \alert{our solution:} take a middle ground and record precisely the information
   380   \item \alert{our solution:} take a middle ground and record precisely the information
   399   \end{itemize}
   398   \end{itemize}
   400 
   399 
   401   \colorbox{cream}{
   400   \colorbox{cream}{
   402   \begin{minipage}{10.5cm}
   401   \begin{minipage}{10.5cm}
   403   {\bf Thm (Soundness)}\\ If our test says an object is taintable, then 
   402   {\bf Thm (Soundness)}\\ If our test says an object is taintable, then 
   404   it is taintable, and we produce a sequence of events that show how it can
   403   it is taintable in the OS, and we produce a sequence of events that show how it can
   405   be tainted.
   404   be tainted.
   406   \end{minipage}}\bigskip\pause
   405   \end{minipage}}\bigskip\pause
   407 
   406 
   408   \colorbox{cream}{
   407   \colorbox{cream}{
   409   \begin{minipage}{10.5cm}
   408   \begin{minipage}{10.5cm}
   426   \begin{frame}[c]
   425   \begin{frame}[c]
   427   \frametitle{Why the Restriction?}
   426   \frametitle{Why the Restriction?}
   428 
   427 
   429   \begin{itemize}
   428   \begin{itemize}
   430   \item assume a process with \bl{\emph{ID}} is tainted but gets killed by another process
   429   \item assume a process with \bl{\emph{ID}} is tainted but gets killed by another process
   431   \item after that a proces with \bl{\emph{ID}} gets \emph{re-created} by cloning an untainted process\medskip
   430   \item after that a proces with the same 
   432   \item clearly the new process should be considered untainted\pause
   431   \bl{\emph{ID}} gets \emph{re-created} by cloning an untainted process\medskip
       
   432   \item clearly the new process should be considered \emph{un}tainted\pause
   433   \end{itemize}
   433   \end{itemize}
   434 
   434 
   435   unfortunately our test will not be able to detect the difference (we are 
   435   unfortunately our test will not be able to detect the difference (we are 
   436   less precise about newly created processes)\bigskip\medskip\pause
   436   less precise about newly created processes)\bigskip\medskip\pause
   437 
   437 
   477   \mode<presentation>{
   477   \mode<presentation>{
   478   \begin{frame}[c]
   478   \begin{frame}[c]
   479   \frametitle{Conclusion}
   479   \frametitle{Conclusion}
   480 
   480 
   481   \begin{itemize}
   481   \begin{itemize}
   482   \item we considered Role-Compatibility Model for the Apache Server\medskip \\
   482   \item we considered the Role-Compatibility Model used for securing the Apache Server\medskip \\
   483   13 events, 13 rules for OS admisibility, 14 rules for RC-granting, 10 rules for 
   483   13 events, 13 rules for OS admisibility, 14 rules for RC-granting, 10 rules for 
   484   tainted
   484   tainted
   485   \end{itemize}\bigskip
   485   \end{itemize}\medskip
   486 
   486 
   487   \begin{itemize}
   487   \begin{itemize}
   488   \item we can scale this to SELinux\medskip\\
   488   \item we can scale this to SELinux\medskip\\
   489   more fine-grainded OS events (inodes, hard-links, shared memory, \ldots)
   489   more fine-grainded OS events (inodes, hard-links, shared memory, \ldots)
   490   \end{itemize}\pause\bigskip
   490   \end{itemize}\smallskip
       
   491   22 events, 22 admisibility, 22 granting, 15 taintable
       
   492   \pause\bigskip
   491 
   493 
   492   \begin{itemize}
   494   \begin{itemize}
   493   \item hard sell to Ott (who designed the RC-model)
   495   \item hard sell to Ott (who designed the RC-model)
   494   \item hard sell to the community working on access control (beyond \emph{good science})
   496   \item hard sell to the community working on access control (beyond \emph{good science})
   495   \end{itemize}
   497   \end{itemize}