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