--- /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
+(*>*)
+
+