(*<*)

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

(*>*)