(*<*)theory Slides1imports "../rc_theory" "../final_theorems" "../rc_theory" "../os_rc" beginnotation (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::'aabbreviation "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 microeditdr--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}}\only<3->{ \begin{textblock}{3}(10,9) \onslide<2-3>{ \begin{tikzpicture} \node at (0,0) [single arrow, fill=red,text=white, rotate=0, shape border rotate=180]{\mbox{\hspace{8mm}}}; \end{tikzpicture}} \end{textblock}} \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 in the OS 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}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *}text_raw {* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \mode<presentation>{ \begin{frame}[c] \begin{center} \alert{\bf\huge{Thanks!}}\bigskip \alert{\bf\huge{Questions?}} \end{center} \end{frame}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *}(*<*)endend(*>*)