src/HOL/Unix/Unix.thy
author huffman
Thu Aug 11 09:11:15 2011 -0700 (2011-08-11)
changeset 44165 d26a45f3c835
parent 43433 f67364f35789
child 44236 b73b7832b384
permissions -rw-r--r--
remove lemma stupid_ext
     1 (*  Title:      HOL/Unix/Unix.thy
     2     Author:     Markus Wenzel, TU Muenchen
     3 *)
     4 
     5 header {* Unix file-systems \label{sec:unix-file-system} *}
     6 
     7 theory Unix
     8 imports
     9   Main
    10   "~~/src/HOL/Library/Nested_Environment"
    11   "~~/src/HOL/Library/List_Prefix"
    12 begin
    13 
    14 text {*
    15   We give a simple mathematical model of the basic structures
    16   underlying the Unix file-system, together with a few fundamental
    17   operations that could be imagined to be performed internally by the
    18   Unix kernel.  This forms the basis for the set of Unix system-calls
    19   to be introduced later (see \secref{sec:unix-trans}), which are the
    20   actual interface offered to processes running in user-space.
    21 
    22   \medskip Basically, any Unix file is either a \emph{plain file} or a
    23   \emph{directory}, consisting of some \emph{content} plus
    24   \emph{attributes}.  The content of a plain file is plain text.  The
    25   content of a directory is a mapping from names to further
    26   files.\footnote{In fact, this is the only way that names get
    27   associated with files.  In Unix files do \emph{not} have a name in
    28   itself.  Even more, any number of names may be associated with the
    29   very same file due to \emph{hard links} (although this is excluded
    30   from our model).}  Attributes include information to control various
    31   ways to access the file (read, write etc.).
    32 
    33   Our model will be quite liberal in omitting excessive detail that is
    34   easily seen to be ``irrelevant'' for the aspects of Unix
    35   file-systems to be discussed here.  First of all, we ignore
    36   character and block special files, pipes, sockets, hard links,
    37   symbolic links, and mount points.
    38 *}
    39 
    40 
    41 subsection {* Names *}
    42 
    43 text {*
    44   User ids and file name components shall be represented by natural
    45   numbers (without loss of generality).  We do not bother about
    46   encoding of actual names (e.g.\ strings), nor a mapping between user
    47   names and user ids as would be present in a reality.
    48 *}
    49 
    50 type_synonym uid = nat
    51 type_synonym name = nat
    52 type_synonym path = "name list"
    53 
    54 
    55 subsection {* Attributes *}
    56 
    57 text {*
    58   Unix file attributes mainly consist of \emph{owner} information and
    59   a number of \emph{permission} bits which control access for
    60   ``user'', ``group'', and ``others'' (see the Unix man pages @{text
    61   "chmod(2)"} and @{text "stat(2)"} for more details).
    62 
    63   \medskip Our model of file permissions only considers the ``others''
    64   part.  The ``user'' field may be omitted without loss of overall
    65   generality, since the owner is usually able to change it anyway by
    66   performing @{text chmod}.\footnote{The inclined Unix expert may try
    67   to figure out some exotic arrangements of a real-world Unix
    68   file-system such that the owner of a file is unable to apply the
    69   @{text chmod} system call.}  We omit ``group'' permissions as a
    70   genuine simplification as we just do not intend to discuss a model
    71   of multiple groups and group membership, but pretend that everyone
    72   is member of a single global group.\footnote{A general HOL model of
    73   user group structures and related issues is given in
    74   \cite{Naraschewski:2001}.}
    75 *}
    76 
    77 datatype perm =
    78     Readable
    79   | Writable
    80   | Executable    -- "(ignored)"
    81 
    82 type_synonym perms = "perm set"
    83 
    84 record att =
    85   owner :: uid
    86   others :: perms
    87 
    88 text {*
    89   For plain files @{term Readable} and @{term Writable} specify read
    90   and write access to the actual content, i.e.\ the string of text
    91   stored here.  For directories @{term Readable} determines if the set
    92   of entry names may be accessed, and @{term Writable} controls the
    93   ability to create or delete any entries (both plain files or
    94   sub-directories).
    95 
    96   As another simplification, we ignore the @{term Executable}
    97   permission altogether.  In reality it would indicate executable
    98   plain files (also known as ``binaries''), or control actual lookup
    99   of directory entries (recall that mere directory browsing is
   100   controlled via @{term Readable}).  Note that the latter means that
   101   in order to perform any file-system operation whatsoever, all
   102   directories encountered on the path would have to grant @{term
   103   Executable}.  We ignore this detail and pretend that all directories
   104   give @{term Executable} permission to anybody.
   105 *}
   106 
   107 
   108 subsection {* Files *}
   109 
   110 text {*
   111   In order to model the general tree structure of a Unix file-system
   112   we use the arbitrarily branching datatype @{typ "('a, 'b, 'c) env"}
   113   from the standard library of Isabelle/HOL
   114   \cite{Bauer-et-al:2002:HOL-Library}.  This type provides
   115   constructors @{term Val} and @{term Env} as follows:
   116 
   117   \medskip
   118   {\def\isastyleminor{\isastyle}
   119   \begin{tabular}{l}
   120   @{term [source] "Val :: 'a \<Rightarrow> ('a, 'b, 'c) env"} \\
   121   @{term [source] "Env :: 'b \<Rightarrow> ('c \<Rightarrow> ('a, 'b, 'c) env option) \<Rightarrow> ('a, 'b, 'c) env"} \\
   122   \end{tabular}}
   123   \medskip
   124 
   125   Here the parameter @{typ 'a} refers to plain values occurring at
   126   leaf positions, parameter @{typ 'b} to information kept with inner
   127   branch nodes, and parameter @{typ 'c} to the branching type of the
   128   tree structure.  For our purpose we use the type instance with @{typ
   129   "att \<times> string"} (representing plain files), @{typ att} (for
   130   attributes of directory nodes), and @{typ name} (for the index type
   131   of directory nodes).
   132 *}
   133 
   134 type_synonym "file" = "(att \<times> string, att, name) env"
   135 
   136 text {*
   137   \medskip The HOL library also provides @{term lookup} and @{term
   138   update} operations for general tree structures with the subsequent
   139   primitive recursive characterizations.
   140 
   141   \medskip
   142   {\def\isastyleminor{\isastyle}
   143   \begin{tabular}{l}
   144   @{term [source] "lookup :: ('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"} \\
   145   @{term [source]
   146   "update :: 'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"} \\
   147   \end{tabular}}
   148 
   149   @{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]}
   150   @{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]}
   151 
   152   Several further properties of these operations are proven in
   153   \cite{Bauer-et-al:2002:HOL-Library}.  These will be routinely used
   154   later on without further notice.
   155 
   156   \bigskip Apparently, the elements of type @{typ "file"} contain an
   157   @{typ att} component in either case.  We now define a few auxiliary
   158   operations to manipulate this field uniformly, following the
   159   conventions for record types in Isabelle/HOL
   160   \cite{Nipkow-et-al:2000:HOL}.
   161 *}
   162 
   163 definition
   164   "attributes file =
   165     (case file of
   166       Val (att, text) \<Rightarrow> att
   167     | Env att dir \<Rightarrow> att)"
   168 
   169 definition
   170   "map_attributes f file =
   171     (case file of
   172       Val (att, text) \<Rightarrow> Val (f att, text)
   173     | Env att dir \<Rightarrow> Env (f att) dir)"
   174 
   175 lemma [simp]: "attributes (Val (att, text)) = att"
   176   by (simp add: attributes_def)
   177 
   178 lemma [simp]: "attributes (Env att dir) = att"
   179   by (simp add: attributes_def)
   180 
   181 lemma [simp]: "attributes (map_attributes f file) = f (attributes file)"
   182   by (cases "file") (simp_all add: attributes_def map_attributes_def
   183     split_tupled_all)
   184 
   185 lemma [simp]: "map_attributes f (Val (att, text)) = Val (f att, text)"
   186   by (simp add: map_attributes_def)
   187 
   188 lemma [simp]: "map_attributes f (Env att dir) = Env (f att) dir"
   189   by (simp add: map_attributes_def)
   190 
   191 
   192 subsection {* Initial file-systems *}
   193 
   194 text {*
   195   Given a set of \emph{known users} a file-system shall be initialized
   196   by providing an empty home directory for each user, with read-only
   197   access for everyone else.  (Note that we may directly use the user
   198   id as home directory name, since both types have been identified.)
   199   Certainly, the very root directory is owned by the super user (who
   200   has user id 0).
   201 *}
   202 
   203 definition
   204   "init users =
   205     Env \<lparr>owner = 0, others = {Readable}\<rparr>
   206       (\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> empty)
   207         else None)"
   208 
   209 
   210 subsection {* Accessing file-systems *}
   211 
   212 text {*
   213   The main internal file-system operation is access of a file by a
   214   user, requesting a certain set of permissions.  The resulting @{typ
   215   "file option"} indicates if a file had been present at the
   216   corresponding @{typ path} and if access was granted according to the
   217   permissions recorded within the file-system.
   218 
   219   Note that by the rules of Unix file-system security (e.g.\
   220   \cite{Tanenbaum:1992}) both the super-user and owner may always
   221   access a file unconditionally (in our simplified model).
   222 *}
   223 
   224 definition
   225   "access root path uid perms =
   226     (case lookup root path of
   227       None \<Rightarrow> None
   228     | Some file \<Rightarrow>
   229         if uid = 0
   230           \<or> uid = owner (attributes file)
   231           \<or> perms \<subseteq> others (attributes file)
   232         then Some file
   233         else None)"
   234 
   235 text {*
   236   \medskip Successful access to a certain file is the main
   237   prerequisite for system-calls to be applicable (cf.\
   238   \secref{sec:unix-trans}).  Any modification of the file-system is
   239   then performed using the basic @{term update} operation.
   240 
   241   \medskip We see that @{term access} is just a wrapper for the basic
   242   @{term lookup} function, with additional checking of
   243   attributes. Subsequently we establish a few auxiliary facts that
   244   stem from the primitive @{term lookup} used within @{term access}.
   245 *}
   246 
   247 lemma access_empty_lookup: "access root path uid {} = lookup root path"
   248   by (simp add: access_def split: option.splits)
   249 
   250 lemma access_some_lookup:
   251   "access root path uid perms = Some file \<Longrightarrow>
   252     lookup root path = Some file"
   253   by (simp add: access_def split: option.splits if_splits)
   254 
   255 lemma access_update_other:
   256   assumes parallel: "path' \<parallel> path"
   257   shows "access (update path' opt root) path uid perms = access root path uid perms"
   258 proof -
   259   from parallel obtain y z xs ys zs where
   260       "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"
   261     by (blast dest: parallel_decomp)
   262   then have "lookup (update path' opt root) path = lookup root path"
   263     by (blast intro: lookup_update_other)
   264   then show ?thesis by (simp only: access_def)
   265 qed
   266 
   267 
   268 section {* File-system transitions \label{sec:unix-trans} *}
   269 
   270 subsection {* Unix system calls \label{sec:unix-syscall} *}
   271 
   272 text {*
   273   According to established operating system design (cf.\
   274   \cite{Tanenbaum:1992}) user space processes may only initiate system
   275   operations by a fixed set of \emph{system-calls}.  This enables the
   276   kernel to enforce certain security policies in the first
   277   place.\footnote{Incidently, this is the very same principle employed
   278   by any ``LCF-style'' theorem proving system according to Milner's
   279   principle of ``correctness by construction'', such as Isabelle/HOL
   280   itself.}
   281 
   282   \medskip In our model of Unix we give a fixed datatype @{text
   283   operation} for the syntax of system-calls, together with an
   284   inductive definition of file-system state transitions of the form
   285   @{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics.
   286 *}
   287 
   288 datatype operation =
   289     Read uid string path
   290   | Write uid string path
   291   | Chmod uid perms path
   292   | Creat uid perms path
   293   | Unlink uid path
   294   | Mkdir uid perms path
   295   | Rmdir uid path
   296   | Readdir uid "name set" path
   297 
   298 text {*
   299   The @{typ uid} field of an operation corresponds to the
   300   \emph{effective user id} of the underlying process, although our
   301   model never mentions processes explicitly.  The other parameters are
   302   provided as arguments by the caller; the @{term path} one is common
   303   to all kinds of system-calls.
   304 *}
   305 
   306 primrec
   307   uid_of :: "operation \<Rightarrow> uid"
   308 where
   309     "uid_of (Read uid text path) = uid"
   310   | "uid_of (Write uid text path) = uid"
   311   | "uid_of (Chmod uid perms path) = uid"
   312   | "uid_of (Creat uid perms path) = uid"
   313   | "uid_of (Unlink uid path) = uid"
   314   | "uid_of (Mkdir uid path perms) = uid"
   315   | "uid_of (Rmdir uid path) = uid"
   316   | "uid_of (Readdir uid names path) = uid"
   317 
   318 primrec
   319   path_of :: "operation \<Rightarrow> path"
   320 where
   321     "path_of (Read uid text path) = path"
   322   | "path_of (Write uid text path) = path"
   323   | "path_of (Chmod uid perms path) = path"
   324   | "path_of (Creat uid perms path) = path"
   325   | "path_of (Unlink uid path) = path"
   326   | "path_of (Mkdir uid perms path) = path"
   327   | "path_of (Rmdir uid path) = path"
   328   | "path_of (Readdir uid names path) = path"
   329 
   330 text {*
   331   \medskip Note that we have omitted explicit @{text Open} and @{text
   332   Close} operations, pretending that @{term Read} and @{term Write}
   333   would already take care of this behind the scenes.  Thus we have
   334   basically treated actual sequences of real system-calls @{text
   335   "open"}--@{text read}/@{text write}--@{text close} as atomic.
   336 
   337   In principle, this could make big a difference in a model with
   338   explicit concurrent processes.  On the other hand, even on a real
   339   Unix system the exact scheduling of concurrent @{text "open"} and
   340   @{text close} operations does \emph{not} directly affect the success
   341   of corresponding @{text read} or @{text write}.  Unix allows several
   342   processes to have files opened at the same time, even for writing!
   343   Certainly, the result from reading the contents later may be hard to
   344   predict, but the system-calls involved here will succeed in any
   345   case.
   346 
   347   \bigskip The operational semantics of system calls is now specified
   348   via transitions of the file-system configuration.  This is expressed
   349   as an inductive relation (although there is no actual recursion
   350   involved here).
   351 *}
   352 
   353 inductive
   354   transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
   355     ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
   356 where
   357 
   358   read:
   359     "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
   360       root \<midarrow>(Read uid text path)\<rightarrow> root" |
   361   "write":
   362     "access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow>
   363       root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root" |
   364 
   365   chmod:
   366     "access root path uid {} = Some file \<Longrightarrow>
   367       uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow>
   368       root \<midarrow>(Chmod uid perms path)\<rightarrow> update path
   369         (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root" |
   370 
   371   creat:
   372     "path = parent_path @ [name] \<Longrightarrow>
   373       access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
   374       access root path uid {} = None \<Longrightarrow>
   375       root \<midarrow>(Creat uid perms path)\<rightarrow> update path
   376         (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root" |
   377   unlink:
   378     "path = parent_path @ [name] \<Longrightarrow>
   379       access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
   380       access root path uid {} = Some (Val plain) \<Longrightarrow>
   381       root \<midarrow>(Unlink uid path)\<rightarrow> update path None root" |
   382 
   383   mkdir:
   384     "path = parent_path @ [name] \<Longrightarrow>
   385       access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
   386       access root path uid {} = None \<Longrightarrow>
   387       root \<midarrow>(Mkdir uid perms path)\<rightarrow> update path
   388         (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root" |
   389   rmdir:
   390     "path = parent_path @ [name] \<Longrightarrow>
   391       access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
   392       access root path uid {} = Some (Env att' empty) \<Longrightarrow>
   393       root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root" |
   394 
   395   readdir:
   396     "access root path uid {Readable} = Some (Env att dir) \<Longrightarrow>
   397       names = dom dir \<Longrightarrow>
   398       root \<midarrow>(Readdir uid names path)\<rightarrow> root"
   399 
   400 text {*
   401   \medskip Certainly, the above specification is central to the whole
   402   formal development.  Any of the results to be established later on
   403   are only meaningful to the outside world if this transition system
   404   provides an adequate model of real Unix systems.  This kind of
   405   ``reality-check'' of a formal model is the well-known problem of
   406   \emph{validation}.
   407 
   408   If in doubt, one may consider to compare our definition with the
   409   informal specifications given the corresponding Unix man pages, or
   410   even peek at an actual implementation such as
   411   \cite{Torvalds-et-al:Linux}.  Another common way to gain confidence
   412   into the formal model is to run simple simulations (see
   413   \secref{sec:unix-examples}), and check the results with that of
   414   experiments performed on a real Unix system.
   415 *}
   416 
   417 
   418 subsection {* Basic properties of single transitions \label{sec:unix-single-trans} *}
   419 
   420 text {*
   421   The transition system @{text "root \<midarrow>x\<rightarrow> root'"} defined above
   422   determines a unique result @{term root'} from given @{term root} and
   423   @{term x} (this is holds rather trivially, since there is even only
   424   one clause for each operation).  This uniqueness statement will
   425   simplify our subsequent development to some extent, since we only
   426   have to reason about a partial function rather than a general
   427   relation.
   428 *}
   429 
   430 theorem transition_uniq:
   431   assumes root': "root \<midarrow>x\<rightarrow> root'"
   432     and root'': "root \<midarrow>x\<rightarrow> root''"
   433   shows "root' = root''"
   434   using root''
   435 proof cases
   436   case read
   437   with root' show ?thesis by cases auto
   438 next
   439   case "write"
   440   with root' show ?thesis by cases auto
   441 next
   442   case chmod
   443   with root' show ?thesis by cases auto
   444 next
   445   case creat
   446   with root' show ?thesis by cases auto
   447 next
   448   case unlink
   449   with root' show ?thesis by cases auto
   450 next
   451   case mkdir
   452   with root' show ?thesis by cases auto
   453 next
   454   case rmdir
   455   with root' show ?thesis by cases auto
   456 next
   457   case readdir
   458   with root' show ?thesis by cases fastsimp+
   459 qed
   460 
   461 text {*
   462   \medskip Apparently, file-system transitions are \emph{type-safe} in
   463   the sense that the result of transforming an actual directory yields
   464   again a directory.
   465 *}
   466 
   467 theorem transition_type_safe:
   468   assumes tr: "root \<midarrow>x\<rightarrow> root'"
   469     and inv: "\<exists>att dir. root = Env att dir"
   470   shows "\<exists>att dir. root' = Env att dir"
   471 proof (cases "path_of x")
   472   case Nil
   473   with tr inv show ?thesis
   474     by cases (auto simp add: access_def split: if_splits)
   475 next
   476   case Cons
   477   from tr obtain opt where
   478       "root' = root \<or> root' = update (path_of x) opt root"
   479     by cases auto
   480   with inv Cons show ?thesis
   481     by (auto simp add: update_eq split: list.splits)
   482 qed
   483 
   484 text {*
   485   The previous result may be seen as the most basic invariant on the
   486   file-system state that is enforced by any proper kernel
   487   implementation.  So user processes --- being bound to the
   488   system-call interface --- may never mess up a file-system such that
   489   the root becomes a plain file instead of a directory, which would be
   490   a strange situation indeed.
   491 *}
   492 
   493 
   494 subsection {* Iterated transitions *}
   495 
   496 text {*
   497   Iterated system transitions via finite sequences of system
   498   operations are modeled inductively as follows.  In a sense, this
   499   relation describes the cumulative effect of the sequence of
   500   system-calls issued by a number of running processes over a finite
   501   amount of time.
   502 *}
   503 
   504 inductive
   505   transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
   506     ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
   507 where
   508     nil: "root =[]\<Rightarrow> root"
   509   | cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''"
   510 
   511 text {*
   512   \medskip We establish a few basic facts relating iterated
   513   transitions with single ones, according to the recursive structure
   514   of lists.
   515 *}
   516 
   517 lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')"
   518 proof
   519   assume "root =[]\<Rightarrow> root'"
   520   then show "root = root'" by cases simp_all
   521 next
   522   assume "root = root'"
   523   then show "root =[]\<Rightarrow> root'" by (simp only: transitions.nil)
   524 qed
   525 
   526 lemma transitions_cons_eq:
   527   "root =(x # xs)\<Rightarrow> root'' = (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root'')"
   528 proof
   529   assume "root =(x # xs)\<Rightarrow> root''"
   530   then show "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
   531     by cases auto
   532 next
   533   assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
   534   then show "root =(x # xs)\<Rightarrow> root''"
   535     by (blast intro: transitions.cons)
   536 qed
   537 
   538 text {*
   539   The next two rules show how to ``destruct'' known transition
   540   sequences.  Note that the second one actually relies on the
   541   uniqueness property of the basic transition system (see
   542   \secref{sec:unix-single-trans}).
   543 *}
   544 
   545 lemma transitions_nilD: "root =[]\<Rightarrow> root' \<Longrightarrow> root' = root"
   546   by (simp add: transitions_nil_eq)
   547 
   548 lemma transitions_consD:
   549   assumes list: "root =(x # xs)\<Rightarrow> root''"
   550     and hd: "root \<midarrow>x\<rightarrow> root'"
   551   shows "root' =xs\<Rightarrow> root''"
   552 proof -
   553   from list obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''"
   554     by cases simp_all
   555   from r' hd have "r' = root'" by (rule transition_uniq)
   556   with root'' show "root' =xs\<Rightarrow> root''" by simp
   557 qed
   558 
   559 text {*
   560   \medskip The following fact shows how an invariant @{term Q} of
   561   single transitions with property @{term P} may be transferred to
   562   iterated transitions.  The proof is rather obvious by rule induction
   563   over the definition of @{term "root =xs\<Rightarrow> root'"}.
   564 *}
   565 
   566 lemma transitions_invariant:
   567   assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r'"
   568     and trans: "root =xs\<Rightarrow> root'"
   569   shows "Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
   570   using trans
   571 proof induct
   572   case nil
   573   show ?case by (rule nil.prems)
   574 next
   575   case (cons root x root' xs root'')
   576   note P = `\<forall>x \<in> set (x # xs). P x`
   577   then have "P x" by simp
   578   with `root \<midarrow>x\<rightarrow> root'` and `Q root` have Q': "Q root'" by (rule r)
   579   from P have "\<forall>x \<in> set xs. P x" by simp
   580   with Q' show "Q root''" by (rule cons.hyps)
   581 qed
   582 
   583 text {*
   584   As an example of applying the previous result, we transfer the basic
   585   type-safety property (see \secref{sec:unix-single-trans}) from
   586   single transitions to iterated ones, which is a rather obvious
   587   result indeed.
   588 *}
   589 
   590 theorem transitions_type_safe:
   591   assumes "root =xs\<Rightarrow> root'"
   592     and "\<exists>att dir. root = Env att dir"
   593   shows "\<exists>att dir. root' = Env att dir"
   594   using transition_type_safe and assms
   595 proof (rule transitions_invariant)
   596   show "\<forall>x \<in> set xs. True" by blast
   597 qed
   598 
   599 
   600 section {* Executable sequences *}
   601 
   602 text {*
   603   An inductively defined relation such as the one of @{text "root \<midarrow>x\<rightarrow>
   604   root'"} (see \secref{sec:unix-syscall}) has two main aspects.  First
   605   of all, the resulting system admits a certain set of transition
   606   rules (introductions) as given in the specification.  Furthermore,
   607   there is an explicit least-fixed-point construction involved, which
   608   results in induction (and case-analysis) rules to eliminate known
   609   transitions in an exhaustive manner.
   610 
   611   \medskip Subsequently, we explore our transition system in an
   612   experimental style, mainly using the introduction rules with basic
   613   algebraic properties of the underlying structures.  The technique
   614   closely resembles that of Prolog combined with functional evaluation
   615   in a very simple manner.
   616 
   617   Just as the ``closed-world assumption'' is left implicit in Prolog,
   618   we do not refer to induction over the whole transition system here.
   619   So this is still purely positive reasoning about possible
   620   executions; exhaustive reasoning will be employed only later on (see
   621   \secref{sec:unix-bogosity}), when we shall demonstrate that certain
   622   behavior is \emph{not} possible.
   623 *}
   624 
   625 
   626 subsection {* Possible transitions *}
   627 
   628 text {*
   629   Rather obviously, a list of system operations can be executed within
   630   a certain state if there is a result state reached by an iterated
   631   transition.
   632 *}
   633 
   634 definition
   635   "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"
   636 
   637 lemma can_exec_nil: "can_exec root []"
   638   unfolding can_exec_def by (blast intro: transitions.intros)
   639 
   640 lemma can_exec_cons:
   641     "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> can_exec root' xs \<Longrightarrow> can_exec root (x # xs)"
   642   unfolding can_exec_def by (blast intro: transitions.intros)
   643 
   644 text {*
   645   \medskip In case that we already know that a certain sequence can be
   646   executed we may destruct it backwardly into individual transitions.
   647 *}
   648 
   649 lemma can_exec_snocD: "can_exec root (xs @ [y])
   650     \<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''"
   651 proof (induct xs arbitrary: root)
   652   case Nil
   653   then show ?case
   654     by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
   655 next
   656   case (Cons x xs)
   657   from `can_exec root ((x # xs) @ [y])` obtain r root'' where
   658       x: "root \<midarrow>x\<rightarrow> r" and
   659       xs_y: "r =(xs @ [y])\<Rightarrow> root''"
   660     by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
   661   from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
   662     unfolding can_exec_def by blast
   663   from x xs have "root =(x # xs)\<Rightarrow> root'"
   664     by (rule transitions.cons)
   665   with y show ?case by blast
   666 qed
   667 
   668 
   669 subsection {* Example executions \label{sec:unix-examples} *}
   670 
   671 text {*
   672   We are now ready to perform a few experiments within our formal
   673   model of Unix system-calls.  The common technique is to alternate
   674   introduction rules of the transition system (see
   675   \secref{sec:unix-trans}), and steps to solve any emerging side
   676   conditions using algebraic properties of the underlying file-system
   677   structures (see \secref{sec:unix-file-system}).
   678 *}
   679 
   680 lemmas eval = access_def init_def
   681 
   682 theorem "u \<in> users \<Longrightarrow> can_exec (init users)
   683     [Mkdir u perms [u, name]]"
   684   apply (rule can_exec_cons)
   685     -- {* back-chain @{term can_exec} (of @{term [source] Cons}) *}
   686   apply (rule mkdir)
   687     -- {* back-chain @{term Mkdir} *}
   688   apply (force simp add: eval)+
   689     -- {* solve preconditions of @{term Mkdir} *}
   690   apply (simp add: eval)
   691     -- {* peek at resulting dir (optional) *}
   692   txt {* @{subgoals [display]} *}
   693   apply (rule can_exec_nil)
   694     -- {* back-chain @{term can_exec} (of @{term [source] Nil}) *}
   695   done
   696 
   697 text {*
   698   By inspecting the result shown just before the final step above, we
   699   may gain confidence that our specification of Unix system-calls
   700   actually makes sense.  Further common errors are usually exhibited
   701   when preconditions of transition rules fail unexpectedly.
   702 
   703   \medskip Here are a few further experiments, using the same
   704   techniques as before.
   705 *}
   706 
   707 theorem "u \<in> users \<Longrightarrow> can_exec (init users)
   708    [Creat u perms [u, name],
   709     Unlink u [u, name]]"
   710   apply (rule can_exec_cons)
   711   apply (rule creat)
   712   apply (force simp add: eval)+
   713   apply (simp add: eval)
   714   apply (rule can_exec_cons)
   715   apply (rule unlink)
   716   apply (force simp add: eval)+
   717   apply (simp add: eval)
   718   txt {* peek at result: @{subgoals [display]} *}
   719   apply (rule can_exec_nil)
   720   done
   721 
   722 theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow>
   723   Readable \<in> perms\<^isub>2 \<Longrightarrow> name\<^isub>3 \<noteq> name\<^isub>4 \<Longrightarrow>
   724   can_exec (init users)
   725    [Mkdir u perms\<^isub>1 [u, name\<^isub>1],
   726     Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2],
   727     Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>3],
   728     Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>4],
   729     Readdir u {name\<^isub>3, name\<^isub>4} [u, name\<^isub>1, name\<^isub>2]]"
   730   apply (rule can_exec_cons, rule transition.intros,
   731     (force simp add: eval)+, (simp add: eval)?)+
   732   txt {* peek at result: @{subgoals [display]} *}
   733   apply (rule can_exec_nil)
   734   done
   735 
   736 theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow> Readable \<in> perms\<^isub>3 \<Longrightarrow>
   737   can_exec (init users)
   738    [Mkdir u perms\<^isub>1 [u, name\<^isub>1],
   739     Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2],
   740     Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>3],
   741     Write u' ''foo'' [u, name\<^isub>1, name\<^isub>2, name\<^isub>3],
   742     Read u ''foo'' [u, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
   743   apply (rule can_exec_cons, rule transition.intros,
   744     (force simp add: eval)+, (simp add: eval)?)+
   745   txt {* peek at result: @{subgoals [display]} *}
   746   apply (rule can_exec_nil)
   747   done
   748 
   749 
   750 section {* Odd effects --- treated formally \label{sec:unix-bogosity} *}
   751 
   752 text {*
   753   We are now ready to give a completely formal treatment of the
   754   slightly odd situation discussed in the introduction (see
   755   \secref{sec:unix-intro}): the file-system can easily reach a state
   756   where a user is unable to remove his very own directory, because it
   757   is still populated by items placed there by another user in an
   758   uncouth manner.
   759 *}
   760 
   761 subsection {* The general procedure \label{sec:unix-inv-procedure} *}
   762 
   763 text {*
   764   The following theorem expresses the general procedure we are
   765   following to achieve the main result.
   766 *}
   767 
   768 theorem general_procedure:
   769   assumes cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False"
   770     and init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root"
   771     and preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
   772     and init_result: "init users =bs\<Rightarrow> root"
   773   shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))"
   774 proof -
   775   {
   776     fix xs
   777     assume Ps: "\<forall>x \<in> set xs. P x"
   778     assume can_exec: "can_exec root (xs @ [y])"
   779     then obtain root' root'' where
   780         xs: "root =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''"
   781       by (blast dest: can_exec_snocD)
   782     from init_result have "Q root" by (rule init_inv)
   783     from preserve_inv xs this Ps have "Q root'"
   784       by (rule transitions_invariant)
   785     from this y have False by (rule cannot_y)
   786   }
   787   then show ?thesis by blast
   788 qed
   789 
   790 text {*
   791   Here @{prop "P x"} refers to the restriction on file-system
   792   operations that are admitted after having reached the critical
   793   configuration; according to the problem specification this will
   794   become @{prop "uid_of x = user\<^isub>1"} later on.  Furthermore,
   795   @{term y} refers to the operations we claim to be impossible to
   796   perform afterwards, we will take @{term Rmdir} later.  Moreover
   797   @{term Q} is a suitable (auxiliary) invariant over the file-system;
   798   choosing @{term Q} adequately is very important to make the proof
   799   work (see \secref{sec:unix-inv-lemmas}).
   800 *}
   801 
   802 
   803 subsection {* The particular situation *}
   804 
   805 text {*
   806   We introduce a few global declarations and axioms to describe our
   807   particular situation considered here.  Thus we avoid excessive use
   808   of local parameters in the subsequent development.
   809 *}
   810 
   811 locale situation =
   812   fixes users :: "uid set"
   813     and user\<^isub>1 :: uid
   814     and user\<^isub>2 :: uid
   815     and name\<^isub>1 :: name
   816     and name\<^isub>2 :: name
   817     and name\<^isub>3 :: name
   818     and perms\<^isub>1 :: perms
   819     and perms\<^isub>2 :: perms
   820   assumes user\<^isub>1_known: "user\<^isub>1 \<in> users"
   821     and user\<^isub>1_not_root: "user\<^isub>1 \<noteq> 0"
   822     and users_neq: "user\<^isub>1 \<noteq> user\<^isub>2"
   823     and perms\<^isub>1_writable: "Writable \<in> perms\<^isub>1"
   824     and perms\<^isub>2_not_writable: "Writable \<notin> perms\<^isub>2"
   825   notes facts = user\<^isub>1_known user\<^isub>1_not_root users_neq
   826     perms\<^isub>1_writable perms\<^isub>2_not_writable
   827 begin
   828 
   829 definition
   830   "bogus =
   831      [Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1],
   832       Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2],
   833       Creat user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
   834 definition
   835   "bogus_path = [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
   836 
   837 text {*
   838   The @{term bogus} operations are the ones that lead into the uncouth
   839   situation; @{term bogus_path} is the key position within the
   840   file-system where things go awry.
   841 *}
   842 
   843 
   844 subsection {* Invariance lemmas \label{sec:unix-inv-lemmas} *}
   845 
   846 text {*
   847   The following invariant over the root file-system describes the
   848   bogus situation in an abstract manner: located at a certain @{term
   849   path} within the file-system is a non-empty directory that is
   850   neither owned nor writable by @{term user\<^isub>1}.
   851 *}
   852 
   853 definition
   854   "invariant root path =
   855     (\<exists>att dir.
   856       access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
   857       user\<^isub>1 \<noteq> owner att \<and>
   858       access root path user\<^isub>1 {Writable} = None)"
   859 
   860 text {*
   861   Following the general procedure (see
   862   \secref{sec:unix-inv-procedure}) we will now establish the three key
   863   lemmas required to yield the final result.
   864 
   865   \begin{enumerate}
   866 
   867   \item The invariant is sufficiently strong to entail the
   868   pathological case that @{term user\<^isub>1} is unable to remove the
   869   (owned) directory at @{term "[user\<^isub>1, name\<^isub>1]"}.
   870 
   871   \item The invariant does hold after having executed the @{term
   872   bogus} list of operations (starting with an initial file-system
   873   configuration).
   874 
   875   \item The invariant is preserved by any file-system operation
   876   performed by @{term user\<^isub>1} alone, without any help by other
   877   users.
   878 
   879   \end{enumerate}
   880 
   881   As the invariant appears both as assumptions and conclusions in the
   882   course of proof, its formulation is rather critical for the whole
   883   development to work out properly.  In particular, the third step is
   884   very sensitive to the invariant being either too strong or too weak.
   885   Moreover the invariant has to be sufficiently abstract, lest the
   886   proof become cluttered by confusing detail.
   887 
   888   \medskip The first two lemmas are technically straight forward ---
   889   we just have to inspect rather special cases.
   890 *}
   891 
   892 lemma cannot_rmdir:
   893   assumes inv: "invariant root bogus_path"
   894     and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
   895   shows False
   896 proof -
   897   from inv obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
   898     unfolding invariant_def by blast
   899   moreover
   900   from rmdir obtain att where
   901       "access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)"
   902     by cases auto
   903   then have "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"
   904     by (simp only: access_empty_lookup lookup_append_some) simp
   905   ultimately show False by (simp add: bogus_path_def)
   906 qed
   907 
   908 lemma
   909   assumes init: "init users =bogus\<Rightarrow> root"
   910   notes eval = facts access_def init_def
   911   shows init_invariant: "invariant root bogus_path"
   912   using init
   913   apply (unfold bogus_def bogus_path_def)
   914   apply (drule transitions_consD, rule transition.intros,
   915       (force simp add: eval)+, (simp add: eval)?)+
   916     -- "evaluate all operations"
   917   apply (drule transitions_nilD)
   918     -- "reach final result"
   919   apply (simp add: invariant_def eval)
   920     -- "check the invariant"
   921   done
   922 
   923 text {*
   924   \medskip At last we are left with the main effort to show that the
   925   ``bogosity'' invariant is preserved by any file-system operation
   926   performed by @{term user\<^isub>1} alone.  Note that this holds for
   927   any @{term path} given, the particular @{term bogus_path} is not
   928   required here.
   929 *}
   930 
   931 lemma preserve_invariant:
   932   assumes tr: "root \<midarrow>x\<rightarrow> root'"
   933     and inv: "invariant root path"
   934     and uid: "uid_of x = user\<^isub>1"
   935   shows "invariant root' path"
   936 proof -
   937   from inv obtain att dir where
   938       inv1: "access root path user\<^isub>1 {} = Some (Env att dir)" and
   939       inv2: "dir \<noteq> empty" and
   940       inv3: "user\<^isub>1 \<noteq> owner att" and
   941       inv4: "access root path user\<^isub>1 {Writable} = None"
   942     by (auto simp add: invariant_def)
   943 
   944   from inv1 have lookup: "lookup root path = Some (Env att dir)"
   945     by (simp only: access_empty_lookup)
   946 
   947   from inv1 inv3 inv4 and user\<^isub>1_not_root
   948   have not_writable: "Writable \<notin> others att"
   949     by (auto simp add: access_def split: option.splits)
   950 
   951   show ?thesis
   952   proof cases
   953     assume "root' = root"
   954     with inv show "invariant root' path" by (simp only:)
   955   next
   956     assume changed: "root' \<noteq> root"
   957     with tr obtain opt where root': "root' = update (path_of x) opt root"
   958       by cases auto
   959     show ?thesis
   960     proof (rule prefix_cases)
   961       assume "path_of x \<parallel> path"
   962       with inv root'
   963       have "\<And>perms. access root' path user\<^isub>1 perms = access root path user\<^isub>1 perms"
   964         by (simp only: access_update_other)
   965       with inv show "invariant root' path"
   966         by (simp only: invariant_def)
   967     next
   968       assume "path_of x \<le> path"
   969       then obtain ys where path: "path = path_of x @ ys" ..
   970 
   971       show ?thesis
   972       proof (cases ys)
   973         assume "ys = []"
   974         with tr uid inv2 inv3 lookup changed path and user\<^isub>1_not_root
   975         have False
   976           by cases (auto simp add: access_empty_lookup dest: access_some_lookup)
   977         then show ?thesis ..
   978       next
   979         fix z zs assume ys: "ys = z # zs"
   980         have "lookup root' path = lookup root path"
   981         proof -
   982           from inv2 lookup path ys
   983           have look: "lookup root (path_of x @ z # zs) = Some (Env att dir)"
   984             by (simp only:)
   985           then obtain att' dir' file' where
   986               look': "lookup root (path_of x) = Some (Env att' dir')" and
   987               dir': "dir' z = Some file'" and
   988               file': "lookup file' zs = Some (Env att dir)"
   989             by (blast dest: lookup_some_upper)
   990 
   991           from tr uid changed look' dir' obtain att'' where
   992               look'': "lookup root' (path_of x) = Some (Env att'' dir')"
   993             by cases (auto simp add: access_empty_lookup lookup_update_some
   994               dest: access_some_lookup)
   995           with dir' file' have "lookup root' (path_of x @ z # zs) =
   996               Some (Env att dir)"
   997             by (simp add: lookup_append_some)
   998           with look path ys show ?thesis
   999             by simp
  1000         qed
  1001         with inv show "invariant root' path"
  1002           by (simp only: invariant_def access_def)
  1003       qed
  1004     next
  1005       assume "path < path_of x"
  1006       then obtain y ys where path: "path_of x = path @ y # ys" ..
  1007 
  1008       obtain dir' where
  1009         lookup': "lookup root' path = Some (Env att dir')" and
  1010         inv2': "dir' \<noteq> empty"
  1011       proof (cases ys)
  1012         assume "ys = []"
  1013         with path have parent: "path_of x = path @ [y]" by simp
  1014         with tr uid inv4 changed obtain "file" where
  1015             "root' = update (path_of x) (Some file) root"
  1016           by cases auto
  1017         with lookup parent have "lookup root' path = Some (Env att (dir(y\<mapsto>file)))"
  1018           by (simp only: update_append_some update_cons_nil_env)
  1019         moreover have "dir(y\<mapsto>file) \<noteq> empty" by simp
  1020         ultimately show ?thesis ..
  1021       next
  1022         fix z zs assume ys: "ys = z # zs"
  1023         with lookup root' path
  1024         have "lookup root' path = Some (update (y # ys) opt (Env att dir))"
  1025           by (simp only: update_append_some)
  1026         also obtain file' where
  1027           "update (y # ys) opt (Env att dir) = Env att (dir(y\<mapsto>file'))"
  1028         proof -
  1029           have "dir y \<noteq> None"
  1030           proof -
  1031             have "dir y = lookup (Env att dir) [y]"
  1032               by (simp split: option.splits)
  1033             also from lookup have "\<dots> = lookup root (path @ [y])"
  1034               by (simp only: lookup_append_some)
  1035             also have "\<dots> \<noteq> None"
  1036             proof -
  1037               from ys obtain us u where rev_ys: "ys = us @ [u]"
  1038                 by (cases ys rule: rev_cases) fastsimp+
  1039               with tr path
  1040               have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
  1041                   lookup root ((path @ [y]) @ us) \<noteq> None"
  1042                 by cases (auto dest: access_some_lookup)
  1043               then show ?thesis 
  1044                 by (simp, blast dest!: lookup_some_append)
  1045             qed
  1046             finally show ?thesis .
  1047           qed
  1048           with ys show ?thesis using that by auto
  1049         qed
  1050         also have "dir(y\<mapsto>file') \<noteq> empty" by simp
  1051         ultimately show ?thesis ..
  1052       qed
  1053 
  1054       from lookup' have inv1': "access root' path user\<^isub>1 {} = Some (Env att dir')"
  1055         by (simp only: access_empty_lookup)
  1056 
  1057       from inv3 lookup' and not_writable user\<^isub>1_not_root
  1058       have "access root' path user\<^isub>1 {Writable} = None"
  1059         by (simp add: access_def)
  1060       with inv1' inv2' inv3 show ?thesis unfolding invariant_def by blast
  1061     qed
  1062   qed
  1063 qed
  1064 
  1065 
  1066 subsection {* Putting it all together \label{sec:unix-main-result} *}
  1067 
  1068 text {*
  1069   The main result is now imminent, just by composing the three
  1070   invariance lemmas (see \secref{sec:unix-inv-lemmas}) according the the
  1071   overall procedure (see \secref{sec:unix-inv-procedure}).
  1072 *}
  1073 
  1074 corollary
  1075   assumes bogus: "init users =bogus\<Rightarrow> root"
  1076   shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^isub>1) \<and>
  1077     can_exec root (xs @ [Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1]]))"
  1078 proof -
  1079   from cannot_rmdir init_invariant preserve_invariant
  1080     and bogus show ?thesis by (rule general_procedure)
  1081 qed
  1082 
  1083 end
  1084 
  1085 end