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