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