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 \ prop \ prop" + ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") + + "_asms" :: "prop \ asms \ asms" + ("\<^raw:\mbox{>_\<^raw:}\\>/ _") + + "_asm" :: "prop \ 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 \ prop \ prop" + ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + "_asms" :: "prop \ asms \ asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") + "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") + +notation (IfThenNoBox output) + "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") +syntax (IfThenNoBox output) + "_bigimpl" :: "asms \ prop \ prop" + ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + "_asms" :: "prop \ asms \ asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") + "_asm" :: "prop \ asms" ("_") + +consts DUMMY::'a + +abbreviation + "is_parent f pf \ (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 ("\_\") and + erole_functor ("erole'_aux") + +declare [[show_question_marks = false]] + +abbreviation + "is_process_type s p t \ (type_of_process s p = Some t)" + +abbreviation + "is_current_role s p r \ (currentrole s p = Some r)" + +abbreviation + "is_file_type s f t \ (etype_of_file s f = Some t)" + + +lemma osgrant10: (* modified by chunhan *) + "\p \ current_procs \; p' \ current_procs \\ \ os_grant \ (Clone p p')" +by simp + +lemma rcgrant4: + "\is_current_role s p r; is_file_type s f t; (r, File_type t, EXECUTE) \ compatible\ + \ 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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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{ + \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 +(*>*) + +