summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 23 Jan 2001 18:05:53 +0100 | |

changeset 10966 | 8f2c27041a8e |

parent 10965 | cd89ce2795ab |

child 10967 | 69937e62a28e |

added HOL-Unix example;

--- a/NEWS Tue Jan 23 15:48:35 2001 +0100 +++ b/NEWS Tue Jan 23 18:05:53 2001 +0100 @@ -102,6 +102,10 @@ HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While (as While_Combinator), HOL/Lex/Prefix (as List_Prefix); +* HOL/Unix: "Some aspects of Unix file-system security", a typical +modelling and verification task performed in Isabelle/HOL + +Isabelle/Isar + Isabelle document preparation (by Markus Wenzel). + * HOL basics: added overloaded operations "inverse" and "divide" (infix "/"), syntax for generic "abs" operation, generic summation operator;

--- a/src/HOL/IsaMakefile Tue Jan 23 15:48:35 2001 +0100 +++ b/src/HOL/IsaMakefile Tue Jan 23 18:05:53 2001 +0100 @@ -37,6 +37,7 @@ TLA-Inc \ TLA-Memory \ HOL-UNITY \ + HOL-Unix \ HOL-W0 \ HOL-ex # ^ this is the sort position @@ -347,6 +348,16 @@ @$(ISATOOL) usedir $(OUT)/HOL UNITY +## HOL-Unix + +HOL-Unix: HOL $(LOG)/HOL-Unix.gz + +$(LOG)/HOL-Unix.gz: $(OUT)/HOL Library/Nested_Environment.thy \ + Library/List_Prefix.thy Unix/ROOT.ML Unix/Unix.thy \ + Unix/document/root.bib Unix/document/root.tex + @$(ISATOOL) usedir $(OUT)/HOL Unix + + ## HOL-Modelcheck HOL-Modelcheck: HOL $(LOG)/HOL-Modelcheck.gz

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Unix/ROOT.ML Tue Jan 23 18:05:53 2001 +0100 @@ -0,0 +1,2 @@ + +use_thy "Unix";

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Unix/Unix.thy Tue Jan 23 18:05:53 2001 +0100 @@ -0,0 +1,1134 @@ +(* Title: HOL/Unix/Unix.thy + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) +*) + +header {* Unix file-systems \label{sec:unix-file-system} *} + +theory Unix = Nested_Environment + List_Prefix: + +text {* + We give a simple mathematical model of the basic structures + underlying the Unix file-system, together with a few fundamental + operations that could be imagined to be performed internally by the + Unix kernel. This forms the basis for the set of Unix system-calls + to be introduced later (see \secref{sec:unix-trans}), which are the + actual interface offered to processes running in user-space. + + \medskip Basically, any Unix file is either a \emph{plain file} or a + \emph{directory}, consisting of some \emph{content} plus + \emph{attributes}. The content of a plain file is plain text. The + content of a directory is a mapping from names to further + files.\footnote{In fact, this is the only way that names get + associated with files. In Unix files do \emph{not} have a name in + itself. Even more, any number of names may be associated with the + very same file due to \emph{hard links} (although this is excluded + from our model).} Attributes include information to control various + ways to access the file (read, write etc.). + + Our model will be quite liberal in omitting excessive detail that is + easily seen to be ``irrelevant'' for the aspects of Unix + file-systems to be discussed here. First of all, we ignore + character and block special files, pipes, sockets, hard links, + symbolic links, and mount points. +*} + + +subsection {* Names *} + +text {* + User ids and file name components shall be represented by natural + numbers (without loss of generality). We do not bother about + encoding of actual names (e.g.\ strings), nor a mapping between user + names and user ids as would be present in a reality. +*} + +types + uid = nat + name = nat + path = "name list" + + +subsection {* Attributes *} + +text {* + Unix file attributes mainly consist of \emph{owner} information and + a number of \emph{permission} bits which control access for + ``user'', ``group'', and ``others'' (see the Unix man pages @{text + "chmod(2)"} and @{text "stat(2)"} for more details). + + \medskip Our model of file permissions only considers the ``others'' + part. The ``user'' field may be omitted without loss of overall + generality, since the owner is usually able to change it anyway by + performing @{text chmod}.\footnote{The inclined Unix expert may try + to figure out some exotic arrangements of a real-world Unix + file-system such that the owner of a file is unable to apply the + @{text chmod} system call.} We omit ``group'' permissions as a + genuine simplification as we just do not intend to discuss a model + of multiple groups and group membership, but pretend that everyone + is member of a single global group.\footnote{A general HOL model of + user group structures and related issues is given in + \cite{Naraschewski:2001}.} +*} + +datatype perm = + Readable + | Writable + | Executable -- "(ignored)" + +types perms = "perm set" + +record att = + owner :: uid + others :: perms + +text {* + For plain files @{term Readable} and @{term Writable} specify read + and write access to the actual content, i.e.\ the string of text + stored here. For directories @{term Readable} determines if the set + of entry names may be accessed, and @{term Writable} controls the + ability to create or delete any entries (both plain files or + sub-directories). + + As another simplification, we ignore the @{term Executable} + permission altogether. In reality it would indicate executable + plain files (also known as ``binaries''), or control actual lookup + of directory entries (recall that mere directory browsing is + controlled via @{term Readable}). Note that the latter means that + in order to perform any file-system operation whatsoever, all + directories encountered on the path would have to grant @{term + Executable}. We ignore this detail and pretend that all directories + give @{term Executable} permission to anybody. +*} + + +subsection {* Files *} + +text {* + In order to model the general tree structure of a Unix file-system + we use the arbitrarily branching datatype @{typ "('a, 'b, 'c) env"} + from the standard library of Isabelle/HOL + \cite{Bauer-et-al:2001:HOL-Library}. This type provides + constructors @{term Val} and @{term Env} as follows: + + \medskip + {\def\isastyleminor{\isastyle} + \begin{tabular}{l} + @{term [source] "Val :: 'a \<Rightarrow> ('a, 'b, 'c) env"} \\ + @{term [source] "Env :: 'b \<Rightarrow> ('c \<Rightarrow> ('a, 'b, 'c) env option) \<Rightarrow> ('a, 'b, 'c) env"} \\ + \end{tabular}} + \medskip + + Here the parameter @{typ 'a} refers to plain values occurring at + leaf positions, parameter @{typ 'b} to information kept with inner + branch nodes, and parameter @{typ 'c} to the branching type of the + tree structure. For our purpose we use the type instance with @{typ + "att \<times> string"} (representing plain files), @{typ att} (for + attributes of directory nodes), and @{typ name} (for the index type + of directory nodes). +*} + +types + file = "(att \<times> string, att, name) env" + +text {* + \medskip The HOL library also provides @{term lookup} and @{term + update} operations for general tree structures with the subsequent + primitive recursive characterizations. + + \medskip + {\def\isastyleminor{\isastyle} + \begin{tabular}{l} + @{term [source] "lookup :: ('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"} \\ + @{term [source] + "update :: 'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"} \\ + \end{tabular}} + + @{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]} + @{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]} + + Several further properties of these operations are proven in + \cite{Bauer-et-al:2001:HOL-Library}. These will be routinely used + later on without further notice. + + \bigskip Apparently, the elements of type @{typ file} contain an + @{typ att} component in either case. We now define a few auxiliary + operations to manipulate this field uniformly, following the + conventions for record types in Isabelle/HOL + \cite{Nipkow-et-al:2000:HOL}. +*} + +constdefs + attributes :: "file \<Rightarrow> att" + "attributes file \<equiv> + (case file of + Val (att, text) \<Rightarrow> att + | Env att dir \<Rightarrow> att)" + + attributes_update :: "att \<Rightarrow> file \<Rightarrow> file" + "attributes_update att file \<equiv> + (case file of + Val (att', text) \<Rightarrow> Val (att, text) + | Env att' dir \<Rightarrow> Env att dir)" + +lemma [simp]: "attributes (Val (att, text)) = att" + by (simp add: attributes_def) + +lemma [simp]: "attributes (Env att dir) = att" + by (simp add: attributes_def) + +lemma [simp]: "attributes (file \<lparr>attributes := att\<rparr>) = att" + by (cases file) (simp_all add: attributes_def attributes_update_def + split_tupled_all) + +lemma [simp]: "(Val (att, text)) \<lparr>attributes := att'\<rparr> = Val (att', text)" + by (simp add: attributes_update_def) + +lemma [simp]: "(Env att dir) \<lparr>attributes := att'\<rparr> = Env att' dir" + by (simp add: attributes_update_def) + + +subsection {* Initial file-systems *} + +text {* + Given a set of \emph{known users} a file-system shall be initialized + by providing an empty home directory for each user, with read-only + access for everyone else. (Note that we may directly use the user + id as home directory name, since both types have been identified.) + Certainly, the very root directory is owned by the super user (who + has user id 0). +*} + +constdefs + init :: "uid set \<Rightarrow> file" + "init users \<equiv> + Env \<lparr>owner = 0, others = {Readable}\<rparr> + (\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> empty) + else None)" + + +subsection {* Accessing file-systems *} + +text {* + The main internal file-system operation is access of a file by a + user, requesting a certain set of permissions. The resulting @{typ + "file option"} indicates if a file had been present at the + corresponding @{typ path} and if access was granted according to the + permissions recorded within the file-system. + + Note that by the rules of Unix file-system security (e.g.\ + \cite{Tanenbaum:1992}) both the super-user and owner may always + access a file unconditionally (in our simplified model). +*} + +constdefs + access :: "file \<Rightarrow> path \<Rightarrow> uid \<Rightarrow> perms \<Rightarrow> file option" + "access root path uid perms \<equiv> + (case lookup root path of + None \<Rightarrow> None + | Some file \<Rightarrow> + if uid = 0 + \<or> uid = owner (attributes file) + \<or> perms \<subseteq> others (attributes file) + then Some file + else None)" + +text {* + \medskip Successful access to a certain file is the main + prerequisite for system-calls to be applicable (cf.\ + \secref{sec:unix-trans}). Any modification of the file-system is + then performed using the basic @{term update} operation. + + \medskip We see that @{term access} is just a wrapper for the basic + @{term lookup} function, with additional checking of + attributes. Subsequently we establish a few auxiliary facts that + stem from the primitive @{term lookup} used within @{term access}. +*} + +lemma access_empty_lookup: "access root path uid {} = lookup root path" + by (simp add: access_def split: option.splits) + +lemma access_some_lookup: + "access root path uid perms = Some file \<Longrightarrow> + lookup root path = Some file" + by (simp add: access_def split: option.splits if_splits) + +lemma access_update_other: "path' \<parallel> path \<Longrightarrow> + access (update path' opt root) path uid perms = access root path uid perms" +proof - + assume "path' \<parallel> path" + then obtain y z xs ys zs where + "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs" + by (blast dest: parallel_decomp) + hence "lookup (update path' opt root) path = lookup root path" + by (blast intro: lookup_update_other) + thus ?thesis by (simp only: access_def) +qed + + +section {* File-system transitions \label{sec:unix-trans} *} + +subsection {* Unix system calls \label{sec:unix-syscall} *} + +text {* + According to established operating system design (cf.\ + \cite{Tanenbaum:1992}) user space processes may only initiate system + operations by a fixed set of \emph{system-calls}. This enables the + kernel to enforce certain security policies in the first + place.\footnote{Incidently, this is the very same principle employed + by any ``LCF-style'' theorem proving system according to Milner's + principle of ``correctness by construction'', such as Isabelle/HOL + itself.} + + \medskip In our model of Unix we give a fixed datatype @{text + operation} for the syntax of system-calls, together with an + inductive definition of file-system state transitions of the form + @{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics. +*} + +datatype operation = + Read uid string path + | Write uid string path + | Chmod uid perms path + | Creat uid perms path + | Unlink uid path + | Mkdir uid perms path + | Rmdir uid path + | Readdir uid "name set" path + +text {* + The @{typ uid} field of an operation corresponds to the + \emph{effective user id} of the underlying process, although our + model never mentions processes explicitly. The other parameters are + provided as arguments by the caller; the @{term path} one is common + to all kinds of system-calls. +*} + +consts + uid_of :: "operation \<Rightarrow> uid" +primrec + "uid_of (Read uid text path) = uid" + "uid_of (Write uid text path) = uid" + "uid_of (Chmod uid perms path) = uid" + "uid_of (Creat uid perms path) = uid" + "uid_of (Unlink uid path) = uid" + "uid_of (Mkdir uid path perms) = uid" + "uid_of (Rmdir uid path) = uid" + "uid_of (Readdir uid names path) = uid" + +consts + path_of :: "operation \<Rightarrow> path" +primrec + "path_of (Read uid text path) = path" + "path_of (Write uid text path) = path" + "path_of (Chmod uid perms path) = path" + "path_of (Creat uid perms path) = path" + "path_of (Unlink uid path) = path" + "path_of (Mkdir uid perms path) = path" + "path_of (Rmdir uid path) = path" + "path_of (Readdir uid names path) = path" + +text {* + \medskip Note that we have omitted explicit @{text Open} and @{text + Close} operations, pretending that @{term Read} and @{term Write} + would already take care of this behind the scenes. Thus we have + basically treated actual sequences of real system-calls @{text + open}--@{text read}/@{text write}--@{text close} as atomic. + + In principle, this could make big a difference in a model with + explicit concurrent processes. On the other hand, even on a real + Unix system the exact scheduling of concurrent @{text open} and + @{text close} operations does \emph{not} directly affect the success + of corresponding @{text read} or @{text write}. Unix allows several + processes to have files opened at the same time, even for writing! + Certainly, the result from reading the contents later may be hard to + predict, but the system-calls involved here will succeed in any + case. + + \bigskip The operational semantics of system calls is now specified + via transitions of the file-system configuration. This is expressed + as an inductive relation (although there is no actual recursion + involved here). +*} + +consts + transition :: "(file \<times> operation \<times> file) set" + +syntax + "_transition" :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool" + ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100) +translations + "root \<midarrow>x\<rightarrow> root'" \<rightleftharpoons> "(root, x, root') \<in> transition" + +inductive transition + intros + + read: + "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow> + root \<midarrow>(Read uid text path)\<rightarrow> root" + write: + "access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow> + root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root" + + chmod: + "access root path uid {} = Some file \<Longrightarrow> + uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow> + root \<midarrow>(Chmod uid perms path)\<rightarrow> update path + (Some (file \<lparr>attributes := attributes file \<lparr>others := perms\<rparr>\<rparr>)) root" + + creat: + "path = parent_path @ [name] \<Longrightarrow> + access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow> + access root path uid {} = None \<Longrightarrow> + root \<midarrow>(Creat uid perms path)\<rightarrow> update path + (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root" + unlink: + "path = parent_path @ [name] \<Longrightarrow> + access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow> + access root path uid {} = Some (Val plain) \<Longrightarrow> + root \<midarrow>(Unlink uid path)\<rightarrow> update path None root" + + mkdir: + "path = parent_path @ [name] \<Longrightarrow> + access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow> + access root path uid {} = None \<Longrightarrow> + root \<midarrow>(Mkdir uid perms path)\<rightarrow> update path + (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root" + rmdir: + "path = parent_path @ [name] \<Longrightarrow> + access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow> + access root path uid {} = Some (Env att' empty) \<Longrightarrow> + root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root" + + readdir: + "access root path uid {Readable} = Some (Env att dir) \<Longrightarrow> + names = dom dir \<Longrightarrow> + root \<midarrow>(Readdir uid names path)\<rightarrow> root" + +text {* + \medskip Certainly, the above specification is central to the whole + formal development. Any of the results to be established later on + are only meaningful to the outside world if this transition system + provides an adequate model of real Unix systems. This kind of + ``reality-check'' of a formal model is the well-known problem of + \emph{validation}. + + If in doubt, one may consider to compare our definition with the + informal specifications given the corresponding Unix man pages, or + even peek at an actual implementation such as + \cite{Torvalds-et-al:Linux}. Another common way to gain confidence + into the formal model is to run simple simulations (see + \secref{sec:unix-examples}), and check the results with that of + experiments performed on a real Unix system. +*} + + +subsection {* Basic properties of single transitions \label{sec:unix-single-trans} *} + +text {* + The transition system @{text "root \<midarrow>x\<rightarrow> root'"} defined above + determines a unique result @{term root'} from given @{term root} and + @{term x} (this is holds rather trivially, since there is even only + one clause for each operation). This uniqueness statement will + simplify our subsequent development to some extent, since we only + have to reason about a partial function rather than a general + relation. +*} + +theorem transition_uniq: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root \<midarrow>x\<rightarrow> root'' \<Longrightarrow> root' = root''" +proof - + assume root: "root \<midarrow>x\<rightarrow> root'" + assume "root \<midarrow>x\<rightarrow> root''" + thus "root' = root''" + proof cases + case read + with root show ?thesis by cases auto + next + case write + with root show ?thesis by cases auto + next + case chmod + with root show ?thesis by cases auto + next + case creat + with root show ?thesis by cases auto + next + case unlink + with root show ?thesis by cases auto + next + case mkdir + with root show ?thesis by cases auto + next + case rmdir + with root show ?thesis by cases auto + next + case readdir + with root show ?thesis by cases auto + qed +qed + +text {* + \medskip Apparently, file-system transitions are \emph{type-safe} in + the sense that the result of transforming an actual directory yields + again a directory. +*} + +theorem transition_type_safe: + "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir + \<Longrightarrow> \<exists>att dir. root' = Env att dir" +proof - + assume tr: "root \<midarrow>x\<rightarrow> root'" + assume inv: "\<exists>att dir. root = Env att dir" + show ?thesis + proof (cases "path_of x") + case Nil + with tr inv show ?thesis + by cases (auto simp add: access_def split: if_splits) + next + case Cons + from tr obtain opt where + "root' = root \<or> root' = update (path_of x) opt root" + by cases auto + with inv Cons show ?thesis + by (auto simp add: update_eq split: list.splits) + qed +qed + +text {* + The previous result may be seen as the most basic invariant on the + file-system state that is enforced by any proper kernel + implementation. So user processes --- being bound to the + system-call interface --- may never mess up a file-system such that + the root becomes a plain file instead of a directory, which would be + a strange situation indeed. +*} + + +subsection {* Iterated transitions *} + +text {* + Iterated system transitions via finite sequences of system + operations are modeled inductively as follows. In a sense, this + relation describes the cumulative effect of the sequence of + system-calls issued by a number of running processes over a finite + amount of time. +*} + +consts + transitions :: "(file \<times> operation list \<times> file) set" + +syntax + "_transitions" :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" + ("_ =_\<Rightarrow> _" [90, 1000, 90] 100) +translations + "root =xs\<Rightarrow> root'" \<rightleftharpoons> "(root, xs, root') \<in> transitions" + +inductive transitions + intros + nil: "root =[]\<Rightarrow> root" + cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''" + +text {* + \medskip We establish a few basic facts relating iterated + transitions with single ones, according to the recursive structure + of lists. +*} + +lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')" +proof + assume "root =[]\<Rightarrow> root'" + thus "root = root'" by cases simp_all +next + assume "root = root'" + thus "root =[]\<Rightarrow> root'" by (simp only: transitions.nil) +qed + +lemma transitions_cons_eq: + "root =(x # xs)\<Rightarrow> root'' = (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root'')" +proof + assume "root =(x # xs)\<Rightarrow> root''" + thus "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''" + by cases auto +next + assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''" + thus "root =(x # xs)\<Rightarrow> root''" + by (blast intro: transitions.cons) +qed + +text {* + The next two rules show how to ``destruct'' known transition + sequences. Note that the second one actually relies on the + uniqueness property of the basic transition system (see + \secref{sec:unix-single-trans}). +*} + +lemma transitions_nilD: "root =[]\<Rightarrow> root' \<Longrightarrow> root' = root" + by (simp add: transitions_nil_eq) + +lemma transitions_consD: + "root =(x # xs)\<Rightarrow> root'' \<Longrightarrow> root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root''" +proof - + assume "root =(x # xs)\<Rightarrow> root''" + then obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''" + by cases simp_all + assume "root \<midarrow>x\<rightarrow> root'" + with r' have "r' = root'" by (rule transition_uniq) + with root'' show "root' =xs\<Rightarrow> root''" by simp +qed + +text {* + \medskip The following fact shows how an invariant @{term Q} of + single transitions with property @{term P} may be transferred to + iterated transitions. The proof is rather obvious by rule induction + over the definition of @{term "root =xs\<Rightarrow> root'"}. +*} + +lemma transitions_invariant: + "(\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r') \<Longrightarrow> + root =xs\<Rightarrow> root' \<Longrightarrow> Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'" +proof - + assume r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'" + assume "root =xs\<Rightarrow> root'" + thus "Q root \<Longrightarrow> (\<forall>x \<in> set xs. P x) \<Longrightarrow> Q root'" (is "PROP ?P root xs root'") + proof (induct ?P root xs root') + fix root assume "Q root" + thus "Q root" . + next + fix root root' root'' and x xs + assume root': "root \<midarrow>x\<rightarrow> root'" + assume hyp: "PROP ?P root' xs root''" + assume Q: "Q root" + assume P: "\<forall>x \<in> set (x # xs). P x" + hence "P x" by simp + with root' Q have Q': "Q root'" by (rule r) + from P have "\<forall>x \<in> set xs. P x" by simp + with Q' show "Q root''" by (rule hyp) + qed +qed + +text {* + As an example of applying the previous result, we transfer the basic + type-safety property (see \secref{sec:unix-single-trans}) from + single transitions to iterated ones, which is a rather obvious + result indeed. +*} + +theorem transitions_type_safe: + "root =xs\<Rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir + \<Longrightarrow> \<exists>att dir. root' = Env att dir" +proof - + case antecedent + with transition_type_safe show ?thesis + proof (rule transitions_invariant) + show "\<forall>x \<in> set xs. True" by blast + qed +qed + + +section {* Executable sequences *} + +text {* + An inductively defined relation such as the one of + @{text "root \<midarrow>x\<rightarrow> root'"} (see \secref{sec:unix-syscall}) has two + main aspects. First of all, the resulting system admits a certain + set of transition rules (introductions) as given in the + specification. Furthermore, there is an explicit least-fixed-point + construction involved, which results in induction (and + case-analysis) rules to eliminate known transitions in an exhaustive + manner. + + \medskip Subsequently, we explore our transition system in an + experimental style, mainly using the introduction rules with basic + algebraic properties of the underlying structures. The technique + closely resembles that of Prolog combined with functional evaluation + in a very simple manner. + + Just as the ``closed-world assumption'' is left implicit in Prolog, + we do not refer to induction over the whole transition system here. + So this is still purely positive reasoning about possible + executions; exhaustive reasoning will be employed only later on (see + \secref{sec:unix-bogosity}), when we shall demonstrate that certain + behavior is \emph{not} possible. +*} + + +subsection {* Possible transitions *} + +text {* + Rather obviously, a list of system operations can be executed within + a certain state if there is a result state reached by an iterated + transition. +*} + +constdefs + can_exec :: "file \<Rightarrow> operation list \<Rightarrow> bool" + "can_exec root xs \<equiv> \<exists>root'. root =xs\<Rightarrow> root'" + +lemma can_exec_nil: "can_exec root []" + by (unfold can_exec_def) (blast intro: transitions.intros) + +lemma can_exec_cons: + "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> can_exec root' xs \<Longrightarrow> can_exec root (x # xs)" + by (unfold can_exec_def) (blast intro: transitions.intros) + +text {* + \medskip In case that we already know that a certain sequence can be + executed we may destruct it backwardly into individual transitions. +*} + +lemma can_exec_snocD: "\<And>root. can_exec root (xs @ [y]) + \<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''" + (is "PROP ?P xs" is "\<And>root. ?A root xs \<Longrightarrow> ?C root xs") +proof (induct xs) + fix root + { + assume "?A root []" + thus "?C root []" + by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq) + next + fix x xs + assume hyp: "PROP ?P xs" + assume asm: "?A root (x # xs)" + show "?C root (x # xs)" + proof - + from asm obtain r root'' where x: "root \<midarrow>x\<rightarrow> r" and + xs_y: "r =(xs @ [y])\<Rightarrow> root''" + by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq) + from xs_y hyp obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'" + by (auto simp add: can_exec_def) + from x xs have "root =(x # xs)\<Rightarrow> root'" + by (rule transitions.cons) + with y show ?thesis by blast + qed + } +qed + + +subsection {* Example executions \label{sec:unix-examples} *} + +text {* + We are now ready to perform a few experiments within our formal + model of Unix system-calls. The common technique is to alternate + introduction rules of the transition system (see + \secref{sec:unix-trans}), and steps to solve any emerging side + conditions using algebraic properties of the underlying file-system + structures (see \secref{sec:unix-file-system}). +*} + +lemmas eval = access_def init_def + +theorem "u \<in> users \<Longrightarrow> can_exec (init users) + [Mkdir u perms [u, name]]" + apply (rule can_exec_cons) + -- {* back-chain @{term can_exec} (of @{term [source] Cons}) *} + apply (rule mkdir) + -- {* back-chain @{term Mkdir} *} + apply (force simp add: eval)+ + -- {* solve preconditions of @{term Mkdir} *} + apply (simp add: eval) + -- {* peek at resulting dir (optional) *} + txt {* @{subgoals [display]} *} + apply (rule can_exec_nil) + -- {* back-chain @{term can_exec} (of @{term [source] Nil}) *} + done + +text {* + By inspecting the result shown just before the final step above, we + may gain confidence that our specification of Unix system-calls + actually makes sense. Further common errors are usually exhibited + when preconditions of transition rules fail unexpectedly. + + \medskip Here are a few further experiments, using the same + techniques as before. +*} + +theorem "u \<in> users \<Longrightarrow> can_exec (init users) + [Creat u perms [u, name], + Unlink u [u, name]]" + apply (rule can_exec_cons) + apply (rule creat) + apply (force simp add: eval)+ + apply (simp add: eval) + apply (rule can_exec_cons) + apply (rule unlink) + apply (force simp add: eval)+ + apply (simp add: eval) + txt {* peek at result: @{subgoals [display]} *} + apply (rule can_exec_nil) + done + +theorem "u \<in> users \<Longrightarrow> Writable \<in> perms1 \<Longrightarrow> + Readable \<in> perms2 \<Longrightarrow> name3 \<noteq> name4 \<Longrightarrow> + can_exec (init users) + [Mkdir u perms1 [u, name1], + Mkdir u' perms2 [u, name1, name2], + Creat u' perms3 [u, name1, name2, name3], + Creat u' perms3 [u, name1, name2, name4], + Readdir u {name3, name4} [u, name1, name2]]" + apply (rule can_exec_cons, rule transition.intros, + (force simp add: eval)+, (simp add: eval)?)+ + txt {* peek at result: @{subgoals [display]} *} + apply (rule can_exec_nil) + done + +theorem "u \<in> users \<Longrightarrow> Writable \<in> perms1 \<Longrightarrow> Readable \<in> perms3 \<Longrightarrow> + can_exec (init users) + [Mkdir u perms1 [u, name1], + Mkdir u' perms2 [u, name1, name2], + Creat u' perms3 [u, name1, name2, name3], + Write u' ''foo'' [u, name1, name2, name3], + Read u ''foo'' [u, name1, name2, name3]]" + apply (rule can_exec_cons, rule transition.intros, + (force simp add: eval)+, (simp add: eval)?)+ + txt {* peek at result: @{subgoals [display]} *} + apply (rule can_exec_nil) + done + + +section {* Odd effects --- treated formally \label{sec:unix-bogosity} *} + +text {* + We are now ready to give a completely formal treatment of the + slightly odd situation discussed in the introduction (see + \secref{sec:unix-intro}): the file-system can easily reach a state + where a user is unable to remove his very own directory, because it + is still populated by items placed there by another user in an + uncouth manner. +*} + +subsection {* The general procedure \label{sec:unix-inv-procedure} *} + +text {* + The following theorem expresses the general procedure we are + following to achieve the main result. +*} + +theorem general_procedure: + "(\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False) \<Longrightarrow> + (\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root) \<Longrightarrow> + (\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r') \<Longrightarrow> + init users =bs\<Rightarrow> root \<Longrightarrow> + \<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))" +proof - + assume cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False" + assume init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root" + assume preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'" + assume init_result: "init users =bs\<Rightarrow> root" + { + fix xs + assume Ps: "\<forall>x \<in> set xs. P x" + assume can_exec: "can_exec root (xs @ [y])" + then obtain root' root'' where + xs: "root =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''" + by (blast dest: can_exec_snocD) + from init_result have "Q root" by (rule init_inv) + from preserve_inv xs this Ps have "Q root'" + by (rule transitions_invariant) + from this y have False by (rule cannot_y) + } + thus ?thesis by blast +qed + +text {* + Here @{prop "P x"} refers to the restriction on file-system + operations that are admitted after having reached the critical + configuration; according to the problem specification this will + become @{prop "uid_of x = user1"} later on. Furthermore, @{term y} + refers to the operations we claim to be impossible to perform + afterwards, we will take @{term Rmdir} later. Moreover @{term Q} is + a suitable (auxiliary) invariant over the file-system; choosing + @{term Q} adequately is very important to make the proof work (see + \secref{sec:unix-inv-lemmas}). +*} + + +subsection {* The particular setup *} + +text {* + We introduce a few global declarations and axioms to describe our + particular setup considered here. Thus we avoid excessive use of + local parameters in the subsequent development. +*} + +consts + users :: "uid set" + user1 :: uid + user2 :: uid + name1 :: name + name2 :: name + name3 :: name + perms1 :: perms + perms2 :: perms + +axioms + user1_known: "user1 \<in> users" + user1_not_root: "user1 \<noteq> 0" + users_neq: "user1 \<noteq> user2" + perms1_writable: "Writable \<in> perms1" + perms2_not_writable: "Writable \<notin> perms2" + +lemmas "setup" = + user1_known user1_not_root users_neq + perms1_writable perms2_not_writable + +text {* + \medskip The @{term bogus} operations are the ones that lead into + the uncouth situation; @{term bogus_path} is the key position within + the file-system where things go awry. +*} + +constdefs + bogus :: "operation list" + "bogus \<equiv> + [Mkdir user1 perms1 [user1, name1], + Mkdir user2 perms2 [user1, name1, name2], + Creat user2 perms2 [user1, name1, name2, name3]]" + + bogus_path :: path + "bogus_path \<equiv> [user1, name1, name2]" + + +subsection {* Invariance lemmas \label{sec:unix-inv-lemmas} *} + +text {* + The following invariant over the root file-system describes the + bogus situation in an abstract manner: located at a certain @{term + path} within the file-system is a non-empty directory that is + neither owned and nor writable by @{term user1}. +*} + +constdefs + invariant :: "file \<Rightarrow> path \<Rightarrow> bool" + "invariant root path \<equiv> + (\<exists>att dir. + access root path user1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> + user1 \<noteq> owner att \<and> + access root path user1 {Writable} = None)" + +text {* + Following the general procedure (see + \secref{sec:unix-inv-procedure}) we + will now establish the three key lemmas required to yield the final + result. + + \begin{enumerate} + + \item The invariant is sufficiently strong to entail the + pathological case that @{term user1} is unable to remove the (owned) + directory at @{term "[user1, name1]"}. + + \item The invariant does hold after having executed the @{term + bogus} list of operations (starting with an initial file-system + configuration). + + \item The invariant is preserved by any file-system operation + performed by @{term user1} alone, without any help by other users. + + \end{enumerate} + + As the invariant appears both as assumptions and conclusions in the + course of proof, its formulation is rather critical for the whole + development to work out properly. In particular, the third step is + very sensitive to the invariant being either too strong or too weak. + Moreover the invariant has to be sufficiently abstract, lest the + proof become cluttered by confusing detail. + + \medskip The first two lemmas are technically straight forward --- + we just have to inspect rather special cases. +*} + +lemma cannot_rmdir: "invariant root bogus_path \<Longrightarrow> + root \<midarrow>(Rmdir user1 [user1, name1])\<rightarrow> root' \<Longrightarrow> False" +proof - + assume "invariant root bogus_path" + then obtain file where "access root bogus_path user1 {} = Some file" + by (unfold invariant_def) blast + moreover + assume "root \<midarrow>(Rmdir user1 [user1, name1])\<rightarrow> root'" + then obtain att where + "access root [user1, name1] user1 {} = Some (Env att empty)" + by cases auto + hence "access root ([user1, name1] @ [name2]) user1 {} = empty name2" + by (simp only: access_empty_lookup lookup_append_some) simp + ultimately show False by (simp add: bogus_path_def) +qed + +lemma init_invariant: "init users =bogus\<Rightarrow> root \<Longrightarrow> invariant root bogus_path" +proof - + note eval = "setup" access_def init_def + case antecedent thus ?thesis + apply (unfold bogus_def bogus_path_def) + apply (drule transitions_consD, rule transition.intros, + (force simp add: eval)+, (simp add: eval)?)+ + -- "evaluate all operations" + apply (drule transitions_nilD) + -- "reach final result" + apply (simp add: invariant_def eval) + -- "check the invariant" + done +qed + +text {* + \medskip At last we are left with the main effort to show that the + ``bogosity'' invariant is preserved by any file-system operation + performed by @{term user1} alone. Note that this holds for any + @{term path} given, the particular @{term bogus_path} is not + required here. +*} (* FIXME The overall structure of the proof is as follows \dots *) + +lemma preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> + invariant root path \<Longrightarrow> uid_of x = user1 \<Longrightarrow> invariant root' path" +proof - + assume tr: "root \<midarrow>x\<rightarrow> root'" + assume inv: "invariant root path" + assume uid: "uid_of x = user1" + + from inv obtain att dir where + inv1: "access root path user1 {} = Some (Env att dir)" and + inv2: "dir \<noteq> empty" and + inv3: "user1 \<noteq> owner att" and + inv4: "access root path user1 {Writable} = None" + by (auto simp add: invariant_def) + + from inv1 have lookup: "lookup root path = Some (Env att dir)" + by (simp only: access_empty_lookup) + + from inv1 inv3 inv4 and user1_not_root + have not_writable: "Writable \<notin> others att" + by (auto simp add: access_def split: option.splits if_splits) + + show ?thesis + proof cases + assume "root' = root" + with inv show "invariant root' path" by (simp only:) + next + assume changed: "root' \<noteq> root" + with tr obtain opt where root': "root' = update (path_of x) opt root" + by cases auto + show ?thesis + proof (rule prefix_cases) + assume "path_of x \<parallel> path" + with inv root' + have "\<And>perms. access root' path user1 perms = access root path user1 perms" + by (simp only: access_update_other) + with inv show "invariant root' path" + by (simp only: invariant_def) + next + assume "path_of x \<le> path" + then obtain ys where path: "path = path_of x @ ys" .. + + show ?thesis + proof (cases ys) + assume "ys = []" + with tr uid inv2 inv3 lookup changed path and user1_not_root + have False + by cases (auto simp add: access_empty_lookup dest: access_some_lookup) + thus ?thesis .. + next + fix z zs assume ys: "ys = z # zs" + have "lookup root' path = lookup root path" + proof - + from inv2 lookup path ys + have look: "lookup root (path_of x @ z # zs) = Some (Env att dir)" + by (simp only:) + then obtain att' dir' file' where + look': "lookup root (path_of x) = Some (Env att' dir')" and + dir': "dir' z = Some file'" and + file': "lookup file' zs = Some (Env att dir)" + by (blast dest: lookup_some_upper) + + from tr uid changed look' dir' obtain att'' where + look'': "lookup root' (path_of x) = Some (Env att'' dir')" + by cases (auto simp add: access_empty_lookup lookup_update_some + dest: access_some_lookup) + with dir' file' have "lookup root' (path_of x @ z # zs) = + Some (Env att dir)" + by (simp add: lookup_append_some) + with look path ys show ?thesis + by simp + qed + with inv show "invariant root' path" + by (simp only: invariant_def access_def) + qed + next + assume "path < path_of x" + then obtain y ys where path: "path_of x = path @ y # ys" .. + + obtain dir' where + lookup': "lookup root' path = Some (Env att dir')" and + inv2': "dir' \<noteq> empty" + proof (cases ys) + assume "ys = []" + with path have parent: "path_of x = path @ [y]" by simp + with tr uid inv4 changed obtain file where + "root' = update (path_of x) (Some file) root" + by cases auto + with parent lookup have "lookup root' path = Some (Env att (dir(y\<mapsto>file)))" + by (simp only: update_append_some update_cons_nil_env) + moreover have "dir(y\<mapsto>file) \<noteq> empty" by simp + ultimately show ?thesis .. + next + fix z zs assume ys: "ys = z # zs" + with lookup root' path + have "lookup root' path = Some (update (y # ys) opt (Env att dir))" + by (simp only: update_append_some) + also obtain file' where + "update (y # ys) opt (Env att dir) = Env att (dir(y\<mapsto>file'))" + proof - + have "dir y \<noteq> None" + proof - + have "dir y = lookup (Env att dir) [y]" + by (simp split: option.splits) + also from lookup have "\<dots> = lookup root (path @ [y])" + by (simp only: lookup_append_some) + also have "\<dots> \<noteq> None" + proof - + from ys obtain us u where rev_ys: "ys = us @ [u]" + by (cases ys rule: rev_cases) auto + with tr path + have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or> + lookup root ((path @ [y]) @ us) \<noteq> None" + by cases (auto dest: access_some_lookup) + thus ?thesis by (blast dest!: lookup_some_append) + qed + finally show ?thesis . + qed + with ys show ?thesis + by (insert that, auto simp add: update_cons_cons_env) + qed + also have "dir(y\<mapsto>file') \<noteq> empty" by simp + ultimately show ?thesis .. + qed + + from lookup' have inv1': "access root' path user1 {} = Some (Env att dir')" + by (simp only: access_empty_lookup) + + from inv3 lookup' and not_writable user1_not_root + have "access root' path user1 {Writable} = None" + by (simp add: access_def) + with inv1' inv2' inv3 show ?thesis by (unfold invariant_def) blast + qed + qed +qed + + +subsection {* Putting it all together \label{sec:unix-main-result} *} + +text {* + The main result is now imminent, just by composing the three + invariance lemmas (see \secref{sec:unix-inv-lemmas}) according the the + overall procedure (see \secref{sec:unix-inv-procedure}). +*} + +theorem main: + "init users =bogus\<Rightarrow> root \<Longrightarrow> + \<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user1) \<and> + can_exec root (xs @ [Rmdir user1 [user1, name1]]))" +proof - + case antecedent + with cannot_rmdir init_invariant preserve_invariant + show ?thesis by (rule general_procedure) +qed + +end

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Unix/document/root.bib Tue Jan 23 18:05:53 2001 +0100 @@ -0,0 +1,67 @@ + +@Unpublished{Bauer-et-al:2001:HOL-Library, + author = {Gertrud Bauer and Tobias Nipkow and Lawrence C Paulson and Markus Wenzel}, + title = {The Supplemental {Isabelle/HOL} Library}, + note = {\url{http://isabelle.in.tum.de/library/HOL/Library/document.pdf}}, + year = 2001 +} + +@PhdThesis{Naraschewski:2001, + author = {Wolfgang Naraschewski}, + title = {Teams as Types --- A Formal Treatment of Authorization in Groupware}, + school = {TU M\"unchen}, + year = 2001, + note = "submitted"} + +@Manual{Nipkow-et-al:2000:HOL, + author = {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel}, + title = {{Isabelle}'s Logics: {HOL}}, + institution = {Institut f\"ur Informatik, Technische Universi\"at + M\"unchen and Computer Laboratory, University of Cambridge}, + year = 2000, + note = {\url{http://isabelle.in.tum.de/doc/logics-HOL.pdf}} +} + +@Book{Tanenbaum:1992, + author = {Andrew S. Tanenbaum}, + title = {Modern Operating Systems}, + publisher = {Prentice-Hall}, + year = 1992 +} + + +@Misc{Torvalds-et-al:Linux, + author = {Linus Torvalds and others}, + title = {The {L}inux Kernel Archives}, + note = {\url{http://www.kernel.org}} +} + + +@Misc{Unix-heritage, + key = {Unix}, + title = {The {Unix} Heritage Society}, + note = {\url{http://minnie.cs.adfa.edu.au/TUHS/}} +} + +@InProceedings{Wenzel:1999:TPHOL, + author = {Markus Wenzel}, + title = {{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents}, + crossref = {tphols99}} + + +@Manual{Wenzel:2000:isar-ref, + author = {Markus Wenzel}, + title = {The {Isabelle/Isar} Reference Manual}, + year = 2000, + institution = {TU Munich}, + note = {\url{http://isabelle.in.tum.de/doc/isar-ref.pdf}} +} + +@Proceedings{tphols99, + title = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, + booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '99}, + editor = {Bertot, Y. and Dowek, G. and Hirschowitz, A. and + Paulin, C. and Thery, L.}, + series = {LNCS}, + volume = 1690, + year = 1999}

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Unix/document/root.tex Tue Jan 23 18:05:53 2001 +0100 @@ -0,0 +1,223 @@ + +\documentclass[11pt,a4paper]{article} +\usepackage{isabelle,isabellesym,pdfsetup} + +%for best-style documents ... +\urlstyle{rm} +\isabellestyle{it} + +\renewcommand{\isabeginpar}{\par\smallskip} +\renewcommand{\isamarkupcmt}[1]{{\isastylecmt---~~#1}} + +\newcommand{\secref}[1]{\S\ref{#1}} + + +\begin{document} + +\title{Some aspects of Unix file-system security} +\author{Markus Wenzel \\ TU M\"unchen} +\maketitle + +\begin{abstract} + Unix is a simple but powerful system where everything is either a process or + a file. Access to system resources works mainly via the file-system, + including special files and devices. Most Unix security issues are + reflected directly within the file-system. We give a mathematical model of + the main aspects of the Unix file-system including its security model, but + ignoring processes. Within this formal model we discuss some aspects of + Unix security, including a few odd effects caused by the general + ``worse-is-better'' approach followed in Unix. + + Our formal specifications will be giving in simply-typed classical + set-theory as provided by Isabelle/HOL. Formal proofs are expressed in a + human-readable fashion using the structured proof language of Isabelle/Isar, + which is a system intended to support intelligible semi-automated reasoning + over a wide range of application domains. Thus the present development also + demonstrates that Isabelle/Isar is sufficiently flexible to cover typical + abstract verification tasks as well. So far this has been the classical + domain of interactive theorem proving systems based on unstructured tactic + languages. +\end{abstract} + +\tableofcontents +\newpage + +\parindent 0pt\parskip 0.5ex + + +\section{Introduction}\label{sec:unix-intro} + +\subsection{The Unix philosophy} + +Over the last 2 or 3 decades the Unix community has collected a certain amount +of folklore wisdom on building systems that actually work, see +\cite{Unix-heritage} for further historical background information. Here is a +recent account of the philosophical principles behind the Unix way of software +and systems engineering.\footnote{This has appeared on \emph{Slashdot} on + 25-March-2000, see \url{http://slashdot.com}, as well as + \url{http://www.cix.co.uk/~dunnp/unix-philosophy.html}.} + +{\small +\begin{verbatim} +The UNIX Philosophy (Score:2, Insightful) +by yebb on Saturday March 25, @11:06AM EST (#69) +(User Info) + +The philosophy is a result of more than twenty years of software +development and has grown from the UNIX community instead of being +enforced upon it. It is a defacto-style of software development. The +nine major tenets of the UNIX Philosophy are: + + 1. small is beautiful + 2. make each program do one thing well + 3. build a prototype as soon as possible + 4. choose portability over efficiency + 5. store numerical data in flat files + 6. use software leverage to your advantage + 7. use shell scripts to increase leverage and portability + 8. avoid captive user interfaces + 9. make every program a filter + +The Ten Lesser Tenets + + 1. allow the user to tailor the environment + 2. make operating system kernels small and lightweight + 3. use lower case and keep it short + 4. save trees + 5. silence is golden + 6. think parallel + 7. the sum of the parts if greater than the whole + 8. look for the ninety percent solution + 9. worse is better + 10. think hierarchically +\end{verbatim} +} + +The ``worse-is-better'' approach quoted above is particularly interesting. It +basically means that \emph{relevant} concepts have to be implemented in the +right way, while \emph{irrelevant} issues are simply ignored in order to avoid +unnecessary complication of the design and implementation. Certainly, the +overall quality of the resulting system heavily depends on the virtue of +distinction between the two categories of ``relevant'' and ``irrelevant''. + + +\subsection{Unix security} + +The main entities of a Unix system are \emph{files} and \emph{processes} +\cite{Tanenbaum:1992}. Files subsume any persistent ``static'' entity managed +by the system --- ranging from plain files and directories, to more special +ones such device nodes, pipes etc. On the other hand, processes are +``dynamic'' entities that may perform certain operations while being run by +the system. + +The security model of classic Unix systems is centered around the file system. +The operations permitted by a process that is run by a certain user are +determined from information stored within the file system. This includes any +kind of access control, such as read/write access to some plain file, or +read-only access to a certain global device node etc. Thus proper arrangement +of the main Unix file-system is very critical for overall +security.\footnote{Incidently, this is why the operation of mounting new + volumes into the existing file space is usually restricted to the + super-user.} + +\medskip Generally speaking, the Unix security model is a very simplistic one. +The original designers did not have maximum security in mind, but wanted to +get a decent system working for typical multi-user environments. Contemporary +Unix implementations still follow the basic security model of the original +versions from the early 1970's \cite{Unix-heritage}. Even back then there +would have been better approaches available, albeit with more complexity +involved both for implementers and users. + +On the other hand, even in the 2000's many computer systems are run with +little or no file-system security at all, even though virtually any system is +exposed to the net in one way or the other. Even ``personal'' computer +systems have long left the comfortable home environment and entered the +wilderness of the open net sphere. + +\medskip This treatment of file-system security is a typical example of the +``worse-is-better'' principle introduced above. The simplistic security model +of Unix got widely accepted within a large user community, while the more +innovative (and cumbersome) ones are only used very reluctantly and even tend +to be disabled by default in order to avoid confusion of beginners. + + +\subsection{Odd effects} + +Simplistic systems usually work very well in typical situations, but tend to +exhibit some odd features in non-typical ones. As far as Unix file-system +security is concerned, there are many such features that are well-known to +experts, but may surprise naive users. + +Subsequently, we consider an example that is not so exotic after all. As may +be easily experienced on a running Unix system, the following sequence of +commands may put a user's file-system into an uncouth state. Below we assume +that \texttt{user1} and \texttt{user2} are working within the same directory +(e.g.\ somewhere within the home of \texttt{user1}). + +{\small +\begin{verbatim} + user1> umask 000; mkdir foo; umask 022 + user2> mkdir foo/bar + user2> touch foo/bar/baz +\end{verbatim} +} + +That is, \texttt{user1} creates a directory that is writable for everyone, and +\texttt{user2} puts there a non-empty directory without write-access for +others. + +In this situation it has become impossible for \texttt{user1} to remove his +very own directory \texttt{foo} without the cooperation of either +\texttt{user2}, since \texttt{foo} contains another non-empty and non-writable +directory, which cannot be removed. + +{\small +\begin{verbatim} + user1> rmdir foo + rmdir: directory "foo": Directory not empty + user1> rmdir foo/bar + rmdir: directory "bar": Directory not empty + user1> rm foo/bar/baz + rm not removed: Permission denied +\end{verbatim} +} + +Only after \texttt{user2} has cleaned up his directory \texttt{bar}, is +\texttt{user1} enabled to remove both \texttt{foo/bar} and \texttt{foo}. +Alternatively \texttt{user2} could remove \texttt{foo/bar} as well. In the +unfortunate case that \texttt{user2} does not cooperate or is presently +unavailable, \texttt{user1} would have to find the super user (\texttt{root}) +to clean up the situation. In Unix \texttt{root} may perform any file-system +operation without any access control limitations.\footnote{This is the typical + Unix way of handling abnormal situations: while it is easy to run into odd + cases due to simplistic policies it as well quite easy to get out. There + are other well-known systems that make it somewhat harder to get into a fix, + but almost impossible to get out again!} + +\bigskip Is there really no other way out for \texttt{user1} in the above +situation? Experiments can only show possible ways, but never demonstrate the +absence of other means exhaustively. This is a typical situation where +(formal) proof may help. Subsequently, we model the main aspects Unix +file-system security within Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} and +prove that there is indeed no way for \texttt{user1} to get rid of his +directory \texttt{foo} without help by others (see +\secref{sec:unix-main-result} for the main theorem stating this). + +\medskip The formal techniques employed in this development are the typical +ones for abstract ``verification'' tasks, namely induction and case analysis +over the structure of file-systems and possible system transitions. +Isabelle/HOL \cite{Nipkow-et-al:2000:HOL} is particularly well-suited for this +kind of application. By the present development we also demonstrate that the +Isabelle/Isar environment \cite{Wenzel:1999:TPHOL,Wenzel:2000:isar-ref} for +readable formal proofs is sufficiently flexible to cover non-trivial +verification tasks as well. So far this has been the classical domain of +``interactive'' theorem proving systems based on unstructured tactic +languages. + + +\input{Unix} + +\bibliographystyle{abbrv} +\bibliography{root} + +\end{document}