1 (* Title: HOL/Unix/Unix.thy |
1 (* Title: HOL/Unix/Unix.thy |
2 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 header {* Unix file-systems \label{sec:unix-file-system} *} |
5 header \<open>Unix file-systems \label{sec:unix-file-system}\<close> |
6 |
6 |
7 theory Unix |
7 theory Unix |
8 imports |
8 imports |
9 Nested_Environment |
9 Nested_Environment |
10 "~~/src/HOL/Library/Sublist" |
10 "~~/src/HOL/Library/Sublist" |
11 begin |
11 begin |
12 |
12 |
13 text {* |
13 text \<open> |
14 We give a simple mathematical model of the basic structures |
14 We give a simple mathematical model of the basic structures |
15 underlying the Unix file-system, together with a few fundamental |
15 underlying the Unix file-system, together with a few fundamental |
16 operations that could be imagined to be performed internally by the |
16 operations that could be imagined to be performed internally by the |
17 Unix kernel. This forms the basis for the set of Unix system-calls |
17 Unix kernel. This forms the basis for the set of Unix system-calls |
18 to be introduced later (see \secref{sec:unix-trans}), which are the |
18 to be introduced later (see \secref{sec:unix-trans}), which are the |
32 Our model will be quite liberal in omitting excessive detail that is |
32 Our model will be quite liberal in omitting excessive detail that is |
33 easily seen to be ``irrelevant'' for the aspects of Unix |
33 easily seen to be ``irrelevant'' for the aspects of Unix |
34 file-systems to be discussed here. First of all, we ignore |
34 file-systems to be discussed here. First of all, we ignore |
35 character and block special files, pipes, sockets, hard links, |
35 character and block special files, pipes, sockets, hard links, |
36 symbolic links, and mount points. |
36 symbolic links, and mount points. |
37 *} |
37 \<close> |
38 |
38 |
39 |
39 |
40 subsection {* Names *} |
40 subsection \<open>Names\<close> |
41 |
41 |
42 text {* |
42 text \<open> |
43 User ids and file name components shall be represented by natural |
43 User ids and file name components shall be represented by natural |
44 numbers (without loss of generality). We do not bother about |
44 numbers (without loss of generality). We do not bother about |
45 encoding of actual names (e.g.\ strings), nor a mapping between user |
45 encoding of actual names (e.g.\ strings), nor a mapping between user |
46 names and user ids as would be present in a reality. |
46 names and user ids as would be present in a reality. |
47 *} |
47 \<close> |
48 |
48 |
49 type_synonym uid = nat |
49 type_synonym uid = nat |
50 type_synonym name = nat |
50 type_synonym name = nat |
51 type_synonym path = "name list" |
51 type_synonym path = "name list" |
52 |
52 |
53 |
53 |
54 subsection {* Attributes *} |
54 subsection \<open>Attributes\<close> |
55 |
55 |
56 text {* |
56 text \<open> |
57 Unix file attributes mainly consist of \emph{owner} information and |
57 Unix file attributes mainly consist of \emph{owner} information and |
58 a number of \emph{permission} bits which control access for |
58 a number of \emph{permission} bits which control access for |
59 ``user'', ``group'', and ``others'' (see the Unix man pages @{text |
59 ``user'', ``group'', and ``others'' (see the Unix man pages @{text |
60 "chmod(2)"} and @{text "stat(2)"} for more details). |
60 "chmod(2)"} and @{text "stat(2)"} for more details). |
61 |
61 |
68 @{text chmod} system call.} We omit ``group'' permissions as a |
68 @{text chmod} system call.} We omit ``group'' permissions as a |
69 genuine simplification as we just do not intend to discuss a model |
69 genuine simplification as we just do not intend to discuss a model |
70 of multiple groups and group membership, but pretend that everyone |
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 |
71 is member of a single global group.\footnote{A general HOL model of |
72 user group structures and related issues is given in |
72 user group structures and related issues is given in |
73 \cite{Naraschewski:2001}.} |
73 @{cite "Naraschewski:2001"}.} |
74 *} |
74 \<close> |
75 |
75 |
76 datatype perm = |
76 datatype perm = |
77 Readable |
77 Readable |
78 | Writable |
78 | Writable |
79 | Executable -- "(ignored)" |
79 | Executable -- "(ignored)" |
99 controlled via @{term Readable}). Note that the latter means that |
99 controlled via @{term Readable}). Note that the latter means that |
100 in order to perform any file-system operation whatsoever, all |
100 in order to perform any file-system operation whatsoever, all |
101 directories encountered on the path would have to grant @{term |
101 directories encountered on the path would have to grant @{term |
102 Executable}. We ignore this detail and pretend that all directories |
102 Executable}. We ignore this detail and pretend that all directories |
103 give @{term Executable} permission to anybody. |
103 give @{term Executable} permission to anybody. |
104 *} |
104 \<close> |
105 |
105 |
106 |
106 |
107 subsection {* Files *} |
107 subsection \<open>Files\<close> |
108 |
108 |
109 text {* |
109 text \<open> |
110 In order to model the general tree structure of a Unix file-system |
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"} |
111 we use the arbitrarily branching datatype @{typ "('a, 'b, 'c) env"} |
112 from the standard library of Isabelle/HOL |
112 from the standard library of Isabelle/HOL |
113 \cite{Bauer-et-al:2002:HOL-Library}. This type provides |
113 @{cite "Bauer-et-al:2002:HOL-Library"}. This type provides |
114 constructors @{term Val} and @{term Env} as follows: |
114 constructors @{term Val} and @{term Env} as follows: |
115 |
115 |
116 \medskip |
116 \medskip |
117 {\def\isastyleminor{\isastyle} |
117 {\def\isastyleminor{\isastyle} |
118 \begin{tabular}{l} |
118 \begin{tabular}{l} |
126 branch nodes, and parameter @{typ 'c} to the branching type of the |
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 |
127 tree structure. For our purpose we use the type instance with @{typ |
128 "att \<times> string"} (representing plain files), @{typ att} (for |
128 "att \<times> string"} (representing plain files), @{typ att} (for |
129 attributes of directory nodes), and @{typ name} (for the index type |
129 attributes of directory nodes), and @{typ name} (for the index type |
130 of directory nodes). |
130 of directory nodes). |
131 *} |
131 \<close> |
132 |
132 |
133 type_synonym "file" = "(att \<times> string, att, name) env" |
133 type_synonym "file" = "(att \<times> string, att, name) env" |
134 |
134 |
135 text {* |
135 text \<open> |
136 \medskip The HOL library also provides @{term lookup} and @{term |
136 \medskip The HOL library also provides @{term lookup} and @{term |
137 update} operations for general tree structures with the subsequent |
137 update} operations for general tree structures with the subsequent |
138 primitive recursive characterizations. |
138 primitive recursive characterizations. |
139 |
139 |
140 \medskip |
140 \medskip |
147 |
147 |
148 @{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]} |
148 @{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]} |
149 @{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]} |
149 @{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]} |
150 |
150 |
151 Several further properties of these operations are proven in |
151 Several further properties of these operations are proven in |
152 \cite{Bauer-et-al:2002:HOL-Library}. These will be routinely used |
152 @{cite "Bauer-et-al:2002:HOL-Library"}. These will be routinely used |
153 later on without further notice. |
153 later on without further notice. |
154 |
154 |
155 \bigskip Apparently, the elements of type @{typ "file"} contain an |
155 \bigskip Apparently, the elements of type @{typ "file"} contain an |
156 @{typ att} component in either case. We now define a few auxiliary |
156 @{typ att} component in either case. We now define a few auxiliary |
157 operations to manipulate this field uniformly, following the |
157 operations to manipulate this field uniformly, following the |
158 conventions for record types in Isabelle/HOL |
158 conventions for record types in Isabelle/HOL |
159 \cite{Nipkow-et-al:2000:HOL}. |
159 @{cite "Nipkow-et-al:2000:HOL"}. |
160 *} |
160 \<close> |
161 |
161 |
162 definition |
162 definition |
163 "attributes file = |
163 "attributes file = |
164 (case file of |
164 (case file of |
165 Val (att, text) \<Rightarrow> att |
165 Val (att, text) \<Rightarrow> att |
186 |
186 |
187 lemma [simp]: "map_attributes f (Env att dir) = Env (f att) dir" |
187 lemma [simp]: "map_attributes f (Env att dir) = Env (f att) dir" |
188 by (simp add: map_attributes_def) |
188 by (simp add: map_attributes_def) |
189 |
189 |
190 |
190 |
191 subsection {* Initial file-systems *} |
191 subsection \<open>Initial file-systems\<close> |
192 |
192 |
193 text {* |
193 text \<open> |
194 Given a set of \emph{known users} a file-system shall be initialized |
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 |
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 |
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.) |
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 |
198 Certainly, the very root directory is owned by the super user (who |
199 has user id 0). |
199 has user id 0). |
200 *} |
200 \<close> |
201 |
201 |
202 definition |
202 definition |
203 "init users = |
203 "init users = |
204 Env \<lparr>owner = 0, others = {Readable}\<rparr> |
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) |
205 (\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> empty) |
206 else None)" |
206 else None)" |
207 |
207 |
208 |
208 |
209 subsection {* Accessing file-systems *} |
209 subsection \<open>Accessing file-systems\<close> |
210 |
210 |
211 text {* |
211 text \<open> |
212 The main internal file-system operation is access of a file by a |
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 |
213 user, requesting a certain set of permissions. The resulting @{typ |
214 "file option"} indicates if a file had been present at the |
214 "file option"} indicates if a file had been present at the |
215 corresponding @{typ path} and if access was granted according to the |
215 corresponding @{typ path} and if access was granted according to the |
216 permissions recorded within the file-system. |
216 permissions recorded within the file-system. |
217 |
217 |
218 Note that by the rules of Unix file-system security (e.g.\ |
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 |
219 @{cite "Tanenbaum:1992"}) both the super-user and owner may always |
220 access a file unconditionally (in our simplified model). |
220 access a file unconditionally (in our simplified model). |
221 *} |
221 \<close> |
222 |
222 |
223 definition |
223 definition |
224 "access root path uid perms = |
224 "access root path uid perms = |
225 (case lookup root path of |
225 (case lookup root path of |
226 None \<Rightarrow> None |
226 None \<Rightarrow> None |
229 \<or> uid = owner (attributes file) |
229 \<or> uid = owner (attributes file) |
230 \<or> perms \<subseteq> others (attributes file) |
230 \<or> perms \<subseteq> others (attributes file) |
231 then Some file |
231 then Some file |
232 else None)" |
232 else None)" |
233 |
233 |
234 text {* |
234 text \<open> |
235 \medskip Successful access to a certain file is the main |
235 \medskip Successful access to a certain file is the main |
236 prerequisite for system-calls to be applicable (cf.\ |
236 prerequisite for system-calls to be applicable (cf.\ |
237 \secref{sec:unix-trans}). Any modification of the file-system is |
237 \secref{sec:unix-trans}). Any modification of the file-system is |
238 then performed using the basic @{term update} operation. |
238 then performed using the basic @{term update} operation. |
239 |
239 |
240 \medskip We see that @{term access} is just a wrapper for the basic |
240 \medskip We see that @{term access} is just a wrapper for the basic |
241 @{term lookup} function, with additional checking of |
241 @{term lookup} function, with additional checking of |
242 attributes. Subsequently we establish a few auxiliary facts that |
242 attributes. Subsequently we establish a few auxiliary facts that |
243 stem from the primitive @{term lookup} used within @{term access}. |
243 stem from the primitive @{term lookup} used within @{term access}. |
244 *} |
244 \<close> |
245 |
245 |
246 lemma access_empty_lookup: "access root path uid {} = lookup root path" |
246 lemma access_empty_lookup: "access root path uid {} = lookup root path" |
247 by (simp add: access_def split: option.splits) |
247 by (simp add: access_def split: option.splits) |
248 |
248 |
249 lemma access_some_lookup: |
249 lemma access_some_lookup: |
262 by (blast intro: lookup_update_other) |
262 by (blast intro: lookup_update_other) |
263 then show ?thesis by (simp only: access_def) |
263 then show ?thesis by (simp only: access_def) |
264 qed |
264 qed |
265 |
265 |
266 |
266 |
267 section {* File-system transitions \label{sec:unix-trans} *} |
267 section \<open>File-system transitions \label{sec:unix-trans}\<close> |
268 |
268 |
269 subsection {* Unix system calls \label{sec:unix-syscall} *} |
269 subsection \<open>Unix system calls \label{sec:unix-syscall}\<close> |
270 |
270 |
271 text {* |
271 text \<open> |
272 According to established operating system design (cf.\ |
272 According to established operating system design (cf.\ |
273 \cite{Tanenbaum:1992}) user space processes may only initiate system |
273 @{cite "Tanenbaum:1992"}) user space processes may only initiate system |
274 operations by a fixed set of \emph{system-calls}. This enables the |
274 operations by a fixed set of \emph{system-calls}. This enables the |
275 kernel to enforce certain security policies in the first |
275 kernel to enforce certain security policies in the first |
276 place.\footnote{Incidently, this is the very same principle employed |
276 place.\footnote{Incidently, this is the very same principle employed |
277 by any ``LCF-style'' theorem proving system according to Milner's |
277 by any ``LCF-style'' theorem proving system according to Milner's |
278 principle of ``correctness by construction'', such as Isabelle/HOL |
278 principle of ``correctness by construction'', such as Isabelle/HOL |
292 | Unlink uid path |
292 | Unlink uid path |
293 | Mkdir uid perms path |
293 | Mkdir uid perms path |
294 | Rmdir uid path |
294 | Rmdir uid path |
295 | Readdir uid "name set" path |
295 | Readdir uid "name set" path |
296 |
296 |
297 text {* |
297 text \<open> |
298 The @{typ uid} field of an operation corresponds to the |
298 The @{typ uid} field of an operation corresponds to the |
299 \emph{effective user id} of the underlying process, although our |
299 \emph{effective user id} of the underlying process, although our |
300 model never mentions processes explicitly. The other parameters are |
300 model never mentions processes explicitly. The other parameters are |
301 provided as arguments by the caller; the @{term path} one is common |
301 provided as arguments by the caller; the @{term path} one is common |
302 to all kinds of system-calls. |
302 to all kinds of system-calls. |
303 *} |
303 \<close> |
304 |
304 |
305 primrec uid_of :: "operation \<Rightarrow> uid" |
305 primrec uid_of :: "operation \<Rightarrow> uid" |
306 where |
306 where |
307 "uid_of (Read uid text path) = uid" |
307 "uid_of (Read uid text path) = uid" |
308 | "uid_of (Write uid text path) = uid" |
308 | "uid_of (Write uid text path) = uid" |
322 | "path_of (Unlink uid path) = path" |
322 | "path_of (Unlink uid path) = path" |
323 | "path_of (Mkdir uid perms path) = path" |
323 | "path_of (Mkdir uid perms path) = path" |
324 | "path_of (Rmdir uid path) = path" |
324 | "path_of (Rmdir uid path) = path" |
325 | "path_of (Readdir uid names path) = path" |
325 | "path_of (Readdir uid names path) = path" |
326 |
326 |
327 text {* |
327 text \<open> |
328 \medskip Note that we have omitted explicit @{text Open} and @{text |
328 \medskip Note that we have omitted explicit @{text Open} and @{text |
329 Close} operations, pretending that @{term Read} and @{term Write} |
329 Close} operations, pretending that @{term Read} and @{term Write} |
330 would already take care of this behind the scenes. Thus we have |
330 would already take care of this behind the scenes. Thus we have |
331 basically treated actual sequences of real system-calls @{text |
331 basically treated actual sequences of real system-calls @{text |
332 "open"}--@{text read}/@{text write}--@{text close} as atomic. |
332 "open"}--@{text read}/@{text write}--@{text close} as atomic. |
390 readdir: |
390 readdir: |
391 "access root path uid {Readable} = Some (Env att dir) \<Longrightarrow> |
391 "access root path uid {Readable} = Some (Env att dir) \<Longrightarrow> |
392 names = dom dir \<Longrightarrow> |
392 names = dom dir \<Longrightarrow> |
393 root \<midarrow>(Readdir uid names path)\<rightarrow> root" |
393 root \<midarrow>(Readdir uid names path)\<rightarrow> root" |
394 |
394 |
395 text {* |
395 text \<open> |
396 \medskip Certainly, the above specification is central to the whole |
396 \medskip Certainly, the above specification is central to the whole |
397 formal development. Any of the results to be established later on |
397 formal development. Any of the results to be established later on |
398 are only meaningful to the outside world if this transition system |
398 are only meaningful to the outside world if this transition system |
399 provides an adequate model of real Unix systems. This kind of |
399 provides an adequate model of real Unix systems. This kind of |
400 ``reality-check'' of a formal model is the well-known problem of |
400 ``reality-check'' of a formal model is the well-known problem of |
401 \emph{validation}. |
401 \emph{validation}. |
402 |
402 |
403 If in doubt, one may consider to compare our definition with the |
403 If in doubt, one may consider to compare our definition with the |
404 informal specifications given the corresponding Unix man pages, or |
404 informal specifications given the corresponding Unix man pages, or |
405 even peek at an actual implementation such as |
405 even peek at an actual implementation such as |
406 \cite{Torvalds-et-al:Linux}. Another common way to gain confidence |
406 @{cite "Torvalds-et-al:Linux"}. Another common way to gain confidence |
407 into the formal model is to run simple simulations (see |
407 into the formal model is to run simple simulations (see |
408 \secref{sec:unix-examples}), and check the results with that of |
408 \secref{sec:unix-examples}), and check the results with that of |
409 experiments performed on a real Unix system. |
409 experiments performed on a real Unix system. |
410 *} |
410 \<close> |
411 |
411 |
412 |
412 |
413 subsection {* Basic properties of single transitions \label{sec:unix-single-trans} *} |
413 subsection \<open>Basic properties of single transitions \label{sec:unix-single-trans}\<close> |
414 |
414 |
415 text {* |
415 text \<open> |
416 The transition system @{text "root \<midarrow>x\<rightarrow> root'"} defined above |
416 The transition system @{text "root \<midarrow>x\<rightarrow> root'"} defined above |
417 determines a unique result @{term root'} from given @{term root} and |
417 determines a unique result @{term root'} from given @{term root} and |
418 @{term x} (this is holds rather trivially, since there is even only |
418 @{term x} (this is holds rather trivially, since there is even only |
419 one clause for each operation). This uniqueness statement will |
419 one clause for each operation). This uniqueness statement will |
420 simplify our subsequent development to some extent, since we only |
420 simplify our subsequent development to some extent, since we only |
421 have to reason about a partial function rather than a general |
421 have to reason about a partial function rather than a general |
422 relation. |
422 relation. |
423 *} |
423 \<close> |
424 |
424 |
425 theorem transition_uniq: |
425 theorem transition_uniq: |
426 assumes root': "root \<midarrow>x\<rightarrow> root'" |
426 assumes root': "root \<midarrow>x\<rightarrow> root'" |
427 and root'': "root \<midarrow>x\<rightarrow> root''" |
427 and root'': "root \<midarrow>x\<rightarrow> root''" |
428 shows "root' = root''" |
428 shows "root' = root''" |
451 next |
451 next |
452 case readdir |
452 case readdir |
453 with root' show ?thesis by cases blast+ |
453 with root' show ?thesis by cases blast+ |
454 qed |
454 qed |
455 |
455 |
456 text {* |
456 text \<open> |
457 \medskip Apparently, file-system transitions are \emph{type-safe} in |
457 \medskip Apparently, file-system transitions are \emph{type-safe} in |
458 the sense that the result of transforming an actual directory yields |
458 the sense that the result of transforming an actual directory yields |
459 again a directory. |
459 again a directory. |
460 *} |
460 \<close> |
461 |
461 |
462 theorem transition_type_safe: |
462 theorem transition_type_safe: |
463 assumes tr: "root \<midarrow>x\<rightarrow> root'" |
463 assumes tr: "root \<midarrow>x\<rightarrow> root'" |
464 and inv: "\<exists>att dir. root = Env att dir" |
464 and inv: "\<exists>att dir. root = Env att dir" |
465 shows "\<exists>att dir. root' = Env att dir" |
465 shows "\<exists>att dir. root' = Env att dir" |
474 by cases auto |
474 by cases auto |
475 with inv Cons show ?thesis |
475 with inv Cons show ?thesis |
476 by (auto simp add: update_eq split: list.splits) |
476 by (auto simp add: update_eq split: list.splits) |
477 qed |
477 qed |
478 |
478 |
479 text {* |
479 text \<open> |
480 The previous result may be seen as the most basic invariant on the |
480 The previous result may be seen as the most basic invariant on the |
481 file-system state that is enforced by any proper kernel |
481 file-system state that is enforced by any proper kernel |
482 implementation. So user processes --- being bound to the |
482 implementation. So user processes --- being bound to the |
483 system-call interface --- may never mess up a file-system such that |
483 system-call interface --- may never mess up a file-system such that |
484 the root becomes a plain file instead of a directory, which would be |
484 the root becomes a plain file instead of a directory, which would be |
485 a strange situation indeed. |
485 a strange situation indeed. |
486 *} |
486 \<close> |
487 |
487 |
488 |
488 |
489 subsection {* Iterated transitions *} |
489 subsection \<open>Iterated transitions\<close> |
490 |
490 |
491 text {* |
491 text \<open> |
492 Iterated system transitions via finite sequences of system |
492 Iterated system transitions via finite sequences of system |
493 operations are modeled inductively as follows. In a sense, this |
493 operations are modeled inductively as follows. In a sense, this |
494 relation describes the cumulative effect of the sequence of |
494 relation describes the cumulative effect of the sequence of |
495 system-calls issued by a number of running processes over a finite |
495 system-calls issued by a number of running processes over a finite |
496 amount of time. |
496 amount of time. |
497 *} |
497 \<close> |
498 |
498 |
499 inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" |
499 inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" |
500 ("_ =_\<Rightarrow> _" [90, 1000, 90] 100) |
500 ("_ =_\<Rightarrow> _" [90, 1000, 90] 100) |
501 where |
501 where |
502 nil: "root =[]\<Rightarrow> root" |
502 nil: "root =[]\<Rightarrow> root" |
503 | cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''" |
503 | cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''" |
504 |
504 |
505 text {* |
505 text \<open> |
506 \medskip We establish a few basic facts relating iterated |
506 \medskip We establish a few basic facts relating iterated |
507 transitions with single ones, according to the recursive structure |
507 transitions with single ones, according to the recursive structure |
508 of lists. |
508 of lists. |
509 *} |
509 \<close> |
510 |
510 |
511 lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')" |
511 lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')" |
512 proof |
512 proof |
513 assume "root =[]\<Rightarrow> root'" |
513 assume "root =[]\<Rightarrow> root'" |
514 then show "root = root'" by cases simp_all |
514 then show "root = root'" by cases simp_all |
527 assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''" |
527 assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''" |
528 then show "root =(x # xs)\<Rightarrow> root''" |
528 then show "root =(x # xs)\<Rightarrow> root''" |
529 by (blast intro: transitions.cons) |
529 by (blast intro: transitions.cons) |
530 qed |
530 qed |
531 |
531 |
532 text {* |
532 text \<open> |
533 The next two rules show how to ``destruct'' known transition |
533 The next two rules show how to ``destruct'' known transition |
534 sequences. Note that the second one actually relies on the |
534 sequences. Note that the second one actually relies on the |
535 uniqueness property of the basic transition system (see |
535 uniqueness property of the basic transition system (see |
536 \secref{sec:unix-single-trans}). |
536 \secref{sec:unix-single-trans}). |
537 *} |
537 \<close> |
538 |
538 |
539 lemma transitions_nilD: "root =[]\<Rightarrow> root' \<Longrightarrow> root' = root" |
539 lemma transitions_nilD: "root =[]\<Rightarrow> root' \<Longrightarrow> root' = root" |
540 by (simp add: transitions_nil_eq) |
540 by (simp add: transitions_nil_eq) |
541 |
541 |
542 lemma transitions_consD: |
542 lemma transitions_consD: |
548 by cases simp_all |
548 by cases simp_all |
549 from r' hd have "r' = root'" by (rule transition_uniq) |
549 from r' hd have "r' = root'" by (rule transition_uniq) |
550 with root'' show "root' =xs\<Rightarrow> root''" by simp |
550 with root'' show "root' =xs\<Rightarrow> root''" by simp |
551 qed |
551 qed |
552 |
552 |
553 text {* |
553 text \<open> |
554 \medskip The following fact shows how an invariant @{term Q} of |
554 \medskip The following fact shows how an invariant @{term Q} of |
555 single transitions with property @{term P} may be transferred to |
555 single transitions with property @{term P} may be transferred to |
556 iterated transitions. The proof is rather obvious by rule induction |
556 iterated transitions. The proof is rather obvious by rule induction |
557 over the definition of @{term "root =xs\<Rightarrow> root'"}. |
557 over the definition of @{term "root =xs\<Rightarrow> root'"}. |
558 *} |
558 \<close> |
559 |
559 |
560 lemma transitions_invariant: |
560 lemma transitions_invariant: |
561 assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'" |
561 assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'" |
562 and trans: "root =xs\<Rightarrow> root'" |
562 and trans: "root =xs\<Rightarrow> root'" |
563 shows "Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'" |
563 shows "Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'" |
565 proof induct |
565 proof induct |
566 case nil |
566 case nil |
567 show ?case by (rule nil.prems) |
567 show ?case by (rule nil.prems) |
568 next |
568 next |
569 case (cons root x root' xs root'') |
569 case (cons root x root' xs root'') |
570 note P = `\<forall>x \<in> set (x # xs). P x` |
570 note P = \<open>\<forall>x \<in> set (x # xs). P x\<close> |
571 then have "P x" by simp |
571 then have "P x" by simp |
572 with `root \<midarrow>x\<rightarrow> root'` and `Q root` have Q': "Q root'" by (rule r) |
572 with \<open>root \<midarrow>x\<rightarrow> root'\<close> and \<open>Q root\<close> have Q': "Q root'" by (rule r) |
573 from P have "\<forall>x \<in> set xs. P x" by simp |
573 from P have "\<forall>x \<in> set xs. P x" by simp |
574 with Q' show "Q root''" by (rule cons.hyps) |
574 with Q' show "Q root''" by (rule cons.hyps) |
575 qed |
575 qed |
576 |
576 |
577 text {* |
577 text \<open> |
578 As an example of applying the previous result, we transfer the basic |
578 As an example of applying the previous result, we transfer the basic |
579 type-safety property (see \secref{sec:unix-single-trans}) from |
579 type-safety property (see \secref{sec:unix-single-trans}) from |
580 single transitions to iterated ones, which is a rather obvious |
580 single transitions to iterated ones, which is a rather obvious |
581 result indeed. |
581 result indeed. |
582 *} |
582 \<close> |
583 |
583 |
584 theorem transitions_type_safe: |
584 theorem transitions_type_safe: |
585 assumes "root =xs\<Rightarrow> root'" |
585 assumes "root =xs\<Rightarrow> root'" |
586 and "\<exists>att dir. root = Env att dir" |
586 and "\<exists>att dir. root = Env att dir" |
587 shows "\<exists>att dir. root' = Env att dir" |
587 shows "\<exists>att dir. root' = Env att dir" |
589 proof (rule transitions_invariant) |
589 proof (rule transitions_invariant) |
590 show "\<forall>x \<in> set xs. True" by blast |
590 show "\<forall>x \<in> set xs. True" by blast |
591 qed |
591 qed |
592 |
592 |
593 |
593 |
594 section {* Executable sequences *} |
594 section \<open>Executable sequences\<close> |
595 |
595 |
596 text {* |
596 text \<open> |
597 An inductively defined relation such as the one of @{text "root \<midarrow>x\<rightarrow> |
597 An inductively defined relation such as the one of @{text "root \<midarrow>x\<rightarrow> |
598 root'"} (see \secref{sec:unix-syscall}) has two main aspects. First |
598 root'"} (see \secref{sec:unix-syscall}) has two main aspects. First |
599 of all, the resulting system admits a certain set of transition |
599 of all, the resulting system admits a certain set of transition |
600 rules (introductions) as given in the specification. Furthermore, |
600 rules (introductions) as given in the specification. Furthermore, |
601 there is an explicit least-fixed-point construction involved, which |
601 there is an explicit least-fixed-point construction involved, which |
612 we do not refer to induction over the whole transition system here. |
612 we do not refer to induction over the whole transition system here. |
613 So this is still purely positive reasoning about possible |
613 So this is still purely positive reasoning about possible |
614 executions; exhaustive reasoning will be employed only later on (see |
614 executions; exhaustive reasoning will be employed only later on (see |
615 \secref{sec:unix-bogosity}), when we shall demonstrate that certain |
615 \secref{sec:unix-bogosity}), when we shall demonstrate that certain |
616 behavior is \emph{not} possible. |
616 behavior is \emph{not} possible. |
617 *} |
617 \<close> |
618 |
618 |
619 |
619 |
620 subsection {* Possible transitions *} |
620 subsection \<open>Possible transitions\<close> |
621 |
621 |
622 text {* |
622 text \<open> |
623 Rather obviously, a list of system operations can be executed within |
623 Rather obviously, a list of system operations can be executed within |
624 a certain state if there is a result state reached by an iterated |
624 a certain state if there is a result state reached by an iterated |
625 transition. |
625 transition. |
626 *} |
626 \<close> |
627 |
627 |
628 definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')" |
628 definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')" |
629 |
629 |
630 lemma can_exec_nil: "can_exec root []" |
630 lemma can_exec_nil: "can_exec root []" |
631 unfolding can_exec_def by (blast intro: transitions.intros) |
631 unfolding can_exec_def by (blast intro: transitions.intros) |
632 |
632 |
633 lemma can_exec_cons: |
633 lemma can_exec_cons: |
634 "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> can_exec root' xs \<Longrightarrow> can_exec root (x # xs)" |
634 "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> can_exec root' xs \<Longrightarrow> can_exec root (x # xs)" |
635 unfolding can_exec_def by (blast intro: transitions.intros) |
635 unfolding can_exec_def by (blast intro: transitions.intros) |
636 |
636 |
637 text {* |
637 text \<open> |
638 \medskip In case that we already know that a certain sequence can be |
638 \medskip In case that we already know that a certain sequence can be |
639 executed we may destruct it backwardly into individual transitions. |
639 executed we may destruct it backwardly into individual transitions. |
640 *} |
640 \<close> |
641 |
641 |
642 lemma can_exec_snocD: "can_exec root (xs @ [y]) |
642 lemma can_exec_snocD: "can_exec root (xs @ [y]) |
643 \<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''" |
643 \<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''" |
644 proof (induct xs arbitrary: root) |
644 proof (induct xs arbitrary: root) |
645 case Nil |
645 case Nil |
646 then show ?case |
646 then show ?case |
647 by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq) |
647 by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq) |
648 next |
648 next |
649 case (Cons x xs) |
649 case (Cons x xs) |
650 from `can_exec root ((x # xs) @ [y])` obtain r root'' where |
650 from \<open>can_exec root ((x # xs) @ [y])\<close> obtain r root'' where |
651 x: "root \<midarrow>x\<rightarrow> r" and |
651 x: "root \<midarrow>x\<rightarrow> r" and |
652 xs_y: "r =(xs @ [y])\<Rightarrow> root''" |
652 xs_y: "r =(xs @ [y])\<Rightarrow> root''" |
653 by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq) |
653 by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq) |
654 from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'" |
654 from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'" |
655 unfolding can_exec_def by blast |
655 unfolding can_exec_def by blast |
657 by (rule transitions.cons) |
657 by (rule transitions.cons) |
658 with y show ?case by blast |
658 with y show ?case by blast |
659 qed |
659 qed |
660 |
660 |
661 |
661 |
662 subsection {* Example executions \label{sec:unix-examples} *} |
662 subsection \<open>Example executions \label{sec:unix-examples}\<close> |
663 |
663 |
664 text {* |
664 text \<open> |
665 We are now ready to perform a few experiments within our formal |
665 We are now ready to perform a few experiments within our formal |
666 model of Unix system-calls. The common technique is to alternate |
666 model of Unix system-calls. The common technique is to alternate |
667 introduction rules of the transition system (see |
667 introduction rules of the transition system (see |
668 \secref{sec:unix-trans}), and steps to solve any emerging side |
668 \secref{sec:unix-trans}), and steps to solve any emerging side |
669 conditions using algebraic properties of the underlying file-system |
669 conditions using algebraic properties of the underlying file-system |
670 structures (see \secref{sec:unix-file-system}). |
670 structures (see \secref{sec:unix-file-system}). |
671 *} |
671 \<close> |
672 |
672 |
673 lemmas eval = access_def init_def |
673 lemmas eval = access_def init_def |
674 |
674 |
675 theorem "u \<in> users \<Longrightarrow> can_exec (init users) |
675 theorem "u \<in> users \<Longrightarrow> can_exec (init users) |
676 [Mkdir u perms [u, name]]" |
676 [Mkdir u perms [u, name]]" |
677 apply (rule can_exec_cons) |
677 apply (rule can_exec_cons) |
678 -- {* back-chain @{term can_exec} (of @{term [source] Cons}) *} |
678 -- \<open>back-chain @{term can_exec} (of @{term [source] Cons})\<close> |
679 apply (rule mkdir) |
679 apply (rule mkdir) |
680 -- {* back-chain @{term Mkdir} *} |
680 -- \<open>back-chain @{term Mkdir}\<close> |
681 apply (force simp add: eval)+ |
681 apply (force simp add: eval)+ |
682 -- {* solve preconditions of @{term Mkdir} *} |
682 -- \<open>solve preconditions of @{term Mkdir}\<close> |
683 apply (simp add: eval) |
683 apply (simp add: eval) |
684 -- {* peek at resulting dir (optional) *} |
684 -- \<open>peek at resulting dir (optional)\<close> |
685 txt {* @{subgoals [display]} *} |
685 txt \<open>@{subgoals [display]}\<close> |
686 apply (rule can_exec_nil) |
686 apply (rule can_exec_nil) |
687 -- {* back-chain @{term can_exec} (of @{term [source] Nil}) *} |
687 -- \<open>back-chain @{term can_exec} (of @{term [source] Nil})\<close> |
688 done |
688 done |
689 |
689 |
690 text {* |
690 text \<open> |
691 By inspecting the result shown just before the final step above, we |
691 By inspecting the result shown just before the final step above, we |
692 may gain confidence that our specification of Unix system-calls |
692 may gain confidence that our specification of Unix system-calls |
693 actually makes sense. Further common errors are usually exhibited |
693 actually makes sense. Further common errors are usually exhibited |
694 when preconditions of transition rules fail unexpectedly. |
694 when preconditions of transition rules fail unexpectedly. |
695 |
695 |
696 \medskip Here are a few further experiments, using the same |
696 \medskip Here are a few further experiments, using the same |
697 techniques as before. |
697 techniques as before. |
698 *} |
698 \<close> |
699 |
699 |
700 theorem "u \<in> users \<Longrightarrow> can_exec (init users) |
700 theorem "u \<in> users \<Longrightarrow> can_exec (init users) |
701 [Creat u perms [u, name], |
701 [Creat u perms [u, name], |
702 Unlink u [u, name]]" |
702 Unlink u [u, name]]" |
703 apply (rule can_exec_cons) |
703 apply (rule can_exec_cons) |
706 apply (simp add: eval) |
706 apply (simp add: eval) |
707 apply (rule can_exec_cons) |
707 apply (rule can_exec_cons) |
708 apply (rule unlink) |
708 apply (rule unlink) |
709 apply (force simp add: eval)+ |
709 apply (force simp add: eval)+ |
710 apply (simp add: eval) |
710 apply (simp add: eval) |
711 txt {* peek at result: @{subgoals [display]} *} |
711 txt \<open>peek at result: @{subgoals [display]}\<close> |
712 apply (rule can_exec_nil) |
712 apply (rule can_exec_nil) |
713 done |
713 done |
714 |
714 |
715 theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^sub>1 \<Longrightarrow> |
715 theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^sub>1 \<Longrightarrow> |
716 Readable \<in> perms\<^sub>2 \<Longrightarrow> name\<^sub>3 \<noteq> name\<^sub>4 \<Longrightarrow> |
716 Readable \<in> perms\<^sub>2 \<Longrightarrow> name\<^sub>3 \<noteq> name\<^sub>4 \<Longrightarrow> |
720 Creat u' perms\<^sub>3 [u, name\<^sub>1, name\<^sub>2, name\<^sub>3], |
720 Creat u' perms\<^sub>3 [u, name\<^sub>1, name\<^sub>2, name\<^sub>3], |
721 Creat u' perms\<^sub>3 [u, name\<^sub>1, name\<^sub>2, name\<^sub>4], |
721 Creat u' perms\<^sub>3 [u, name\<^sub>1, name\<^sub>2, name\<^sub>4], |
722 Readdir u {name\<^sub>3, name\<^sub>4} [u, name\<^sub>1, name\<^sub>2]]" |
722 Readdir u {name\<^sub>3, name\<^sub>4} [u, name\<^sub>1, name\<^sub>2]]" |
723 apply (rule can_exec_cons, rule transition.intros, |
723 apply (rule can_exec_cons, rule transition.intros, |
724 (force simp add: eval)+, (simp add: eval)?)+ |
724 (force simp add: eval)+, (simp add: eval)?)+ |
725 txt {* peek at result: @{subgoals [display]} *} |
725 txt \<open>peek at result: @{subgoals [display]}\<close> |
726 apply (rule can_exec_nil) |
726 apply (rule can_exec_nil) |
727 done |
727 done |
728 |
728 |
729 theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^sub>1 \<Longrightarrow> Readable \<in> perms\<^sub>3 \<Longrightarrow> |
729 theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^sub>1 \<Longrightarrow> Readable \<in> perms\<^sub>3 \<Longrightarrow> |
730 can_exec (init users) |
730 can_exec (init users) |
733 Creat u' perms\<^sub>3 [u, name\<^sub>1, name\<^sub>2, name\<^sub>3], |
733 Creat u' perms\<^sub>3 [u, name\<^sub>1, name\<^sub>2, name\<^sub>3], |
734 Write u' ''foo'' [u, name\<^sub>1, name\<^sub>2, name\<^sub>3], |
734 Write u' ''foo'' [u, name\<^sub>1, name\<^sub>2, name\<^sub>3], |
735 Read u ''foo'' [u, name\<^sub>1, name\<^sub>2, name\<^sub>3]]" |
735 Read u ''foo'' [u, name\<^sub>1, name\<^sub>2, name\<^sub>3]]" |
736 apply (rule can_exec_cons, rule transition.intros, |
736 apply (rule can_exec_cons, rule transition.intros, |
737 (force simp add: eval)+, (simp add: eval)?)+ |
737 (force simp add: eval)+, (simp add: eval)?)+ |
738 txt {* peek at result: @{subgoals [display]} *} |
738 txt \<open>peek at result: @{subgoals [display]}\<close> |
739 apply (rule can_exec_nil) |
739 apply (rule can_exec_nil) |
740 done |
740 done |
741 |
741 |
742 |
742 |
743 section {* Odd effects --- treated formally \label{sec:unix-bogosity} *} |
743 section \<open>Odd effects --- treated formally \label{sec:unix-bogosity}\<close> |
744 |
744 |
745 text {* |
745 text \<open> |
746 We are now ready to give a completely formal treatment of the |
746 We are now ready to give a completely formal treatment of the |
747 slightly odd situation discussed in the introduction (see |
747 slightly odd situation discussed in the introduction (see |
748 \secref{sec:unix-intro}): the file-system can easily reach a state |
748 \secref{sec:unix-intro}): the file-system can easily reach a state |
749 where a user is unable to remove his very own directory, because it |
749 where a user is unable to remove his very own directory, because it |
750 is still populated by items placed there by another user in an |
750 is still populated by items placed there by another user in an |
751 uncouth manner. |
751 uncouth manner. |
752 *} |
752 \<close> |
753 |
753 |
754 subsection {* The general procedure \label{sec:unix-inv-procedure} *} |
754 subsection \<open>The general procedure \label{sec:unix-inv-procedure}\<close> |
755 |
755 |
756 text {* |
756 text \<open> |
757 The following theorem expresses the general procedure we are |
757 The following theorem expresses the general procedure we are |
758 following to achieve the main result. |
758 following to achieve the main result. |
759 *} |
759 \<close> |
760 |
760 |
761 theorem general_procedure: |
761 theorem general_procedure: |
762 assumes cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False" |
762 assumes cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False" |
763 and init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root" |
763 and init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root" |
764 and preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'" |
764 and preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'" |
778 from this y have False by (rule cannot_y) |
778 from this y have False by (rule cannot_y) |
779 } |
779 } |
780 then show ?thesis by blast |
780 then show ?thesis by blast |
781 qed |
781 qed |
782 |
782 |
783 text {* |
783 text \<open> |
784 Here @{prop "P x"} refers to the restriction on file-system |
784 Here @{prop "P x"} refers to the restriction on file-system |
785 operations that are admitted after having reached the critical |
785 operations that are admitted after having reached the critical |
786 configuration; according to the problem specification this will |
786 configuration; according to the problem specification this will |
787 become @{prop "uid_of x = user\<^sub>1"} later on. Furthermore, |
787 become @{prop "uid_of x = user\<^sub>1"} later on. Furthermore, |
788 @{term y} refers to the operations we claim to be impossible to |
788 @{term y} refers to the operations we claim to be impossible to |
789 perform afterwards, we will take @{term Rmdir} later. Moreover |
789 perform afterwards, we will take @{term Rmdir} later. Moreover |
790 @{term Q} is a suitable (auxiliary) invariant over the file-system; |
790 @{term Q} is a suitable (auxiliary) invariant over the file-system; |
791 choosing @{term Q} adequately is very important to make the proof |
791 choosing @{term Q} adequately is very important to make the proof |
792 work (see \secref{sec:unix-inv-lemmas}). |
792 work (see \secref{sec:unix-inv-lemmas}). |
793 *} |
793 \<close> |
794 |
794 |
795 |
795 |
796 subsection {* The particular situation *} |
796 subsection \<open>The particular situation\<close> |
797 |
797 |
798 text {* |
798 text \<open> |
799 We introduce a few global declarations and axioms to describe our |
799 We introduce a few global declarations and axioms to describe our |
800 particular situation considered here. Thus we avoid excessive use |
800 particular situation considered here. Thus we avoid excessive use |
801 of local parameters in the subsequent development. |
801 of local parameters in the subsequent development. |
802 *} |
802 \<close> |
803 |
803 |
804 locale situation = |
804 locale situation = |
805 fixes users :: "uid set" |
805 fixes users :: "uid set" |
806 and user\<^sub>1 :: uid |
806 and user\<^sub>1 :: uid |
807 and user\<^sub>2 :: uid |
807 and user\<^sub>2 :: uid |
825 Mkdir user\<^sub>2 perms\<^sub>2 [user\<^sub>1, name\<^sub>1, name\<^sub>2], |
825 Mkdir user\<^sub>2 perms\<^sub>2 [user\<^sub>1, name\<^sub>1, name\<^sub>2], |
826 Creat user\<^sub>2 perms\<^sub>2 [user\<^sub>1, name\<^sub>1, name\<^sub>2, name\<^sub>3]]" |
826 Creat user\<^sub>2 perms\<^sub>2 [user\<^sub>1, name\<^sub>1, name\<^sub>2, name\<^sub>3]]" |
827 definition |
827 definition |
828 "bogus_path = [user\<^sub>1, name\<^sub>1, name\<^sub>2]" |
828 "bogus_path = [user\<^sub>1, name\<^sub>1, name\<^sub>2]" |
829 |
829 |
830 text {* |
830 text \<open> |
831 The @{term bogus} operations are the ones that lead into the uncouth |
831 The @{term bogus} operations are the ones that lead into the uncouth |
832 situation; @{term bogus_path} is the key position within the |
832 situation; @{term bogus_path} is the key position within the |
833 file-system where things go awry. |
833 file-system where things go awry. |
834 *} |
834 \<close> |
835 |
835 |
836 |
836 |
837 subsection {* Invariance lemmas \label{sec:unix-inv-lemmas} *} |
837 subsection \<open>Invariance lemmas \label{sec:unix-inv-lemmas}\<close> |
838 |
838 |
839 text {* |
839 text \<open> |
840 The following invariant over the root file-system describes the |
840 The following invariant over the root file-system describes the |
841 bogus situation in an abstract manner: located at a certain @{term |
841 bogus situation in an abstract manner: located at a certain @{term |
842 path} within the file-system is a non-empty directory that is |
842 path} within the file-system is a non-empty directory that is |
843 neither owned nor writable by @{term user\<^sub>1}. |
843 neither owned nor writable by @{term user\<^sub>1}. |
844 *} |
844 \<close> |
845 |
845 |
846 definition |
846 definition |
847 "invariant root path = |
847 "invariant root path = |
848 (\<exists>att dir. |
848 (\<exists>att dir. |
849 access root path user\<^sub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> |
849 access root path user\<^sub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> |
850 user\<^sub>1 \<noteq> owner att \<and> |
850 user\<^sub>1 \<noteq> owner att \<and> |
851 access root path user\<^sub>1 {Writable} = None)" |
851 access root path user\<^sub>1 {Writable} = None)" |
852 |
852 |
853 text {* |
853 text \<open> |
854 Following the general procedure (see |
854 Following the general procedure (see |
855 \secref{sec:unix-inv-procedure}) we will now establish the three key |
855 \secref{sec:unix-inv-procedure}) we will now establish the three key |
856 lemmas required to yield the final result. |
856 lemmas required to yield the final result. |
857 |
857 |
858 \begin{enumerate} |
858 \begin{enumerate} |
878 Moreover the invariant has to be sufficiently abstract, lest the |
878 Moreover the invariant has to be sufficiently abstract, lest the |
879 proof become cluttered by confusing detail. |
879 proof become cluttered by confusing detail. |
880 |
880 |
881 \medskip The first two lemmas are technically straight forward --- |
881 \medskip The first two lemmas are technically straight forward --- |
882 we just have to inspect rather special cases. |
882 we just have to inspect rather special cases. |
883 *} |
883 \<close> |
884 |
884 |
885 lemma cannot_rmdir: |
885 lemma cannot_rmdir: |
886 assumes inv: "invariant root bogus_path" |
886 assumes inv: "invariant root bogus_path" |
887 and rmdir: "root \<midarrow>(Rmdir user\<^sub>1 [user\<^sub>1, name\<^sub>1])\<rightarrow> root'" |
887 and rmdir: "root \<midarrow>(Rmdir user\<^sub>1 [user\<^sub>1, name\<^sub>1])\<rightarrow> root'" |
888 shows False |
888 shows False |
911 -- "reach final result" |
911 -- "reach final result" |
912 apply (simp add: invariant_def eval) |
912 apply (simp add: invariant_def eval) |
913 -- "check the invariant" |
913 -- "check the invariant" |
914 done |
914 done |
915 |
915 |
916 text {* |
916 text \<open> |
917 \medskip At last we are left with the main effort to show that the |
917 \medskip At last we are left with the main effort to show that the |
918 ``bogosity'' invariant is preserved by any file-system operation |
918 ``bogosity'' invariant is preserved by any file-system operation |
919 performed by @{term user\<^sub>1} alone. Note that this holds for |
919 performed by @{term user\<^sub>1} alone. Note that this holds for |
920 any @{term path} given, the particular @{term bogus_path} is not |
920 any @{term path} given, the particular @{term bogus_path} is not |
921 required here. |
921 required here. |
922 *} |
922 \<close> |
923 |
923 |
924 lemma preserve_invariant: |
924 lemma preserve_invariant: |
925 assumes tr: "root \<midarrow>x\<rightarrow> root'" |
925 assumes tr: "root \<midarrow>x\<rightarrow> root'" |
926 and inv: "invariant root path" |
926 and inv: "invariant root path" |
927 and uid: "uid_of x = user\<^sub>1" |
927 and uid: "uid_of x = user\<^sub>1" |
1054 qed |
1054 qed |
1055 qed |
1055 qed |
1056 qed |
1056 qed |
1057 |
1057 |
1058 |
1058 |
1059 subsection {* Putting it all together \label{sec:unix-main-result} *} |
1059 subsection \<open>Putting it all together \label{sec:unix-main-result}\<close> |
1060 |
1060 |
1061 text {* |
1061 text \<open> |
1062 The main result is now imminent, just by composing the three |
1062 The main result is now imminent, just by composing the three |
1063 invariance lemmas (see \secref{sec:unix-inv-lemmas}) according the the |
1063 invariance lemmas (see \secref{sec:unix-inv-lemmas}) according the the |
1064 overall procedure (see \secref{sec:unix-inv-procedure}). |
1064 overall procedure (see \secref{sec:unix-inv-procedure}). |
1065 *} |
1065 \<close> |
1066 |
1066 |
1067 corollary |
1067 corollary |
1068 assumes bogus: "init users =bogus\<Rightarrow> root" |
1068 assumes bogus: "init users =bogus\<Rightarrow> root" |
1069 shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^sub>1) \<and> |
1069 shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^sub>1) \<and> |
1070 can_exec root (xs @ [Rmdir user\<^sub>1 [user\<^sub>1, name\<^sub>1]]))" |
1070 can_exec root (xs @ [Rmdir user\<^sub>1 [user\<^sub>1, name\<^sub>1]]))" |