1 (*<*)

     2 theory Slides1

     3 imports "../rc_theory" "../final_theorems" "../rc_theory" "../os_rc" 

     4 begin

     5 

     6 notation (Rule output)

     7   "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")

     8 

     9 syntax (Rule output)

    10   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    11   ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")

    12 

    13   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 

    14   ("\<^raw:\mbox{>_\<^raw:}\\>/ _")

    15 

    16   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

    17 

    18 notation (Axiom output)

    19   "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")

    20 

    21 notation (IfThen output)

    22   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    23 syntax (IfThen output)

    24   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    25   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    26   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

    27   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")

    28 

    29 notation (IfThenNoBox output)

    30   "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    31 syntax (IfThenNoBox output)

    32   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"

    33   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")

    34   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")

    35   "_asm" :: "prop \<Rightarrow> asms" ("_")

    36 

    37 consts DUMMY::'a

    38 

    39 abbreviation

    40   "is_parent f pf \<equiv> (parent f = Some pf)"

    41 

    42 context tainting_s_sound begin 

    43 

    44 notation (latex output)

    45   source_dir ("anchor") and

    46   SProc ("P_\<^bsup>_\<^esup>") and

    47   SFile ("F_\<^bsup>_\<^esup>") and

    48   SIPC ("I'(_')\<^bsup>_\<^esup>") and

    49   READ ("Read") and 

    50   WRITE ("Write") and

    51   EXECUTE ("Execute") and

    52   CHANGE_OWNER ("ChangeOwner") and

    53   CREATE ("Create") and

    54   SEND ("Send") and

    55   RECEIVE ("Receive") and

    56   DELETE ("Delete") and

    57   compatible ("permissions") and

    58   comproles ("compatible") and

    59   DUMMY  ("\<^raw:\mbox{$\_$}>") and

    60   Cons ("_::_" [78,77] 79) and 

    61   Proc ("") and

    62   File ("") and

    63   File_type ("") and

    64   Proc_type ("") and

    65   IPC ("") and

    66   init_processes ("init'_procs") and

    67   os_grant ("admissible") and

    68   rc_grant ("granted") and

    69   exists ("alive") and

    70   default_fd_create_type ("default'_type") and

    71   InheritParent_file_type ("InheritPatentType") and

    72   NormalFile_type ("NormalFileType") and

    73   deleted ("deleted _ _" [50, 100] 100) and

    74   taintable_s ("taintable\<^sup>s") and

    75   tainted_s ("tainted\<^sup>s") and

    76   all_sobjs ("reachable\<^sup>s") and

    77   init_obj2sobj ("\<lbrakk>_\<rbrakk>") and

    78   erole_functor ("erole'_aux") 

    79 

    80 declare [[show_question_marks = false]]

    81 

    82 abbreviation

    83   "is_process_type s p t \<equiv> (type_of_process s p = Some t)"

    84 

    85 abbreviation

    86   "is_current_role s p r \<equiv> (currentrole s p = Some r)"

    87 

    88 abbreviation

    89   "is_file_type s f t \<equiv> (etype_of_file s f = Some t)"

    90 

    91 

    92 lemma osgrant10: (* modified by chunhan *)

    93   "\<lbrakk>p \<in> current_procs \<tau>; p' \<notin> current_procs \<tau>\<rbrakk> \<Longrightarrow> os_grant \<tau> (Clone p p')"

    94 by simp 

    95 

    96 lemma rcgrant4:

    97   "\<lbrakk>is_current_role s p r; is_file_type s f t; (r, File_type t, EXECUTE) \<in> compatible\<rbrakk>

    98    \<Longrightarrow> rc_grant s (Execute p f)"

    99 by simp

   100 

   101 (*>*)

   102 

   103 text_raw {*

   104   \tikzset{alt/.code args={<#1>#2#3#4}{%

   105   \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}} % \pgfkeysalso doesn't change the path

   106   }}

   107   \renewcommand{\slidecaption}{CPP, 13 December 2013}

   108   \newcommand{\bl}[1]{\textcolor{blue}{#1}}                        

   109   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   110   \mode<presentation>{

   111   \begin{frame}

   112   \frametitle{%

   113   \begin{tabular}{@ {\hspace{-2mm}}c@ {}}

   114   \\[-3mm]

   115   \Large A Formalisation of an\\[-1mm] 

   116   \Large Access Control Framework

   117   \end{tabular}}

   118   

   119   \begin{center}

   120   \begin{tabular}{c@ {\hspace{15mm}}c}

   121   \includegraphics[scale=0.034]{chunhan.jpg} &

   122   \includegraphics[scale=0.034]{xingyuan.jpg}\\[-3mm]

   123   \end{tabular}

   124   \end{center}

   125  

   126   \begin{center}

   127   \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA

   128   University of Science and Technology in Nanjing

   129   \end{center}

   130 

   131   \begin{center}

   132   \small Christian Urban\\

   133   \small King's College London

   134   \end{center}

   135 

   136   \end{frame}}

   137   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   138 *}

   139 

   140 text_raw {*

   141   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   142   \begin{frame}[c]

   143   \frametitle{Access Control}

   144 

   145 \only<1>{

   146   Perhaps most known are

   147 

   148   \begin{itemize}

   149   \item Unix-style access control systems\\ 

   150   (root super-user, setuid mechanism)\bigskip

   151 

   152   \begin{center}\footnotesize

   153   \begin{semiverbatim}

   154 > ls -ld . * */*

   155 

   156 drwxr-xr-x 1 alice staff\ \ \ \  32768\ \ Apr\ \  2 2010 .

   157 

   158 -rw----r-- 1 alice students 31359\ \ Jul 24 2011 manual.txt

   159 

   160 -rwsr--r-x 1 bob\ \ \  students 141359 Jun\ \  1 2013 microedit

   161 

   162 dr--r-xr-x 1 bob\ \ \  staff\ \ \ \  32768\ \ Jul 23 2011 src

   163 

   164 -rw-r--r-- 1 bob\ \ \  staff\ \ \ \  81359\ \ Feb 28 2012 src/code.c

   165 \end{semiverbatim}

   166   \end{center}

   167 \end{itemize}}

   168 

   169 \only<2->{

   170 More fine-grained access control is provided by\medskip

   171 

   172 \begin{itemize}

   173   \item SELinux\\ (security enhanced Linux devloped by the NSA;\\ mandatory access control system)\bigskip 

   174   \item Role-Compatibility Model\\ (developed by Amon Ott;\\ main application in the

   175   Apache server) 

   176   \end{itemize}}

   177 

   178   \end{frame}

   179   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   180 

   181 *}

   182 

   183 text_raw {*

   184   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   185   \mode<presentation>{

   186   \begin{frame}[c]

   187   \frametitle{Operations in the OS}

   188   \bigskip

   189 

   190   using Paulson's inductive method a \alert{\bf state of the system} is 

   191   a \alert{\bf trace}, a list of events (system calls):

   192 

   193   \begin{center}\large

   194   \bl{$[e_1,\ldots, e_2]$}

   195   \end{center}\bigskip

   196   

   197 

   198    \begin{isabelle}\small

   199   \mbox{

   200   \begin{tabular}{@ {}r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l@ {\hspace{2mm}}l@ 

   201                      {\hspace{1.5mm}}l@ {\hspace{2mm}}l@ {\hspace{1.5mm}}l@ 

   202                      {\hspace{2mm}}l@ {}}

   203   @{text e} 

   204   & @{text "::="} & @{term "CreateFile p f"} & @{text "|"} & @{term "ReadFile p f"} & @{text "|"} & @{term "Send p i"}     \\

   205   & @{text "|"} & @{term "WriteFile p f"}    & @{text "|"} & @{term "Execute p f"} & @{text "|"} & @{term "Recv p i"}\\

   206   & @{text "|"} & @{term "DeleteFile p f"}   & @{text "|"} & @{term "Clone p p'"} & @{text "|"} & @{term "CreateIPC p i"}  \\

   207   & @{text "|"} & @{term "ChangeOwner p u"}  & @{text "|"} & @{term "ChangeRole p r"} & @{text "|"} & @{term "DeleteIPC p i"}\\

   208   & @{text "|"} & @{term "Kill p p'"}

   209   \end{tabular}}

   210   \end{isabelle}

   211   \end{frame}}

   212   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   213 

   214 *}

   215 

   216 

   217 

   218 text_raw {*

   219   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   220   \mode<presentation>{

   221   \begin{frame}[c]

   222   \frametitle{Valid Traces}

   223 

   224   we need to restrict the traces to \alert{\bf valid traces}:\bigskip\bigskip\bigskip 

   225 

   226   

   227   \begin{center}

   228   \begin{tabular}{@ {}c@ {}}

   229   \bl{@{thm [mode=Axiom] valid.intros(1)}}\hspace{5mm}

   230   \bl{@{thm [mode=Rule] valid.intros(2)}} 

   231   \end{tabular}

   232   \end{center}

   233 

   234   \begin{textblock}{3}(9,6.1)

   235   \onslide<2-3>{

   236   \begin{tikzpicture}

   237   \node at (0,0) [single arrow, fill=red,text=white, rotate=50, shape border rotate=180]{OS};

   238   \end{tikzpicture}}

   239   \end{textblock}

   240 

   241   \begin{textblock}{3}(6,11.2)

   242   \only<3>{

   243   \begin{tikzpicture}

   244   \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   245   {\normalsize\color{darkgray}

   246   \begin{minipage}{5.6cm}\raggedright

   247   \bl{@{thm[mode=Rule] osgrant10[of _ "s"]}}

   248   \end{minipage}};

   249   \end{tikzpicture}}

   250   \end{textblock}

   251 

   252   \begin{textblock}{6}(12.6,6.1)

   253   \onslide<4->{

   254   \begin{tikzpicture}

   255   \node at (0,0) [single arrow, fill=red,text=white, rotate=50, shape border rotate=180]{RC};

   256   \end{tikzpicture}}

   257   \end{textblock}

   258 

   259   \begin{textblock}{3}(4,11.3)

   260   \only<4->{

   261   \begin{tikzpicture}

   262   \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   263   {\normalsize\color{darkgray}

   264   \begin{minipage}{8.5cm}\raggedright

   265   \bl{@{thm[mode=Rule] rcgrant4}}

   266   \end{minipage}};

   267   \end{tikzpicture}}

   268   \end{textblock}

   269 

   270 

   271   \end{frame}}

   272   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   273 

   274 *}

   275 

   276 

   277 text_raw {*

   278   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   279   \mode<presentation>{

   280   \begin{frame}[c]

   281   \frametitle{Design of AC-Policies}

   282 

   283   \Large

   284   \begin{quote}

   285   ''what you specify is what you get but not necessarily what you want\ldots''

   286   \end{quote}

   287 

   288   \end{frame}}

   289   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   290 

   291 *}

   292 

   293 text_raw {*

   294   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   295   \mode<presentation>{

   296   \begin{frame}[c]

   297   \frametitle{Testing Policies}

   298 

   299   \begin{center}

   300   \begin{tikzpicture}[scale=1]

   301   %\draw[black!10,step=2mm] (-5,-3) grid (5,4);

   302   %\draw[black!10,thick,step=10mm] (-5,-3) grid (5,4);

   303   \draw[white,thick,step=10mm] (-5,-3) grid (5,4);

   304 

   305   \draw [black!20, line width=1mm] (0,0) circle (1cm);

   306   \draw [line width=1mm] (0,0) circle (3cm);

   307   \node [black!20] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}};

   308   

   309   \draw [red, line width=2mm, <-] (-2.1,2.1) -- (-3.5,3.2);

   310   \node at (-3.5,3.6) {your system};

   311   \node at (-4.8,0) {\Large policy $+$};

   312 

   313   

   314   \only<2>{

   315   \draw [black, fill=red, line width=0.5mm] (2,1) circle (3mm);

   316   \draw [red, line width=2mm, <-] (2.3,1.2) -- (3.5,2);

   317   \node at (3.8,2.3) {a seed};}

   318 

   319   \only<3>{

   320   \draw [black, fill=red, line width=0.5mm] (2,1) circle (7mm);

   321   \node[white] at (2,1) {\small tainted};}

   322 

   323   \only<4>{

   324   \begin{scope}

   325   \draw [clip] (0,0) circle (2.955cm);

   326   \draw [black, fill=red, line width=0.5mm] (2,1) circle (9mm);

   327   \node[white] at (2,1) {\small tainted};

   328   \end{scope}}

   329 

   330   \only<5->{

   331   \begin{scope}

   332   \draw [clip] (0,0) circle (2.955cm);

   333   \draw [black, fill=red, line width=0.5mm] (2,1) circle (13mm);

   334   \node[white] at (2,1) {\small tainted};

   335   \end{scope}}

   336 

   337   \only<6->{

   338   \draw[fill=white, line width=1mm] (1.265,2.665) arc (-35:183:5mm);

   339   \draw[fill=white, line width=1mm] (1.25,3.25) arc (-35:183:3mm);

   340   \node[black, rotate=10] at (1.9,3.6) {\LARGE\ldots};

   341   }

   342 

   343   \end{tikzpicture}

   344   \end{center}

   345 

   346 

   347   \begin{textblock}{3}(1,11.9)

   348   \only<5->{

   349   \begin{tikzpicture}

   350   \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   351   {\normalsize\color{darkgray}

   352   \begin{minipage}{6.9cm}\raggedright\small

   353   \bl{@{thm [mode=Rule] tainted.intros(6)}}

   354   \end{minipage}};

   355   \end{tikzpicture}}

   356   \end{textblock}

   357 

   358   \end{frame}}

   359   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   360 *}

   361 

   362 text_raw {*

   363   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   364   \mode<presentation>{

   365   \begin{frame}[c]

   366   \frametitle{\begin{tabular}{@ {}c@ {}}A Sound and Complete Test\end{tabular}}

   367 

   368   \begin{itemize}

   369   \item working purely in the \emph{dynamic world} does not work -\!-\!- infinite state space\bigskip

   370 

   371   \item working purely on \emph{static} policies also does not\\ work -\!-\!- because of over approximation

   372   \smallskip

   373   \begin{itemize}

   374   \item suppose a tainted file has type \emph{bin} and

   375   \item there is a role \bl{$r$} which can both read and write \emph{bin}-files\pause

   376   \item then we would conclude that the tainted file can spread\medskip\pause

   377   \item but if there is no process with role \bl{$r$} and it will never been

   378   created, then the file actually does not spread

   379   \end{itemize}\bigskip\pause

   380 

   381   \item \alert{our solution:} take a middle ground and record precisely the information

   382   of the initial state, but be less precise about every newly created object.

   383   \end{itemize}

   384 

   385   \end{frame}}

   386   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   387 *}

   388 

   389 text_raw {*

   390   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   391   \mode<presentation>{

   392   \begin{frame}[c]

   393   \frametitle{Results about our Test}

   394 

   395   \begin{itemize}

   396   \item we can show that the objects (files, processes, \ldots) we need to consider 

   397   are only finite (at some point

   398   it does not matter if we create another \emph{bin}-file)

   399   \end{itemize}

   400 

   401   \colorbox{cream}{

   402   \begin{minipage}{10.5cm}

   403   {\bf Thm (Soundness)}\\ If our test says an object is taintable, then 

   404   it is taintable, and we produce a sequence of events that show how it can

   405   be tainted.

   406   \end{minipage}}\bigskip\pause

   407 

   408   \colorbox{cream}{

   409   \begin{minipage}{10.5cm}

   410   {\bf Thm (Completeness)}\\ 

   411   If an object is taintable and \emph{undeletable$^\star$}, then 

   412   our test will find out that it is taintable.

   413   \end{minipage}}\medskip

   414 

   415   \small

   416   $^\star$ an object is \emph{undeleteable} if it exists in the initial state,

   417   but there exists no valid state in which it could have been deleted

   418 

   419   \end{frame}}

   420   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   421 *}

   422 

   423 text_raw {*

   424   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   425   \mode<presentation>{

   426   \begin{frame}[c]

   427   \frametitle{Why the Restriction?}

   428 

   429   \begin{itemize}

   430   \item assume a process with \bl{\emph{ID}} is tainted but gets killed by another process

   431   \item after that a proces with \bl{\emph{ID}} gets \emph{re-created} by cloning an untainted process\medskip

   432   \item clearly the new process should be considered untainted\pause

   433   \end{itemize}

   434 

   435   unfortunately our test will not be able to detect the difference (we are 

   436   less precise about newly created processes)\bigskip\medskip\pause

   437 

   438   \alert{Is this a serious restriction? We think not \ldots}

   439   

   440   \end{frame}}

   441   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   442 *}

   443 

   444 text_raw {*

   445   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   446   \mode<presentation>{

   447   \begin{frame}[c]

   448   \frametitle{Core System}

   449 

   450   Admins usually ask whether their policy is strong enough to protect their

   451   core system?

   452   

   453   \begin{center}

   454   \begin{tikzpicture}[scale=0.8]

   455 

   456   \draw [black!100, line width=1mm, fill=red] (0,0) circle (1.2cm);

   457   \draw [line width=1mm] (0,0) circle (3cm);

   458   \node [white] at (0,0) {\begin{tabular}{c}core\\[-1mm] system\end{tabular}};

   459   

   460   \begin{scope}

   461   \draw [clip] (0,0) circle (2.955cm);

   462   \draw [black, fill=red, line width=0.5mm] (2,1) circle (10mm);

   463   \node[white] at (2,1) {\small tainted};

   464   \end{scope}

   465 

   466   \end{tikzpicture}

   467   \end{center}

   468 

   469   core system files are typically undeletable

   470 

   471   \end{frame}}

   472   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   473 *}

   474 

   475 text_raw {*

   476   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   477   \mode<presentation>{

   478   \begin{frame}[c]

   479   \frametitle{Conclusion}

   480 

   481   \begin{itemize}

   482   \item we considered Role-Compatibility Model for the Apache Server\medskip \\

   483   13 events, 13 rules for OS admisibility, 14 rules for RC-granting, 10 rules for 

   484   tainted

   485   \end{itemize}\bigskip

   486 

   487   \begin{itemize}

   488   \item we can scale this to SELinux\medskip\\

   489   more fine-grainded OS events (inodes, hard-links, shared memory, \ldots)

   490   \end{itemize}\pause\bigskip

   491 

   492   \begin{itemize}

   493   \item hard sell to Ott (who designed the RC-model)

   494   \item hard sell to the community working on access control (beyond \emph{good science})

   495   \end{itemize}

   496   \end{frame}}

   497   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   498 *}

   499 

   500 

   501 

   502 (*<*)

   503 end

   504 end

   505 (*>*)

   506 

   507