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