(*<*)
theory Slides1
imports "../rc_theory" "../final_theorems" "../rc_theory" "../os_rc" 
begin

notation (Rule output)
  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

syntax (Rule output)
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")

  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")

  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (Axiom output)
  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")

notation (IfThen output)
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThen output)
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

notation (IfThenNoBox output)
  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
syntax (IfThenNoBox output)
  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
  "_asm" :: "prop \<Rightarrow> asms" ("_")

consts DUMMY::'a

abbreviation
  "is_parent f pf \<equiv> (parent f = Some pf)"

context tainting_s_sound begin 

notation (latex output)
  source_dir ("anchor") and
  SProc ("P_\<^bsup>_\<^esup>") and
  SFile ("F_\<^bsup>_\<^esup>") and
  SIPC ("I'(_')\<^bsup>_\<^esup>") and
  READ ("Read") and 
  WRITE ("Write") and
  EXECUTE ("Execute") and
  CHANGE_OWNER ("ChangeOwner") and
  CREATE ("Create") and
  SEND ("Send") and
  RECEIVE ("Receive") and
  DELETE ("Delete") and
  compatible ("permissions") and
  comproles ("compatible") and
  DUMMY  ("\<^raw:\mbox{$\_$}>") and
  Cons ("_::_" [78,77] 79) and 
  Proc ("") and
  File ("") and
  File_type ("") and
  Proc_type ("") and
  IPC ("") and
  init_processes ("init'_procs") and
  os_grant ("admissible") and
  rc_grant ("granted") and
  exists ("alive") and
  default_fd_create_type ("default'_type") and
  InheritParent_file_type ("InheritPatentType") and
  NormalFile_type ("NormalFileType") and
  deleted ("deleted _ _" [50, 100] 100) and
  taintable_s ("taintable\<^sup>s") and
  tainted_s ("tainted\<^sup>s") and
  all_sobjs ("reachable\<^sup>s") and
  init_obj2sobj ("\<lbrakk>_\<rbrakk>") and
  erole_functor ("erole'_aux") 

declare [[show_question_marks = false]]

abbreviation
  "is_process_type s p t \<equiv> (type_of_process s p = Some t)"

abbreviation
  "is_current_role s p r \<equiv> (currentrole s p = Some r)"

abbreviation
  "is_file_type s f t \<equiv> (etype_of_file s f = Some t)"


lemma osgrant10: (* modified by chunhan *)
  "\<lbrakk>p \<in> current_procs \<tau>; p' \<notin> current_procs \<tau>\<rbrakk> \<Longrightarrow> os_grant \<tau> (Clone p p')"
by simp 

lemma rcgrant4:
  "\<lbrakk>is_current_role s p r; is_file_type s f t; (r, File_type t, EXECUTE) \<in> compatible\<rbrakk>
   \<Longrightarrow> rc_grant s (Execute p f)"
by simp

(*>*)

text_raw {*
  \tikzset{alt/.code args={<#1>#2#3#4}{%
  \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}} % \pgfkeysalso doesn't change the path
  }}
  \renewcommand{\slidecaption}{CPP, 13 December 2013}
  \newcommand{\bl}[1]{\textcolor{blue}{#1}}                        
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{%
  \begin{tabular}{@ {\hspace{-2mm}}c@ {}}
  \\[-3mm]
  \Large A Formalisation of an\\[-1mm] 
  \Large Access Control Framework
  \end{tabular}}
  
  \begin{center}
  \begin{tabular}{c@ {\hspace{15mm}}c}
  \includegraphics[scale=0.034]{chunhan.jpg} &
  \includegraphics[scale=0.034]{xingyuan.jpg}\\[-3mm]
  \end{tabular}
  \end{center}
 
  \begin{center}
  \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA
  University of Science and Technology in Nanjing
  \end{center}

  \begin{center}
  \small Christian Urban\\
  \small King's College London
  \end{center}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \begin{frame}[c]
  \frametitle{Access Control}

\only<1>{
  \begin{itemize}
  \item perhaps most known are
  Unix-style access control systems 
  (root super-user, setuid mechanism)\bigskip

  \begin{center}\footnotesize
  \begin{semiverbatim}
> ls -ld . * */*

drwxr-xr-x 1 alice staff\ \ \ \  32768\ \ Apr\ \  2 2010 .

-rw----r-- 1 alice students 31359\ \ Jul 24 2011 manual.txt

-rwsr--r-x 1 bob\ \ \  students 141359 Jun\ \  1 2013 microedit

dr--r-xr-x 1 bob\ \ \  staff\ \ \ \  32768\ \ Jul 23 2011 src

-rw-r--r-- 1 bob\ \ \  staff\ \ \ \  81359\ \ Feb 28 2012 src/code.c
\end{semiverbatim}
  \end{center}
\end{itemize}}

\only<2->{
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 
  \item Role-Compatibility Model\\ (developed by Amon Ott;\\ main application in the
  Apache server) 
  \end{itemize}}

  \end{frame}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Operations in the OS}
  \bigskip

  using Paulson's inductive method a \alert{\bf state of the system} is 
  a \alert{\bf trace}, a list of events (system calls):

  \begin{center}\large
  \bl{$[e_1,\ldots, e_2]$}
  \end{center}\bigskip
  

   \begin{isabelle}\small
  \mbox{
  \begin{tabular}{@ {}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l@ {\hspace{2mm}}l@ 
                     {\hspace{1.5mm}}l@ {\hspace{2mm}}l@ {\hspace{1.5mm}}l@ 
                     {\hspace{2mm}}l@ {}}
  @{text e} 
  & @{text "::="} & @{term "CreateFile p f"} & @{text "|"} & @{term "ReadFile p f"} & @{text "|"} & @{term "Send p i"}     \\
  & @{text "|"} & @{term "WriteFile p f"}    & @{text "|"} & @{term "Execute p f"} & @{text "|"} & @{term "Recv p i"}\\
  & @{text "|"} & @{term "DeleteFile p f"}   & @{text "|"} & @{term "Clone p p'"} & @{text "|"} & @{term "CreateIPC p i"}  \\
  & @{text "|"} & @{term "ChangeOwner p u"}  & @{text "|"} & @{term "ChangeRole p r"} & @{text "|"} & @{term "DeleteIPC p i"}\\
  & @{text "|"} & @{term "Kill p p'"}
  \end{tabular}}
  \end{isabelle}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}



text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Valid Traces}

  we need to restrict the traces to \alert{\bf valid traces}:\bigskip\bigskip\bigskip 

  
  \begin{center}
  \begin{tabular}{@ {}c@ {}}
  \bl{@{thm [mode=Axiom] valid.intros(1)}}\hspace{5mm}
  \bl{@{thm [mode=Rule] valid.intros(2)}} 
  \end{tabular}
  \end{center}

  \begin{textblock}{3}(9,6.1)
  \onslide<2-3>{
  \begin{tikzpicture}
  \node at (0,0) [single arrow, fill=red,text=white, rotate=50, shape border rotate=180]{OS};
  \end{tikzpicture}}
  \end{textblock}

  \begin{textblock}{3}(6,11.2)
  \only<3>{
  \begin{tikzpicture}
  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
  {\normalsize\color{darkgray}
  \begin{minipage}{5.6cm}\raggedright
  \bl{@{thm[mode=Rule] osgrant10[of _ "s"]}}
  \end{minipage}};
  \end{tikzpicture}}
  \end{textblock}

  \begin{textblock}{6}(12.6,6.1)
  \onslide<4->{
  \begin{tikzpicture}
  \node at (0,0) [single arrow, fill=red,text=white, rotate=50, shape border rotate=180]{RC};
  \end{tikzpicture}}
  \end{textblock}

  \begin{textblock}{3}(4,11.3)
  \only<4->{
  \begin{tikzpicture}
  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
  {\normalsize\color{darkgray}
  \begin{minipage}{8.5cm}\raggedright
  \bl{@{thm[mode=Rule] rcgrant4}}
  \end{minipage}};
  \end{tikzpicture}}
  \end{textblock}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \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}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Testing Policies}

  \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);

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

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

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

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


  \begin{textblock}{3}(1,11.9)
  \only<5->{
  \begin{tikzpicture}
  \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 
  {\normalsize\color{darkgray}
  \begin{minipage}{6.9cm}\raggedright\small
  \bl{@{thm [mode=Rule] tainted.intros(6)}}
  \end{minipage}};
  \end{tikzpicture}}
  \end{textblock}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\begin{tabular}{@ {}c@ {}}A Sound and Complete Test\end{tabular}}

  \begin{itemize}
  \item working purely in the \emph{dynamic world} does not work -\!-\!- infinite state space\bigskip

  \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

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

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Results about our Test}

  \begin{itemize}
  \item we can show that the objects (files, processes, \ldots) we need to consider 
  are only finite (at some point
  it does not matter if we create another \emph{bin}-file)
  \end{itemize}

  \colorbox{cream}{
  \begin{minipage}{10.5cm}
  {\bf Thm (Soundness)}\\ If our test says an object is taintable, then 
  it is taintable in the OS, and we produce a sequence of events that show how it can
  be tainted.
  \end{minipage}}\bigskip\pause

  \colorbox{cream}{
  \begin{minipage}{10.5cm}
  {\bf Thm (Completeness)}\\ 
  If an object is taintable and \emph{undeletable$^\star$}, then 
  our test will find out that it is taintable.
  \end{minipage}}\medskip

  \small
  $^\star$ an object is \emph{undeleteable} if it exists in the initial state,
  but there exists no valid state in which it could have been deleted

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Why the Restriction?}

  \begin{itemize}
  \item assume a process with \bl{\emph{ID}} is tainted but gets killed by another process
  \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 
  less precise about newly created processes)\bigskip\medskip\pause

  \alert{Is this a serious restriction? We think not \ldots}
  
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Core System}

  Admins usually ask whether their policy is strong enough to protect their
  core system?
  
  \begin{center}
  \begin{tikzpicture}[scale=0.8]

  \draw [black!100, line width=1mm, fill=red] (0,0) circle (1.2cm);
  \draw [line width=1mm] (0,0) circle (3cm);
  \node [white] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}};
  
  \begin{scope}
  \draw [clip] (0,0) circle (2.955cm);
  \draw [black, fill=red, line width=0.5mm] (2,1) circle (10mm);
  \node[white] at (2,1) {\small tainted};
  \end{scope}

  \end{tikzpicture}
  \end{center}

  core system files are typically undeletable

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{Conclusion}

  \begin{itemize}
  \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}\medskip

  \begin{itemize}
  \item we can scale this to SELinux\medskip\\
  more fine-grainded OS events (inodes, hard-links, shared memory, \ldots)
  \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)
  \item hard sell to the community working on access control (beyond \emph{good science})
  \end{itemize}
  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}



(*<*)
end
end
(*>*)