
diff -r a87e2181d6b6 -r cfd4b8219c87 Slides/Slides1.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides1.thy	Fri Dec 13 10:37:25 2013 +1100
@@ -0,0 +1,507 @@
+(*<*)
+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>{
+  Perhaps most known are
+
+  \begin{itemize}
+  \item 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.3) {a seed};}
+
+  \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 the 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, 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 \bl{\emph{ID}} gets \emph{re-created} by cloning an untainted process\medskip
+  \item clearly the new process should be considered untainted\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 Role-Compatibility Model for the Apache Server\medskip \\
+  13 events, 13 rules for OS admisibility, 14 rules for RC-granting, 10 rules for 
+  tainted
+  \end{itemize}\bigskip
+
+  \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
+
+  \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
+(*>*)
+
+




