1 (*<*)

     2 theory Paper

     3 imports rc_theory final_theorems rc_theory os_rc 

     4 begin

     5 

     6 (* THEOREMS *)

     7 

     8 

     9 notation (Rule output)

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

    11 

    12 syntax (Rule output)

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

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

    15 

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

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

    18 

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

    20 

    21 notation (Axiom output)

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

    23 

    24 notation (IfThen output)

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

    26 syntax (IfThen output)

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

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

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

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

    31 

    32 notation (IfThenNoBox output)

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

    34 syntax (IfThenNoBox output)

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

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

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

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

    39 

    40 (* insert *)

    41 notation (latex)

    42   "Set.empty" ("\<emptyset>")

    43 

    44 translations 

    45   "{x} \<union> A" <= "CONST insert x A"

    46   "{x,y}" <= "{x} \<union> {y}"

    47   "{x,y} \<union> A" <= "{x} \<union> ({y} \<union> A)"

    48   "{x}" <= "{x} \<union> \<emptyset>"

    49 

    50 lemma impeq:

    51   "A = B \<Longrightarrow> (B \<Longrightarrow> A)"

    52 by auto

    53 

    54 

    55 

    56 

    57 consts DUMMY::'a

    58 

    59 abbreviation

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

    61 

    62 context tainting_s_sound begin 

    63 

    64 notation (latex output)

    65   source_dir ("anchor") and

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

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

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

    69   READ ("Read") and 

    70   WRITE ("Write") and

    71   EXECUTE ("Execute") and

    72   CHANGE_OWNER ("ChangeOwner") and

    73   CREATE ("Create") and

    74   SEND ("Send") and

    75   RECEIVE ("Receive") and

    76   DELETE ("Delete") and

    77   compatible ("permissions") and

    78   comproles ("compatible") and

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

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

    81   Proc ("") and

    82   File ("") and

    83   File_type ("") and

    84   Proc_type ("") and

    85   IPC ("") and

    86   init_processes ("init'_procs") and

    87   os_grant ("admissible") and

    88   rc_grant ("granted") and

    89   exists ("alive") and

    90   default_fd_create_type ("default'_type") and

    91   InheritParent_file_type ("InheritPatentType") and

    92   NormalFile_type ("NormalFileType") and

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

    94   taintable_s ("taintable\<^isup>s") and

    95   tainted_s ("tainted\<^isup>s") and

    96   all_sobjs ("reachable\<^isup>s") and

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

    98   erole_functor ("erole'_aux") --"I have a erole_functor and etype_aux to handle 

    99                                  efficient, but their name not same, so ..., but don't work"

   100 

   101 

   102 abbreviation

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

   104 

   105 abbreviation

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

   107 

   108 abbreviation

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

   110 

   111 lemma osgrant2:

   112   "\<lbrakk>p \<in> current_procs \<tau>; f \<notin> current_files \<tau>; parent f = Some pf; pf \<in> current_files \<tau>\<rbrakk> \<Longrightarrow>

   113    os_grant \<tau> (CreateFile p f)"

   114 by simp

   115 

   116 lemma osgrant6:

   117  "\<lbrakk>p \<in> current_procs \<tau>; u \<in> init_users\<rbrakk> \<Longrightarrow> os_grant \<tau> (ChangeOwner p u)"

   118 by simp

   119 

   120 lemma osgrant10:

   121   "\<lbrakk>p \<in> current_procs \<tau>; p' = new_proc \<tau>\<rbrakk> \<Longrightarrow> os_grant \<tau> (Clone p p')"

   122 by simp 

   123 

   124 

   125 lemma rcgrant1:

   126   "\<lbrakk>is_parent f pf; is_file_type s pf t; is_current_role s p r;

   127     default_fd_create_type r = InheritParent_file_type; 

   128     (r, File_type t, WRITE) \<in> compatible\<rbrakk>

   129    \<Longrightarrow> rc_grant s (CreateFile p f)"

   130 by simp

   131 

   132 lemma rcgrant1':

   133   "\<lbrakk>is_parent f pf; is_file_type s pf t; is_current_role s p r; 

   134     default_fd_create_type r = NormalFile_type t'; 

   135     (r, File_type t, WRITE) \<in> compatible;

   136     (r, File_type t', CREATE) \<in> compatible\<rbrakk>

   137    \<Longrightarrow> rc_grant s (CreateFile p f)"

   138 by simp

   139 

   140 lemma rcgrant4:

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

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

   143 by simp

   144 

   145 lemma rcgrant7: 

   146   "\<lbrakk>is_current_role s p r; r' \<in> comproles r\<rbrakk> \<Longrightarrow> rc_grant s (ChangeRole p r')"

   147 by simp

   148 

   149 lemma rcgrant_CHO:

   150 "\<lbrakk>is_current_role s p r; 

   151   type_of_process s p = Some t;

   152   (r, Proc_type t, CHANGE_OWNER) \<in> compatible\<rbrakk> \<Longrightarrow> rc_grant s (ChangeOwner p u)"

   153 by(simp)

   154 

   155 lemma pf_in_current_paper:

   156   "\<lbrakk>is_parent f pf; f \<in> current_files s; valid s\<rbrakk> \<Longrightarrow> pf \<in> current_files s"

   157 by (simp add:parent_file_in_current)

   158 

   159 lemma dels:

   160   shows "deleted (Proc p') ((Kill p p')#s)" 

   161   and   "deleted (File f) ((DeleteFile p f)#s)" 

   162   and   "deleted (IPC i) ((DeleteIPC p i)#s)"

   163   and   "deleted obj s \<Longrightarrow> deleted obj (e#s)"

   164 apply simp_all

   165 apply(case_tac e)

   166 apply(simp_all)

   167 done

   168 

   169 lemma tainted_10:

   170   "\<lbrakk>(File f) \<in> tainted s; valid (e # s); f \<in> current_files (e # s)\<rbrakk> 

   171   \<Longrightarrow> (File f) \<in> tainted (e # s)"

   172 apply(rule tainted.intros)

   173 apply(assumption)

   174 apply(assumption)

   175 apply(simp only: exists.simps)

   176 done

   177 

   178 definition

   179   Init ("init _")

   180 where

   181   "Init obj \<equiv> exists [] obj" 

   182 

   183 lemma Init_rhs:

   184   shows "Init (File f) = (f \<in> init_files)"

   185   and   "Init (Proc p) = (p \<in> init_processes)"

   186   and   "Init (IPC i) = (i \<in> init_ipcs)"

   187 unfolding Init_def

   188 by(simp_all)

   189 

   190 notation (latex output)

   191   Init ("_ \<in> init")

   192 

   193 lemma af_init':

   194   "\<lbrakk>f \<in> init_files; is_file_type [] f t\<rbrakk>

   195   \<Longrightarrow> SFile (t, f) (Some f) \<in> all_sobjs"

   196 apply(rule af_init)

   197 apply(simp)

   198 by (simp add:etype_of_file_def)

   199 

   200 declare [[show_question_marks = false]]

   201 

   202 

   203 (*>*)

   204 

   205 section {* Introduction *}

   206 

   207 text {*

   208   Role-based access control models are used in many operating systems

   209   for enforcing security properties.  The

   210   \emph{Role-Compatibility Model} (RC-Model), introduced by Ott

   211   \cite{ottrc,ottthesis}, is one such role-based access control

   212   model. It defines \emph{roles}, which are associated with processes,

   213   and defines \emph{types}, which are associated with system

   214   resources, such as files and directories. The RC-Model also includes

   215   types for interprocess communication, that is message queues,

   216   sockets and shared memory. A policy in the RC-Model gives every user

   217   a default role, and also specifies how roles can be

   218   changed. Moreover, it specifies which types of resources a role has

   219   permission to access, and also the \emph{mode} with which the role

   220   can access the resources, for example read, write, send, receive and

   221   so on.

   222    

   223   The RC-Model is built on top of a collection of system calls

   224   provided by the operating system, for instance system calls for

   225   reading and writing files, cloning and killing of processes, and

   226   sending and receiving messages. The purpose of the RC-Model is to

   227   restrict access to these system calls and thereby enforce security

   228   properties of the system. A problem with the RC-Model and role-based

   229   access control models in general is that a system administrator has

   230   to specify an appropriate access control policy. The difficulty with

   231   this is that \emph{``what you specify is what you get but not

   232   necessarily what you want''} \cite[Page 242]{Jha08}. To overcome

   233   this difficulty, a system administrator needs some kind of sanity

   234   check for whether an access control policy is really securing

   235   resources.  Existing works, for example \cite{sanity01,sanity02},

   236   provide sanity checks for policies by specifying properties and

   237   using model checking techniques to ensure a policy at hand satisfies

   238   these properties. However, these checks only address the problem on

   239   the level of policies---they can only check ``on the surface''

   240   whether the policy reflects the intentions of the system

   241   administrator---these checks are not justified by the actual

   242   behaviour of the operating system. The main problem this paper addresses is to check

   243   when a policy matches the intentions of a system administrator

   244   \emph{and} given such a policy, the operating system actually

   245   enforces this policy.

   246  

   247   Our work is related to the preliminary work by Archer et al

   248   \cite{Archer03} about the security model of SELinux. 

   249   They also give a dynamic model of system calls on which the access

   250   controls are implemented. Their dynamic model is defined in terms of

   251   IO automata and mechanised in the PVS theorem prover. For specifying

   252   and reasoning about automata they use the TAME tool in PVS. Their work checks

   253   well-formedness properties of access policies by type-checking 

   254   generated definitions in PVS. They can also ensure some ``\emph{simple

   255   properties}'' (their terminology), for example whether a process

   256   with a particular PID is present in every reachable state from 

   257   an initial state. They also consider ``\emph{deeper properties}'', for

   258   example whether only a process with root-permissions 

   259   or one of its descendents ever gets permission to write to kernel

   260   log files. They write that they can state such deeper 

   261   properties about access policies, but about checking such properties

   262   they write that ``\emph{the feasibility of doing 

   263   so is currently an open question}'' \cite[Page 167]{Archer03}.

   264   We improve upon their results by using our sound and complete 

   265   static policy check to make this feasible. 

   266 

   267   Our formal models and correctness proofs are mechanised in the

   268   interactive theorem prover Isabelle/HOL. The mechanisation of the models is a

   269   prerequisite for any correctness proof about the RC-Model, since it

   270   includes a large number of interdependent concepts and very complex

   271   operations that determine roles and types. In our opinion it is

   272   futile to attempt to reason about them by just using ``pencil-and-paper''.

   273   Following good experience in earlier mechanisation work

   274   \cite{ZhangUrbanWu12}, we use Paulson's inductive method for

   275   reasoning about sequences of events \cite{Paulson98}.  For example

   276   we model system calls as events and reason about an inductive

   277   definition of valid traces, that is lists of events.  Central to

   278   this paper is a notion of a resource being \emph{tainted}, which for

   279   example means it contains a virus or a back door.  We use our model

   280   of system calls in order to characterise how such a tainted object

   281   can ``spread'' through the system.  For a system administrator the

   282   important question is whether such a tainted file, possibly

   283   introduced by a user, can affect core system files and render the

   284   whole system insecure, or whether it can be contained by the access

   285   policy. Our results show that a corresponding check can be performed

   286   statically by analysing the initial state of the system and the access policy.

   287   \smallskip

   288  

   289   \noindent

   290   {\bf Contributions:} 

   291   We give a complete formalisation of the RC-Model in the interactive

   292   theorem prover Isabelle/HOL.  We also give a dynamic model of the

   293   operating system by formalising all security related events that can

   294   happen while the system is running.  As far as we are aware, we are

   295   the first ones who formally prove that if a policy in the RC-Model

   296   satisfies an access property, then there is no sequence of events

   297   (system calls) that can violate this access property.  We also prove

   298   the opposite: if a policy does not meet an access property, then

   299   there is a sequence of events that will violate this property in our

   300   model of the operating system.  With these two results in place we

   301   can show that a static policy check is sufficient in order to

   302   guarantee the access properties before running the system. Again as

   303   far as we know, no such check that is the operating

   304   system behaviour has been designed before.

   305   

   306 

   307   %Specified dynamic behaviour of the system; 

   308   %we specified a static AC model; designed a tainted relation for 

   309   %the system; proved that they coincide.

   310   %In our paper ....

   311    

   312 *}

   313   

   314 section {* Preliminaries about the RC-Model *}

   315 

   316 

   317 text {*

   318   The Role-Compatibility Model (RC-Model) is a role-based access

   319   control model. It has been introduced by Ott \cite{ottrc} and is

   320   used in running systems for example to secure Apache servers. It

   321   provides a more fine-grained control over access permissions than

   322   simple Unix-style access control models. This more fine-grained

   323   control solves the problem of server processes running as root with

   324   too many access permissions in order to accomplish a task at

   325   hand. In the RC-Model, system administrators are able to restrict

   326   what the role of server is allowed to do and in doing so reduce the

   327   attack surface of a system.

   328   

   329   Policies in the RC-Model talk about \emph{users}, \emph{roles},

   330   \emph{types} and \emph{objects}.  Objects are processes, files or

   331   IPCs (interprocess communication objects---such as message queues,

   332   sockets and shared memory). Objects are the resources of a system an

   333   RC-policy can restrict access to.  In what follows we use the letter

   334   @{term u} to stand for users, @{text r} for roles, @{term p} for

   335   processes, @{term f} for files and @{term i} for IPCs. We also

   336   use @{text obj} as a generic variable for objects.

   337   The RC-Model has the following eight kinds of access modes to objects:

   338 

   339   \begin{isabelle}\ \ \ \ \ %%%

   340   \begin{tabular}{@ {}l}

   341   @{term READ}, @{term WRITE}, @{term EXECUTE}, @{term "CHANGE_OWNER"}, 

   342   @{term CREATE}, @{term SEND}, @{term RECEIVE} and @{term DELETE}

   343   \end{tabular}

   344   \end{isabelle}

   345 

   346   In the RC-Model, roles group users according to tasks they need to 

   347   accomplish. Users have a default role specified by the policy,

   348   which is the role they start with whenever they log into the system.

   349   A process contains the information about its owner (a user), its

   350   role and its type, whereby a type in the RC-Model allows system

   351   administrators to group resources according to a common criteria.

   352   Such detailed information is needed in the RC-Model, for example, in

   353   order to allow a process to change its ownership. For this the

   354   RC-Model checks the role of the process and its type: if the access

   355   control policy states that the role has @{term CHANGE_OWNER} access mode for

   356   processes of that type, then the process is permitted to assume a

   357   new owner.

   358 

   359   Files in the RC-Model contain the information about their types.  A

   360   policy then specifies whether a process with a given role can access

   361   a file under a certain access mode. Files, however, also

   362   include in the RC-Model information about roles. This information is

   363   used when a process is permitted to execute a file. By doing so it

   364   might change its role. This is often used in the context of

   365   web-servers when a cgi-script is uploaded and then executed by the

   366   server.  The resulting process should have much more restricted

   367   access permissions.  This kind of behaviour when executing a file can

   368   be specified in an RC-policy in several ways: first, the role of the

   369   process does not change when executing a file; second, the process

   370   takes on the role specified with the file; or third, use the role of

   371   the owner, who currently owns this process. The RC-Model also makes

   372   assumptions on how types can change.  For example for files and IPCs

   373   the type can never change once they are created. But processes can

   374   change their types according to the roles they have.

   375   

   376   As can be seen, the information contained in a policy in the

   377   RC-Model can be rather complex: Roles and types, for example, are

   378   policy-dependent, meaning each policy needs to define a set of roles and a

   379   set of types. Apart from recording for each role the information

   380   which type of resource it can access and under which access-mode, it

   381   also needs to include a role compatibility set. This set specifies how one

   382   role can change into another role. Moreover it needs to include default

   383   information for cases when new processes or files are created.

   384   For example, when a process clones itself, the type of the new

   385   process is determined as follows: the policy might specify a default

   386   type whenever a process with a certain role is cloned, or the policy

   387   might specify that the cloned process inherits the type of the

   388   parent process.

   389   

   390   Ott implemented the RC-Model on top of Linux, but only specified it

   391   as a set of informal rules, partially given as logic formulas,

   392   partially given as rules in ``English''. Unfortunately, some

   393   presentations about the RC-Model give conflicting definitions for

   394   some concepts---for example when defining the semantics of the special role

   395   ``inherit parent''. In \cite{ottrc} it means inherit the initial role

   396   of the parent directory, but in \cite{ottweb} it means inherit

   397   the role of the parent process.  In our formalisation we mainly follow the

   398   version given in \cite{ottrc}. In the next section we give a mechanised

   399   model of the system calls on which the RC-Model is implemented.  

   400 *}

   401 

   402 

   403 

   404 section {* Dynamic Model of System Calls *}

   405 

   406 text {*

   407   Central to the RC-Model are processes, since they initiate any action

   408   involving resources and access control. We use natural numbers to stand for process IDs,

   409   but do not model the fact that the number of processes in any practical 

   410   system is limited. Similarly, IPCs and users are represented by natural 

   411   numbers. The thirteen actions a process can perform are represented by

   412   the following datatype of \emph{events}

   413   

   414   \begin{isabelle}\ \ \ \ \ %%%

   415   \mbox{

   416   \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l@ {\hspace{3mm}}l@ 

   417                      {\hspace{1.5mm}}l@ {\hspace{3mm}}l@ {\hspace{1.5mm}}l@ 

   418                      {\hspace{3mm}}l@ {\hspace{1.5mm}}l}

   419   event 

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

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

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

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

   424   \end{tabular}}

   425   \end{isabelle}

   426 

   427   \noindent

   428   with the idea that for example in @{term Clone} a process @{term p} is cloned

   429   and the new process has the ID @{term "p'"}; with @{term Kill} the

   430   intention is that the process @{term p} kills another process with

   431   ID @{term p'}. We will later give the definition what the role

   432   @{term r} can stand for in the constructor @{term ChangeRole}

   433   (namely \emph{normal roles} only). As is custom in Unix, there is no

   434   difference between a directory and a file. The files @{term f} in

   435   the definition above are simply lists of strings.  For example, the

   436   file @{text "/usr/bin/make"} is represented by the list @{text

   437   "[make, bin, usr]"} and the @{text root}-directory is the @{text

   438   Nil}-list. Following the presentation in \cite{ottrc}, our model of

   439   IPCs is rather simple-minded: we only have events for creation and deletion Of IPCs,

   440   as well as sending and receiving messages.

   441 

   442   Events essentially transform one state of the system into

   443   another. The system starts with an initial state determining which 

   444   processes, files and IPCs are active at the start of the system. We assume the

   445   users of the system are fixed in the initial state; we also assume

   446   that the policy does not change while the system is running. We have 

   447   three sets, namely

   448   @{term init_processes},

   449   @{term init_files} and

   450   @{term init_ipcs}

   451   specifying the processes, files and IPCs present in the initial state.

   452   We will often use the abbreviation

   453 

   454   \begin{center}

   455   @{thm (lhs) Init_def} @{text "\<equiv>"} 

   456   @{thm (rhs) Init_rhs(1)[where f=obj]} @{text "\<or>"}

   457   @{thm (rhs) Init_rhs(2)[where p=obj]} @{text "\<or>"}

   458   @{thm (rhs) Init_rhs(3)[where i=obj]}

   459   \end{center}

   460 

   461   \noindent

   462   There are some assumptions we make about the files present in the initial state: we always

   463   require that the @{text "root"}-directory @{term "[]"} is part of the initial state

   464   and for every file in the initial state (excluding @{term "[]"}) we require that its 

   465   parent is also part of the 

   466   initial state.

   467   After the initial state, the next states are determined

   468   by a list of events, called the \emph{trace}.  We need to define

   469   functions that allow us to make some observations about traces. One 

   470   such function is called @{term "current_procs"} and

   471   calculates the set of ``alive'' processes in a state:

   472 

   473   %initial state:

   474   %We make assumptions about the initial state, they're:

   475   %1. there exists a set of processes, files, IPCs and users already in the initial state,

   476   %users are not changed in system's running, we regards users adding and deleting a

   477   %administration task, not the issue for our policy checker; 

   478   %2. every object in the initial state have got already roles/types/owner ... information assigned;

   479   %3. all the policy information are already preloaded in the initial state, including:

   480   %a compatible type table, @{term compatible};

   481   %a mapping function from a role to its compatible role set, @{term comproles};

   482   %every role's default values is pre-set, e.g. default process create type and 

   483   %and default file/directory create type.

   484 

   485   \begin{isabelle}\ \ \ \ \ %%%

   486   \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

   487   @{thm (lhs) current_procs.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) current_procs.simps(1)}\\

   488   @{thm (lhs) current_procs.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) current_procs.simps(2)}\\

   489   @{thm (lhs) current_procs.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) current_procs.simps(3)}\\

   490   @{term "current_procs (DUMMY#s)"} & @{text "\<equiv>"} & @{term "current_procs s"}

   491   \end{tabular}}

   492   \end{isabelle}

   493     

   494   \noindent

   495   The first clause states that in the empty trace, that is initial

   496   state, the processes are given by @{text "init_processes"}. The 

   497   events for cloning a process, respectively killing a process, update this

   498   set of processes appropriately. Otherwise the set of live

   499   processes is unchanged. We have similar functions for alive files and 

   500   IPCs, called @{term "current_files"} and @{term "current_ipcs"}. 

   501 

   502   We can use these function in order to formally model which events are

   503   \emph{admissible} by the operating system in each state. We show just three 

   504   rules that give the gist of this definition. First the rule for changing 

   505   an owner of a process:

   506 

   507   \begin{center}

   508   @{thm[mode=Rule] osgrant6}

   509   \end{center}

   510 

   511   \noindent

   512   We require that the process @{text p} is alive in the state @{text s}

   513   (first premise) and that the new owner is a user that existed in the initial state

   514   (second premise).

   515   Next the rule for creating a new file:

   516 

   517   \begin{center}

   518   @{thm[mode=Rule] osgrant2}

   519   \end{center}

   520   

   521   \noindent

   522   It states that

   523   a file @{text f} can be created by a process @{text p} being alive in the state @{text s},

   524   the new file does not exist already in this state and there exists

   525   a parent file @{text "pf"} for the new file. The parent file is just

   526   the tail of the list representing @{text f}. % if it exists 

   527   %(@{text "Some"}-case) or @{text None} if it does not. 

   528   Finally, the rule for cloning a process:

   529 

   530   \begin{center}

   531   @{thm[mode=Rule] osgrant10}

   532   \end{center}

   533 

   534   \noindent

   535   Clearly the operating system should only allow to clone a process @{text p} if the 

   536   process is currently alive. The cloned process will get the process

   537   ID generated by the function @{term new_proc}. This process ID should

   538   not already exist. Therefore we define @{term new_proc} as

   539 

   540   \begin{isabelle}\ \ \ \ \ %%%

   541   \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l}

   542   @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"}

   543   \end{tabular}}

   544   \end{isabelle}

   545 

   546   \noindent

   547   namely the highest ID currently in existence increased by one. The 

   548   admissibility rules for the other events impose similar conditions.

   549 

   550   However, the admissibility check by the operating system is only one

   551   ``side'' of the constraints the RC-Model imposes. We also need to

   552   model the constraints of the access policy. For this we introduce

   553   separate @{text granted}-rules involving the sets @{text

   554   permissions} and @{text "compatible r"}: the former contains triples

   555   describing access control rules; the latter specifies for each role @{text r} 

   556   which roles are compatible with @{text r}. These sets are used in the

   557   RC-Model when a process having a role @{text r} takes on a new role

   558   @{text r'}. For example, a login-process might belong to root;

   559   once the user logs in, however, the role of the process should change to

   560   the user's default role. The corresponding @{text "granted"}-rule is

   561   as follows

   562 

   563   \begin{center}

   564   @{thm[mode=Rule] rcgrant7}

   565   \end{center}

   566   

   567   \noindent

   568   where we check whether the process @{text p} has currently role @{text r} and

   569   whether the RC-policy states that @{text r'} is in the role compatibility

   570   set of @{text r}. 

   571 

   572   The complication in the RC-Model arises from the

   573   way how the current role of a process in a state @{text s} is

   574   calculated---represented by the predicate @{term is_current_role} in our formalisation.  

   575   For defining this predicate we need to trace the role of a process from

   576   the initial state to the current state. In the

   577   initial state all processes have the role given by the function

   578   @{term "init_current_role"}.  If a @{term Clone} event happens then

   579   the new process will inherit the role from the parent

   580   process. Similarly, if a @{term ChangeRole} event happens, then 

   581   as seen in the rule above we just change the role accordingly. More interesting 

   582   is an @{term Execute} event in the RC-Model. For this event we have 

   583   to check the role attached to the file to be executed. 

   584   There are a number of cases: If the role of the file is a 

   585   \emph{normal} role, then the process will just take on this role 

   586   when executing the file (this is like the setuid mechanism in Unix). But 

   587   there are also four \emph{special} roles in the RC-Model:

   588   @{term "InheritProcessRole"}, @{term "InheritUserRole"}, 

   589    @{term "InheritParentRole"} and @{term

   590   InheritUpMixed}. For example, if a file to be executed has

   591   @{term "InheritProcessRole"} attached to it, then the process 

   592   that executes this file keeps its role regardless of the information 

   593   attached to the file. In this way programs can be can quarantined;

   594   @{term "InheritUserRole"} can be used for login shells

   595   to make sure they run with the user's default role.

   596   The purpose of the other special roles is to determine the

   597   role of a process according to the directory in which the

   598   files are stored.

   599 

   600   Having the notion of current role in place, we can define the

   601   granted rule for the @{term Execute}-event: Suppose a process @{term

   602   p} wants to execute a file @{text f}. The RC-Model first fetches the

   603   role @{text r} of this process (in the current state @{text s}) and

   604   the type @{text t} of the file. It then checks if the tuple @{term

   605   "(r, t, EXECUTE)"} is part of the policy, that is in our

   606   formalisation being an element in the set @{term compatible}. The

   607   corresponding rule is as follows

   608 

   609   \begin{center}

   610   @{thm[mode=Rule] rcgrant4}

   611   \end{center}

   612 

   613   \noindent

   614   The next @{text granted}-rule concerns the @{term CreateFile} event.

   615   If this event occurs, then we have two rules in our RC-Model

   616   depending on how the type of the created file is derived. If the type is inherited

   617   from the parent directory @{text pf}, then the @{term granted}-rule is as follows:

   618 

   619   \begin{center}

   620   @{thm[mode=Rule] rcgrant1} 

   621   \end{center}

   622 

   623   \noindent

   624   We check whether @{term pf} is the parent file (directory) of @{text f} and check

   625   whether the type of @{term pf} is @{term t}. We also need to fetch the 

   626   the role @{text r} of the process that seeks to get permission for creating 

   627   the file. If the default type of this role @{text r} states that the 

   628   type of the newly created file will be inherited from the parent file

   629   type, then we only need to check that the policy states that @{text r}

   630   has permission to write into the directory @{text pf}.

   631 

   632   The situation is different if the default type of role @{text r} is

   633   some \emph{normal} type, like text-file or executable. In such cases we want

   634   that the process creates some predetermined type of files. Therefore in the

   635   rule we have to check whether the role is allowed to create a file of that

   636   type, and also check whether the role is allowed to write any new

   637   file into the parent file (directory). The corresponding rule is

   638   as follows.

   639 

   640   \begin{center}

   641   @{thm[mode=Rule] rcgrant1'}

   642   \end{center}

   643   

   644   \noindent

   645   Interestingly, the type-information in the RC-model is also used for

   646   processes, for example when they need to change their owner. For

   647   this we have the rule

   648 

   649   \begin{center}

   650   @{thm[mode=Rule] rcgrant_CHO}

   651   \end{center}

   652 

   653   \noindent

   654   whereby we have to obtain both the role and type of the process @{term p}, and then check

   655   whether the policy allows a @{term ChangeOwner}-event for that role and type.

   656 

   657   Overall we have 13 rules for the admissibility check by the operating system and

   658   14 rules for the granted check by the RC-Model.  

   659   They are used to characterise when an event @{text e} is \emph{valid} to 

   660   occur in a state @{text s}. This can be inductively defined as the set of valid

   661   states.

   662 

   663   \begin{center}

   664   \begin{tabular}{@ {}c@ {}}

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

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

   667   \end{tabular}

   668   \end{center}  

   669 

   670   The novel notion we introduce in this paper is the @{text tainted} 

   671   relation. It characterises how a system can become infected when 

   672   a file in the system contains, for example, a virus. We assume

   673   that the initial state contains some tainted

   674   objects (we call them @{term "seeds"}). Therefore in the initial state @{term "[]"}

   675   an object is tainted, if it is an element in @{text "seeds"}.

   676 

   677   \begin{center}

   678   \mbox{@{thm [mode=Rule] tainted.intros(1)}}

   679   \end{center}

   680 

   681   \noindent

   682   Let us first assume such a tainted object is a file @{text f}.

   683   If a process reads or executes a tainted file, then this process becomes

   684   tainted (in the state where the corresponding event occurs).

   685 

   686   \begin{center}

   687   \mbox{@{thm [mode=Rule] tainted.intros(3)}}\hspace{3mm}

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

   689   \end{center}

   690 

   691   \noindent

   692   We have a similar rule for a tainted IPC, namely

   693 

   694   \begin{center}

   695   \mbox{@{thm [mode=Rule] tainted.intros(9)}}

   696   \end{center}

   697 

   698   \noindent

   699   which means if we receive anything from a tainted IPC, then

   700   the process becomes tainted. A process is also tainted 

   701   when it is a produced by a @{text Clone}-event.

   702 

   703   \begin{center}

   704   \mbox{@{thm [mode=Rule] tainted.intros(2)}}

   705   \end{center}

   706 

   707   \noindent

   708   However, the tainting relationship must also work in the 

   709   ``other'' direction, meaning if a process is tainted, then

   710   every file that is written or created will be tainted. 

   711   This is captured by the four rules:

   712 

   713   \begin{center}

   714   \begin{tabular}{c}

   715   \mbox{@{thm [mode=Rule] tainted.intros(4)}} \hspace{3mm}

   716   \mbox{@{thm [mode=Rule] tainted.intros(7)}} \medskip\\

   717   \mbox{@{thm [mode=Rule] tainted.intros(5)}} \hspace{3mm}

   718   \mbox{@{thm [mode=Rule] tainted.intros(8)}} 

   719   \end{tabular}

   720   \end{center}

   721   

   722   \noindent

   723   Finally, we have three rules that state whenever an object is tainted

   724   in a state @{text s}, then it will be still tainted in the 

   725   next state @{term "e#s"}, provided the object is still \emph{alive}

   726   in that state. We have such a rule for each kind of objects, for

   727   example for files the rule is:

   728 

   729   \begin{center}

   730   \mbox{@{thm [mode=Rule] tainted_10}} 

   731   \end{center}

   732 

   733   \noindent

   734   Similarly for alive processes and IPCs (then respectively with premises 

   735   @{term "p \<in> current_procs (e#s)"} and @{term "i \<in> current_ipcs (e#s)"}). 

   736   When an object present in the initial state can be tainted in 

   737   \emph{some} state (system run), we say it is @{text "taintable"}:

   738 

   739   \begin{isabelle}\ \ \ \ \ %%%

   740   \mbox{\begin{tabular}{lcl}

   741   @{thm (lhs) taintable_def} & @{text "\<equiv>"} & @{term "init obj"} @{text "\<and>"} @{thm (rhs) taintable_def}

   742   \end{tabular}}

   743   \end{isabelle}

   744 

   745   Before we can describe our static check deciding when a file is taintable, we

   746   need to describe the notions @{term deleted} and @{term undeletable}

   747   for objects. The former characterises whether there is an event that deletes  

   748   these objects (files, processes or IPCs). For this we have the following 

   749   four rules:

   750 

   751   \begin{center}

   752   \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}

   753   \begin{tabular}{c}

   754   @{thm [mode=Axiom] dels(1)}\\[-2mm]

   755   @{thm [mode=Axiom] dels(2)}\\[-2mm]

   756   @{thm [mode=Axiom] dels(3)}

   757   \end{tabular} &

   758   @{thm [mode=Rule] dels(4)}

   759   \end{tabular}

   760   \end{center}

   761 

   762 

   763   \noindent

   764   Note that an object cannot be deleted in the initial state @{text

   765   "[]"}.  An object is then said to be @{text "undeletable"} provided

   766   it did exist in the initial state and there does not exists a valid

   767   state in which the object is deleted:

   768   

   769   \begin{isabelle}\ \ \ \ \ %%%

   770   \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}

   771   @{thm (lhs) undeletable_def} & @{text "\<equiv>"} & %%@{thm (rhs) undeletable_def}

   772   @{term "init obj \<and> \<not>(\<exists> s. (valid s \<and> deleted obj s))"}

   773   \end{tabular}}

   774   \end{isabelle}

   775 

   776   \noindent

   777   The point of this definition is that our static taintable check will only be

   778   complete for undeletable objects. But these are

   779   the ones system administrators are typically interested in (for

   780   example system files).  It should be clear, however, that we cannot

   781   hope for a meaningful check by just trying out all possible

   782   valid states in our dynamic model. The reason is that there are

   783   potentially infinitely many of them and therefore the search space would be

   784   infinite.  For example staring from an

   785   initial state containing a process @{text p} and a file @{text pf}, 

   786   we can create files @{text "f\<^isub>1"}, @{text "f\<^isub>2"}, @{text "..."} 

   787   via @{text "CreateFile"}-events. This can be pictured roughly as follows:

   788 

   789   \begin{center}

   790   \begin{tabular}[t]{c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}c@ {\hspace{-8mm}}cc}

   791   \begin{tabular}[t]{c}

   792   Initial state:\\

   793   @{term "{p, pf}"}

   794   \end{tabular} &

   795   \begin{tabular}[t]{c}

   796   \\

   797   @{text "\<Longrightarrow>"}\\[2mm]

   798   {\small@{term "CreateFile p (f\<^isub>1#pf)"}}

   799   \end{tabular}

   800   &

   801   \begin{tabular}[t]{c}

   802   \\

   803   @{term "{p, pf, f\<^isub>1#pf}"}

   804   \end{tabular} 

   805   &

   806   \begin{tabular}[t]{c}

   807   \\

   808   @{text "\<Longrightarrow>"}\\[2mm]

   809   {\small@{term "CreateFile p (f\<^isub>2#f\<^isub>1#pf)"}}

   810   \end{tabular}

   811   &

   812   \begin{tabular}[t]{c}

   813   \\

   814   @{term "{p, pf, f\<^isub>1#pf, f\<^isub>2#f\<^isub>1#pf}"}

   815   \end{tabular} &

   816   \begin{tabular}[t]{c}

   817   \\

   818   @{text "..."}\\

   819   \end{tabular}

   820   \end{tabular}

   821   \end{center}

   822 

   823   \noindent

   824   Instead, the idea of our static check is to use

   825   the policies of the RC-model for generating an answer, since they

   826   provide always a finite ``description of the system''. As we 

   827   will see in the next section, this needs some care, however.

   828 *}

   829 

   830 section {* Our Static Check *}

   831 

   832 text {*

   833   Assume there is a tainted file in the system and suppose we face the

   834   problem of finding out whether this file can affect other files,

   835   IPCs or processes? One idea is to work on the level of policies only, and

   836   check which operations are permitted by the role and type of this

   837   file. Then one builds the ``transitive closure'' of this information

   838   and checks for example whether the role @{text root} has become

   839   affected, in which case the whole system is compromised.  This is indeed the solution investigated

   840   in~\cite{guttman2005verifying} in the context of information flow

   841   and SELinux.

   842 

   843   Unfortunately, restricting the calculations to only use policies is

   844   too simplistic for obtaining a check that is sound and complete---it

   845   over-approximates the dynamic tainted relation defined in the previous

   846   section. To see the problem consider

   847   the case where the tainted file has, say, the type @{text bin}. If

   848   the RC-policy contains a role @{text r} that can both read and write

   849   @{text bin}-files, we would conclude that all @{text bin}-files can potentially 

   850   be tainted. That

   851   is indeed the case, \emph{if} there is a process having this role @{text

   852   r} running in the system. But if there is \emph{not}, then the

   853   tainted file cannot ``spread''.  A similar problem arises in case there

   854   are two processes having the same role @{text r},  and this role is

   855   restricted to read files only.  Now if one of the processes is tainted, then

   856   the simple check involving only policies would incorrectly infer

   857   that all processes involving that role are tainted. But since the

   858   policy for @{text r} is restricted to be read-only, there is in fact

   859   no danger that both processes can become tainted.

   860 

   861   The main idea of our sound and complete check is to find a ``middle'' ground between

   862   the potentially infinite dynamic model and the too coarse

   863   information contained in the RC-policies. Our solution is to

   864   define a ``static'' version of the tainted relation, called @{term

   865   "tainted_s"}, that records relatively precisely the information

   866   about the initial state of the system (the one in which an object

   867   might be a @{term seed} and therefore tainted). However,

   868   we are less precise about the objects created in every subsequent

   869   state. The result is that we can avoid the potential infinity of

   870   the dynamic model. 

   871   For the @{term tainted_s}-relation we will consider the following 

   872   three kinds of \emph{items} recording the information we need about

   873   processes, files and IPCs, respectively:

   874 

   875   \begin{center}

   876   \begin{tabular}{l@ {\hspace{5mm}}l}

   877   & Recorded information:\smallskip\\

   878   Processes: & @{term "SProc (r, dr, t, u) po"}\\

   879   Files: & @{term "SFile (t, a) fo"}\\

   880   IPCs: & @{term "SIPC (t) io"}

   881   \end{tabular}

   882   \end{center}

   883   

   884   \noindent

   885   For a process we record its role @{text r}, its default role @{text dr} (used to determine

   886   the role when executing a file or changing the owner of a process), its type @{text t} 

   887   and its owner @{text u}. For a file we record

   888   just the type @{text t} and its @{term "source_dir"} @{text a} (we define this

   889   notion shortly). For IPCs we only record its type @{text t}. Note the superscripts

   890   @{text po}, @{text fo} and @{text io} in each item. They are optional arguments and depend on

   891   whether the corresponding object is present in the initial state or not.

   892   If it \emph{is}, then for processes and IPCs we will record @{term "Some(id)"},

   893   where @{text id} is the natural number that uniquely identifies a process or IPC;

   894   for files we just record their path @{term "Some(f)"}. If the object is

   895   \emph{not} present in the initial state, that is newly created, then we just have

   896   @{term None} as superscript. 

   897   Let us illustrate the different superscripts with the following example

   898   where the initial state contains a process @{term p} and a file (directory)

   899   @{term pf}. Then this

   900   process creates a file via a @{term "CreateFile"}-event and after that reads

   901   the created file via a @{term Read}-event:

   902 

   903   \begin{center}

   904   \begin{tabular}[t]{ccccc}

   905   \begin{tabular}[t]{c}

   906   Initial state:\\

   907   @{term "{p, pf}"}

   908   \end{tabular} &

   909   \begin{tabular}[t]{c}

   910   \\

   911   @{text "\<Longrightarrow>"}\\

   912   {\small@{term "CreateFile p (f#pf)"}}

   913   \end{tabular}

   914   &

   915   \begin{tabular}[t]{c}

   916   \\

   917   @{term "{p, pf, f#pf}"}

   918   \end{tabular} 

   919   &

   920   \begin{tabular}[t]{c}

   921   \\

   922   @{text "\<Longrightarrow>"}\\

   923   {\small@{term "ReadFile p (f#pf)"}}

   924   \end{tabular}

   925   &

   926   \begin{tabular}[t]{c}

   927   \\

   928   @{term "{p, pf, f#pf}"}

   929   \end{tabular} 

   930   \end{tabular}

   931   \end{center}

   932 

   933   \noindent

   934   For the two objects in the initial state our static check records

   935   the information @{term "SProc (r, dr, t, u) (Some(p))"} and @{term

   936   "SFile (t', a) (Some(pf))"} (assuming @{text "r"}, @{text t} and so

   937   on are the corresponding roles, types etc).  In both cases we have

   938   the superscript @{text "Some(...)"}  since they are objects present

   939   in the initial state. For the file @{term "f#pf"} created by the

   940   @{term "CreateFile"}-event, we record @{term "SFile (t', a')

   941   (None)"}, since it is a newly created file.  The @{text

   942   "ReadFile"}-event does not change the set of objects, therefore no

   943   new information needs to be recorded. The problem we are avoiding

   944   with this setup of recording the precise information for the initial

   945   state is where two processes have the same role and type

   946   information, but only one is tainted in the initial state, but the

   947   other is not. The recorded unique process IDs allows us to

   948   distinguish between both processes.  For all newly created objects,

   949   on the other hand, we do not care.  This is crucial, because

   950   otherwise exploring all possible ``reachable'' objects can lead to

   951   the potential infinity like in the dynamic model.

   952 

   953   An @{term source_dir} for a file is the ``nearest'' directory that

   954   is present in the initial state and has not been deleted in a state

   955   @{text s}. Its definition is the recursive function

   956   

   957   \begin{isabelle}\ \ \ \ \ %%%

   958   \mbox{\begin{tabular}{lcl}

   959   @{thm (lhs) source_dir.simps(1)} & @{text "\<equiv>"} \;\; &

   960   @{text "if"} @{text "\<not> deleted [] s"} @{text "then"} @{term "Some []"} @{text "else"} @{term "None"}\\

   961   @{thm (lhs) source_dir.simps(2)} & @{text "\<equiv>"} & 

   962   @{text "if"} @{term "(f#pf) \<in> init_files \<and> \<not>(deleted (File (f#pf)) s)"}\\

   963   & & @{text "then"} @{term "Some (f#pf)"} @{text "else"} @{term "source_dir s pf"}\\

   964   \end{tabular}}

   965   \end{isabelle}

   966   

   967   \noindent

   968   generating an optional value.

   969   The first clause states that the anchor of the @{text

   970   root}-directory is always its own anchor unless it has been

   971   deleted. If a file is present in the initial state and not deleted

   972   in @{text s}, then it is also its own anchor, otherwise the anchor

   973   will be the anchor of the parent directory.  For example if we have

   974   a directory @{text pf} in the initial state, then its anchor is @{text "Some pf"}

   975   (assuming it is not deleted). If we create a new file in this directory,

   976   say @{term "f#pf"}, then its anchor will also be @{text "Some pf"}.

   977   The purpose of @{term source_dir} is to determine the

   978   role information when a file is executed, because the role of the

   979   corresponding process, according to the RC-model, is determined by the role information of the

   980   anchor of the file to be executed.

   981 

   982   There is one last problem we have to solve before we can give the

   983   rules of our @{term "tainted_s"}-check. Suppose an RC-policy 

   984   includes the rule @{text "(r, foo, Write) \<in> permissions"}, that is

   985   a process of role @{text "r"} is allowed to write files of type @{text "foo"}.

   986   If there is a tainted process with this role, we would conclude that

   987   also every file of that type can potentially become tainted. However, that

   988   is not the case if the initial state does not contain any file

   989   with type @{text foo} and the RC-policy does not allow the

   990   creation of such files, that is does not contain an access rule

   991   @{text "(r, foo, Create) \<in> permissions"}. In a sense the original

   992   @{text "(r, foo, Write)"} is ``useless'' and should not contribute

   993   to the relation characterising the objects that are tainted.

   994   To exclude such ``useless'' access rules, we define

   995   a relation @{term "all_sobjs"} restricting our search space 

   996   to only configurations that correspond to states in our dynamic model.

   997   We first have a rule for reachable items of the form  @{text "F(t, f)\<^bsup>Some f\<^esup>"}

   998   where the file @{text f} with type @{text t} is present in 

   999   the initial state. 

  1000 

  1001   \begin{center}

  1002   @{thm [mode=Rule] af_init'}

  1003   \end{center}

  1004 

  1005   \noindent

  1006   We have similar reachability rules for processes and IPCs that are part of the 

  1007   initial state. Next is the reachability rule in case a file is created

  1008 

  1009   \begin{center}

  1010   @{thm [mode=Rule] af_cfd[where sd=a and sf="fo" and sp="po" and fr="dr"]}

  1011   \end{center}

  1012 

  1013   \noindent

  1014   where we require that we have a reachable parent directory, recorded

  1015   as @{text "F(t, a)\<^bsup>fo\<^esup>"}, and also a

  1016   process that can create the file, recorded as @{text "P(r, dr, pt,

  1017   u)\<^bsup>po\<^esup>"}. As can be seen, we also require that we have both @{text "(r, t,

  1018   Write)"} and \mbox{@{text "(r, t', Create)"}} in the @{text permissions} set 

  1019   for this rule to apply. If we did \emph{not} impose this requirement

  1020   about the RC-policy, then there would be no way to create a file

  1021   with @{term "NormalFileType t'"} according to our ``dynamic'' model. 

  1022   However in case we want to create a 

  1023   file of type @{term InheritPatentType}, then we only need the access-rule

  1024   @{text "(r, t, Write)"}: 

  1025   

  1026   \begin{center}

  1027   @{thm [mode=Rule] af_cfd'[where sd=a and sf="fo" and sp="po" and fr="dr"]}

  1028   \end{center}

  1029 

  1030   \noindent

  1031   We also have reachability rules for processes executing files, and

  1032   for changing their roles and owners, for example

  1033 

  1034   \begin{center}

  1035   @{thm [mode=Rule] ap_crole[where sp="po" and fr="dr"]}

  1036   \end{center}

  1037 

  1038   \noindent

  1039   which states that when we have a process with role @{text r}, and the role

  1040   @{text "r'"} is in the corresponding role-compatibility set, then also

  1041   a process with role @{text "r'"} is reachable.

  1042 

  1043   The crucial difference between between the ``dynamic'' notion of validity 

  1044   and the ``static'' notion of @{term "all_sobjs"}

  1045   is that there can be infinitely many valid states, but assuming the initial

  1046   state contains only finitely many objects, then also @{term "all_sobjs"} will 

  1047   be finite. To see the difference, consider the infinite ``chain'' of events 

  1048   just cloning a process @{text "p\<^isub>0"}:

  1049 

  1050   \begin{center}

  1051   \begin{tabular}[t]{c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}c@ {\hspace{-2mm}}cc}

  1052   \begin{tabular}[t]{c}

  1053   Initial state:\\

  1054   @{term "{p\<^isub>0}"}

  1055   \end{tabular} &

  1056   \begin{tabular}[t]{c}

  1057   \\

  1058   @{text "\<Longrightarrow>"}\\[2mm]

  1059   {\small@{term "Clone p\<^isub>0 p\<^isub>1"}}

  1060   \end{tabular}

  1061   &

  1062   \begin{tabular}[t]{c}

  1063   \\

  1064   @{term "{p\<^isub>0, p\<^isub>1}"}

  1065   \end{tabular} 

  1066   &

  1067   \begin{tabular}[t]{c}

  1068   \\

  1069   @{text "\<Longrightarrow>"}\\[2mm]

  1070   {\small@{term "Clone p\<^isub>0 p\<^isub>2"}}

  1071   \end{tabular}

  1072   &

  1073   \begin{tabular}[t]{c}

  1074   \\

  1075   @{term "{p\<^isub>0, p\<^isub>1, p\<^isub>2}"}

  1076   \end{tabular} &

  1077   \begin{tabular}[t]{c}

  1078   \\

  1079   @{text "..."}\\

  1080   \end{tabular}

  1081   \end{tabular}

  1082   \end{center}

  1083 

  1084   \noindent

  1085   The corresponding reachable objects are

  1086 

  1087   \begin{center}

  1088   \begin{tabular}[t]{cccc}

  1089   \begin{tabular}[t]{c}

  1090   @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>}"}

  1091   \end{tabular} &

  1092   \begin{tabular}[t]{c}

  1093   @{text "\<Longrightarrow>"}

  1094   \end{tabular}

  1095   &

  1096   \begin{tabular}[t]{c}

  1097   @{text "{P(r, dr, t, u)\<^bsup>Some (p\<^isub>0)\<^esup>, P(r, dr, t, u)\<^bsup>None\<^esup>}"}

  1098   \end{tabular} 

  1099   \end{tabular}

  1100   \end{center}

  1101 

  1102   \noindent

  1103   where no further progress can be made because the information

  1104   recorded about @{text "p\<^isub>2"}, @{text "p\<^isub>3"} and so on is just the same

  1105   as for @{text "p\<^isub>1"}, namely @{text "P(r, dr, t, u)\<^bsup>None\<^esup>"}.  Indeed we

  1106   can prove the lemma:

  1107 

  1108   \begin{lemma}\label{finite}

  1109   If @{text "finite init"}, then @{term "finite all_sobjs"}.

  1110   \end{lemma}

  1111 

  1112   \noindent

  1113   This fact of @{term all_sobjs} being finite enables us to design a

  1114   decidable tainted-check. For this we introduce inductive rules defining the

  1115   set @{term "tainted_s"}. Like in the ``dynamic'' version of tainted,

  1116   if an object is element of @{text seeds}, then it is @{term "tainted_s"}.

  1117 

  1118   \begin{center}

  1119   @{thm [mode=Rule] ts_init}

  1120   \end{center}

  1121 

  1122   \noindent

  1123   The function @{text "\<lbrakk>_\<rbrakk>"} extracts the static information from an object.

  1124   For example for a process it extracts the role, default role, type and

  1125   user; for a file the type and the anchor. If a process in tainted and creates

  1126   a file with a normal type @{text "t'"} then also the created file

  1127   is tainted. The corresponding rule is

  1128 

  1129   \begin{center}

  1130   @{thm [mode=Rule] ts_cfd[where sd=a and sf="fo" and sp="po" and fr="dr"]}

  1131   \end{center}

  1132 

  1133   \noindent

  1134   If a tainted process  creates a file that inherits the type of the directory,

  1135   then the file will also be tainted: