author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 47215  ca516aa5b6ce 
child 49077  154f25a162e3 
permissions  rwrr 
10966  1 
(* Title: HOL/Unix/Unix.thy 
2 
Author: Markus Wenzel, TU Muenchen 

3 
*) 

4 

5 
header {* Unix filesystems \label{sec:unixfilesystem} *} 

6 

17455  7 
theory Unix 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
39224
diff
changeset

8 
imports 
44236
b73b7832b384
moved theory Nested_Environment to HOLUnix (a bit too specific for HOLLibrary);
wenzelm
parents:
43433
diff
changeset

9 
Nested_Environment 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
39224
diff
changeset

10 
"~~/src/HOL/Library/List_Prefix" 
17455  11 
begin 
10966  12 

13 
text {* 

14 
We give a simple mathematical model of the basic structures 

15 
underlying the Unix filesystem, together with a few fundamental 

16 
operations that could be imagined to be performed internally by the 

17 
Unix kernel. This forms the basis for the set of Unix systemcalls 

18 
to be introduced later (see \secref{sec:unixtrans}), which are the 

19 
actual interface offered to processes running in userspace. 

20 

21 
\medskip Basically, any Unix file is either a \emph{plain file} or a 

22 
\emph{directory}, consisting of some \emph{content} plus 

23 
\emph{attributes}. The content of a plain file is plain text. The 

24 
content of a directory is a mapping from names to further 

25 
files.\footnote{In fact, this is the only way that names get 

26 
associated with files. In Unix files do \emph{not} have a name in 

27 
itself. Even more, any number of names may be associated with the 

28 
very same file due to \emph{hard links} (although this is excluded 

29 
from our model).} Attributes include information to control various 

30 
ways to access the file (read, write etc.). 

31 

32 
Our model will be quite liberal in omitting excessive detail that is 

33 
easily seen to be ``irrelevant'' for the aspects of Unix 

34 
filesystems to be discussed here. First of all, we ignore 

35 
character and block special files, pipes, sockets, hard links, 

36 
symbolic links, and mount points. 

37 
*} 

38 

39 

40 
subsection {* Names *} 

41 

42 
text {* 

43 
User ids and file name components shall be represented by natural 

44 
numbers (without loss of generality). We do not bother about 

45 
encoding of actual names (e.g.\ strings), nor a mapping between user 

46 
names and user ids as would be present in a reality. 

47 
*} 

48 

41579  49 
type_synonym uid = nat 
50 
type_synonym name = nat 

51 
type_synonym path = "name list" 

10966  52 

53 

54 
subsection {* Attributes *} 

55 

56 
text {* 

57 
Unix file attributes mainly consist of \emph{owner} information and 

58 
a number of \emph{permission} bits which control access for 

59 
``user'', ``group'', and ``others'' (see the Unix man pages @{text 

60 
"chmod(2)"} and @{text "stat(2)"} for more details). 

61 

62 
\medskip Our model of file permissions only considers the ``others'' 

63 
part. The ``user'' field may be omitted without loss of overall 

64 
generality, since the owner is usually able to change it anyway by 

65 
performing @{text chmod}.\footnote{The inclined Unix expert may try 

66 
to figure out some exotic arrangements of a realworld Unix 

67 
filesystem such that the owner of a file is unable to apply the 

68 
@{text chmod} system call.} We omit ``group'' permissions as a 

69 
genuine simplification as we just do not intend to discuss a model 

70 
of multiple groups and group membership, but pretend that everyone 

71 
is member of a single global group.\footnote{A general HOL model of 

72 
user group structures and related issues is given in 

73 
\cite{Naraschewski:2001}.} 

74 
*} 

75 

76 
datatype perm = 

77 
Readable 

78 
 Writable 

79 
 Executable  "(ignored)" 

80 

41579  81 
type_synonym perms = "perm set" 
10966  82 

83 
record att = 

84 
owner :: uid 

85 
others :: perms 

86 

87 
text {* 

88 
For plain files @{term Readable} and @{term Writable} specify read 

89 
and write access to the actual content, i.e.\ the string of text 

90 
stored here. For directories @{term Readable} determines if the set 

91 
of entry names may be accessed, and @{term Writable} controls the 

92 
ability to create or delete any entries (both plain files or 

93 
subdirectories). 

94 

95 
As another simplification, we ignore the @{term Executable} 

96 
permission altogether. In reality it would indicate executable 

97 
plain files (also known as ``binaries''), or control actual lookup 

98 
of directory entries (recall that mere directory browsing is 

99 
controlled via @{term Readable}). Note that the latter means that 

100 
in order to perform any filesystem operation whatsoever, all 

101 
directories encountered on the path would have to grant @{term 

102 
Executable}. We ignore this detail and pretend that all directories 

103 
give @{term Executable} permission to anybody. 

104 
*} 

105 

106 

107 
subsection {* Files *} 

108 

109 
text {* 

110 
In order to model the general tree structure of a Unix filesystem 

111 
we use the arbitrarily branching datatype @{typ "('a, 'b, 'c) env"} 

112 
from the standard library of Isabelle/HOL 

13380  113 
\cite{Baueretal:2002:HOLLibrary}. This type provides 
10966  114 
constructors @{term Val} and @{term Env} as follows: 
115 

116 
\medskip 

117 
{\def\isastyleminor{\isastyle} 

118 
\begin{tabular}{l} 

119 
@{term [source] "Val :: 'a \<Rightarrow> ('a, 'b, 'c) env"} \\ 

120 
@{term [source] "Env :: 'b \<Rightarrow> ('c \<Rightarrow> ('a, 'b, 'c) env option) \<Rightarrow> ('a, 'b, 'c) env"} \\ 

121 
\end{tabular}} 

122 
\medskip 

123 

124 
Here the parameter @{typ 'a} refers to plain values occurring at 

125 
leaf positions, parameter @{typ 'b} to information kept with inner 

126 
branch nodes, and parameter @{typ 'c} to the branching type of the 

127 
tree structure. For our purpose we use the type instance with @{typ 

128 
"att \<times> string"} (representing plain files), @{typ att} (for 

129 
attributes of directory nodes), and @{typ name} (for the index type 

130 
of directory nodes). 

131 
*} 

132 

41579  133 
type_synonym "file" = "(att \<times> string, att, name) env" 
10966  134 

135 
text {* 

136 
\medskip The HOL library also provides @{term lookup} and @{term 

137 
update} operations for general tree structures with the subsequent 

138 
primitive recursive characterizations. 

139 

140 
\medskip 

141 
{\def\isastyleminor{\isastyle} 

142 
\begin{tabular}{l} 

143 
@{term [source] "lookup :: ('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"} \\ 

144 
@{term [source] 

145 
"update :: 'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"} \\ 

146 
\end{tabular}} 

147 

148 
@{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]} 

149 
@{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]} 

150 

151 
Several further properties of these operations are proven in 

13380  152 
\cite{Baueretal:2002:HOLLibrary}. These will be routinely used 
10966  153 
later on without further notice. 
154 

17146
67e9b86ed211
Put quotation marks around some occurrences of "file", since it is now
berghofe
parents:
16670
diff
changeset

155 
\bigskip Apparently, the elements of type @{typ "file"} contain an 
10966  156 
@{typ att} component in either case. We now define a few auxiliary 
157 
operations to manipulate this field uniformly, following the 

158 
conventions for record types in Isabelle/HOL 

159 
\cite{Nipkowetal:2000:HOL}. 

160 
*} 

161 

19086  162 
definition 
163 
"attributes file = 

10966  164 
(case file of 
165 
Val (att, text) \<Rightarrow> att 

166 
 Env att dir \<Rightarrow> att)" 

167 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21372
diff
changeset

168 
definition 
21001  169 
"map_attributes f file = 
10966  170 
(case file of 
21001  171 
Val (att, text) \<Rightarrow> Val (f att, text) 
172 
 Env att dir \<Rightarrow> Env (f att) dir)" 

10966  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 

21001  180 
lemma [simp]: "attributes (map_attributes f file) = f (attributes file)" 
181 
by (cases "file") (simp_all add: attributes_def map_attributes_def 

10966  182 
split_tupled_all) 
183 

21001  184 
lemma [simp]: "map_attributes f (Val (att, text)) = Val (f att, text)" 
185 
by (simp add: map_attributes_def) 

10966  186 

21001  187 
lemma [simp]: "map_attributes f (Env att dir) = Env (f att) dir" 
188 
by (simp add: map_attributes_def) 

10966  189 

190 

191 
subsection {* Initial filesystems *} 

192 

193 
text {* 

194 
Given a set of \emph{known users} a filesystem shall be initialized 

195 
by providing an empty home directory for each user, with readonly 

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 

19086  202 
definition 
203 
"init users = 

10966  204 
Env \<lparr>owner = 0, others = {Readable}\<rparr> 
205 
(\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> empty) 

206 
else None)" 

207 

208 

209 
subsection {* Accessing filesystems *} 

210 

211 
text {* 

212 
The main internal filesystem operation is access of a file by a 

213 
user, requesting a certain set of permissions. The resulting @{typ 

214 
"file option"} indicates if a file had been present at the 

215 
corresponding @{typ path} and if access was granted according to the 

216 
permissions recorded within the filesystem. 

217 

218 
Note that by the rules of Unix filesystem security (e.g.\ 

219 
\cite{Tanenbaum:1992}) both the superuser and owner may always 

220 
access a file unconditionally (in our simplified model). 

221 
*} 

222 

19086  223 
definition 
20321  224 
"access root path uid perms = 
10966  225 
(case lookup root path of 
226 
None \<Rightarrow> None 

227 
 Some file \<Rightarrow> 

228 
if uid = 0 

229 
\<or> uid = owner (attributes file) 

230 
\<or> perms \<subseteq> others (attributes file) 

231 
then Some file 

232 
else None)" 

233 

234 
text {* 

235 
\medskip Successful access to a certain file is the main 

236 
prerequisite for systemcalls to be applicable (cf.\ 

237 
\secref{sec:unixtrans}). Any modification of the filesystem is 

238 
then performed using the basic @{term update} operation. 

239 

240 
\medskip We see that @{term access} is just a wrapper for the basic 

241 
@{term lookup} function, with additional checking of 

242 
attributes. Subsequently we establish a few auxiliary facts that 

243 
stem from the primitive @{term lookup} used within @{term access}. 

244 
*} 

245 

246 
lemma access_empty_lookup: "access root path uid {} = lookup root path" 

247 
by (simp add: access_def split: option.splits) 

248 

249 
lemma access_some_lookup: 

250 
"access root path uid perms = Some file \<Longrightarrow> 

251 
lookup root path = Some file" 

252 
by (simp add: access_def split: option.splits if_splits) 

253 

18372  254 
lemma access_update_other: 
255 
assumes parallel: "path' \<parallel> path" 

256 
shows "access (update path' opt root) path uid perms = access root path uid perms" 

10966  257 
proof  
18372  258 
from parallel obtain y z xs ys zs where 
11072  259 
"y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs" 
10966  260 
by (blast dest: parallel_decomp) 
18372  261 
then have "lookup (update path' opt root) path = lookup root path" 
10966  262 
by (blast intro: lookup_update_other) 
18372  263 
then show ?thesis by (simp only: access_def) 
10966  264 
qed 
265 

266 

267 
section {* Filesystem transitions \label{sec:unixtrans} *} 

268 

269 
subsection {* Unix system calls \label{sec:unixsyscall} *} 

270 

271 
text {* 

272 
According to established operating system design (cf.\ 

273 
\cite{Tanenbaum:1992}) user space processes may only initiate system 

274 
operations by a fixed set of \emph{systemcalls}. This enables the 

275 
kernel to enforce certain security policies in the first 

276 
place.\footnote{Incidently, this is the very same principle employed 

277 
by any ``LCFstyle'' theorem proving system according to Milner's 

278 
principle of ``correctness by construction'', such as Isabelle/HOL 

279 
itself.} 

280 

281 
\medskip In our model of Unix we give a fixed datatype @{text 

282 
operation} for the syntax of systemcalls, together with an 

283 
inductive definition of filesystem state transitions of the form 

284 
@{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics. 

285 
*} 

286 

287 
datatype operation = 

288 
Read uid string path 

289 
 Write uid string path 

290 
 Chmod uid perms path 

291 
 Creat uid perms path 

292 
 Unlink uid path 

293 
 Mkdir uid perms path 

294 
 Rmdir uid path 

295 
 Readdir uid "name set" path 

296 

297 
text {* 

298 
The @{typ uid} field of an operation corresponds to the 

299 
\emph{effective user id} of the underlying process, although our 

300 
model never mentions processes explicitly. The other parameters are 

301 
provided as arguments by the caller; the @{term path} one is common 

302 
to all kinds of systemcalls. 

303 
*} 

304 

44601  305 
primrec uid_of :: "operation \<Rightarrow> uid" 
25974  306 
where 
307 
"uid_of (Read uid text path) = uid" 

308 
 "uid_of (Write uid text path) = uid" 

309 
 "uid_of (Chmod uid perms path) = uid" 

310 
 "uid_of (Creat uid perms path) = uid" 

311 
 "uid_of (Unlink uid path) = uid" 

312 
 "uid_of (Mkdir uid path perms) = uid" 

313 
 "uid_of (Rmdir uid path) = uid" 

314 
 "uid_of (Readdir uid names path) = uid" 

10966  315 

44601  316 
primrec path_of :: "operation \<Rightarrow> path" 
25974  317 
where 
318 
"path_of (Read uid text path) = path" 

319 
 "path_of (Write uid text path) = path" 

320 
 "path_of (Chmod uid perms path) = path" 

321 
 "path_of (Creat uid perms path) = path" 

322 
 "path_of (Unlink uid path) = path" 

323 
 "path_of (Mkdir uid perms path) = path" 

324 
 "path_of (Rmdir uid path) = path" 

325 
 "path_of (Readdir uid names path) = path" 

10966  326 

327 
text {* 

328 
\medskip Note that we have omitted explicit @{text Open} and @{text 

329 
Close} operations, pretending that @{term Read} and @{term Write} 

330 
would already take care of this behind the scenes. Thus we have 

331 
basically treated actual sequences of real systemcalls @{text 

13380  332 
"open"}@{text read}/@{text write}@{text close} as atomic. 
10966  333 

334 
In principle, this could make big a difference in a model with 

335 
explicit concurrent processes. On the other hand, even on a real 

13380  336 
Unix system the exact scheduling of concurrent @{text "open"} and 
10966  337 
@{text close} operations does \emph{not} directly affect the success 
338 
of corresponding @{text read} or @{text write}. Unix allows several 

339 
processes to have files opened at the same time, even for writing! 

340 
Certainly, the result from reading the contents later may be hard to 

341 
predict, but the systemcalls involved here will succeed in any 

342 
case. 

343 

344 
\bigskip The operational semantics of system calls is now specified 

345 
via transitions of the filesystem configuration. This is expressed 

346 
as an inductive relation (although there is no actual recursion 

347 
involved here). 

348 
*} 

349 

44601  350 
inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool" 
351 
("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100) 

21372  352 
where 
10966  353 
read: 
354 
"access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow> 

21372  355 
root \<midarrow>(Read uid text path)\<rightarrow> root"  
36504  356 
"write": 
10966  357 
"access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow> 
21372  358 
root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"  
10966  359 

360 
chmod: 

361 
"access root path uid {} = Some file \<Longrightarrow> 

362 
uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow> 

363 
root \<midarrow>(Chmod uid perms path)\<rightarrow> update path 

25706  364 
(Some (map_attributes (others_update (\<lambda>_. perms)) file)) root"  
10966  365 

366 
creat: 

367 
"path = parent_path @ [name] \<Longrightarrow> 

368 
access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow> 

369 
access root path uid {} = None \<Longrightarrow> 

370 
root \<midarrow>(Creat uid perms path)\<rightarrow> update path 

21372  371 
(Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"  
10966  372 
unlink: 
373 
"path = parent_path @ [name] \<Longrightarrow> 

374 
access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow> 

375 
access root path uid {} = Some (Val plain) \<Longrightarrow> 

21372  376 
root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"  
10966  377 

378 
mkdir: 

379 
"path = parent_path @ [name] \<Longrightarrow> 

380 
access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow> 

381 
access root path uid {} = None \<Longrightarrow> 

382 
root \<midarrow>(Mkdir uid perms path)\<rightarrow> update path 

21372  383 
(Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"  
10966  384 
rmdir: 
385 
"path = parent_path @ [name] \<Longrightarrow> 

386 
access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow> 

387 
access root path uid {} = Some (Env att' empty) \<Longrightarrow> 

21372  388 
root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"  
10966  389 

390 
readdir: 

391 
"access root path uid {Readable} = Some (Env att dir) \<Longrightarrow> 

392 
names = dom dir \<Longrightarrow> 

393 
root \<midarrow>(Readdir uid names path)\<rightarrow> root" 

394 

395 
text {* 

396 
\medskip Certainly, the above specification is central to the whole 

397 
formal development. Any of the results to be established later on 

398 
are only meaningful to the outside world if this transition system 

399 
provides an adequate model of real Unix systems. This kind of 

400 
``realitycheck'' of a formal model is the wellknown problem of 

401 
\emph{validation}. 

402 

403 
If in doubt, one may consider to compare our definition with the 

404 
informal specifications given the corresponding Unix man pages, or 

405 
even peek at an actual implementation such as 

406 
\cite{Torvaldsetal:Linux}. Another common way to gain confidence 

407 
into the formal model is to run simple simulations (see 

408 
\secref{sec:unixexamples}), and check the results with that of 

409 
experiments performed on a real Unix system. 

410 
*} 

411 

412 

413 
subsection {* Basic properties of single transitions \label{sec:unixsingletrans} *} 

414 

415 
text {* 

416 
The transition system @{text "root \<midarrow>x\<rightarrow> root'"} defined above 

417 
determines a unique result @{term root'} from given @{term root} and 

418 
@{term x} (this is holds rather trivially, since there is even only 

419 
one clause for each operation). This uniqueness statement will 

420 
simplify our subsequent development to some extent, since we only 

421 
have to reason about a partial function rather than a general 

422 
relation. 

423 
*} 

424 

18372  425 
theorem transition_uniq: 
426 
assumes root': "root \<midarrow>x\<rightarrow> root'" 

427 
and root'': "root \<midarrow>x\<rightarrow> root''" 

428 
shows "root' = root''" 

429 
using root'' 

430 
proof cases 

431 
case read 

432 
with root' show ?thesis by cases auto 

433 
next 

36504  434 
case "write" 
18372  435 
with root' show ?thesis by cases auto 
436 
next 

437 
case chmod 

438 
with root' show ?thesis by cases auto 

439 
next 

440 
case creat 

441 
with root' show ?thesis by cases auto 

442 
next 

443 
case unlink 

444 
with root' show ?thesis by cases auto 

445 
next 

446 
case mkdir 

447 
with root' show ?thesis by cases auto 

448 
next 

449 
case rmdir 

450 
with root' show ?thesis by cases auto 

451 
next 

452 
case readdir 

45671  453 
with root' show ?thesis by cases blast+ 
10966  454 
qed 
455 

456 
text {* 

457 
\medskip Apparently, filesystem transitions are \emph{typesafe} in 

458 
the sense that the result of transforming an actual directory yields 

459 
again a directory. 

460 
*} 

461 

462 
theorem transition_type_safe: 

18372  463 
assumes tr: "root \<midarrow>x\<rightarrow> root'" 
464 
and inv: "\<exists>att dir. root = Env att dir" 

465 
shows "\<exists>att dir. root' = Env att dir" 

466 
proof (cases "path_of x") 

467 
case Nil 

468 
with tr inv show ?thesis 

469 
by cases (auto simp add: access_def split: if_splits) 

470 
next 

471 
case Cons 

472 
from tr obtain opt where 

473 
"root' = root \<or> root' = update (path_of x) opt root" 

474 
by cases auto 

475 
with inv Cons show ?thesis 

476 
by (auto simp add: update_eq split: list.splits) 

10966  477 
qed 
478 

479 
text {* 

480 
The previous result may be seen as the most basic invariant on the 

481 
filesystem state that is enforced by any proper kernel 

482 
implementation. So user processes  being bound to the 

483 
systemcall interface  may never mess up a filesystem such that 

484 
the root becomes a plain file instead of a directory, which would be 

485 
a strange situation indeed. 

486 
*} 

487 

488 

489 
subsection {* Iterated transitions *} 

490 

491 
text {* 

492 
Iterated system transitions via finite sequences of system 

493 
operations are modeled inductively as follows. In a sense, this 

494 
relation describes the cumulative effect of the sequence of 

495 
systemcalls issued by a number of running processes over a finite 

496 
amount of time. 

497 
*} 

498 

44601  499 
inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" 
500 
("_ =_\<Rightarrow> _" [90, 1000, 90] 100) 

21372  501 
where 
10966  502 
nil: "root =[]\<Rightarrow> root" 
21372  503 
 cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''" 
10966  504 

505 
text {* 

506 
\medskip We establish a few basic facts relating iterated 

507 
transitions with single ones, according to the recursive structure 

508 
of lists. 

509 
*} 

510 

511 
lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')" 

512 
proof 

513 
assume "root =[]\<Rightarrow> root'" 

18372  514 
then show "root = root'" by cases simp_all 
10966  515 
next 
516 
assume "root = root'" 

18372  517 
then show "root =[]\<Rightarrow> root'" by (simp only: transitions.nil) 
10966  518 
qed 
519 

520 
lemma transitions_cons_eq: 

521 
"root =(x # xs)\<Rightarrow> root'' = (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root'')" 

522 
proof 

523 
assume "root =(x # xs)\<Rightarrow> root''" 

18372  524 
then show "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''" 
10966  525 
by cases auto 
526 
next 

527 
assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''" 

18372  528 
then show "root =(x # xs)\<Rightarrow> root''" 
10966  529 
by (blast intro: transitions.cons) 
530 
qed 

531 

532 
text {* 

533 
The next two rules show how to ``destruct'' known transition 

534 
sequences. Note that the second one actually relies on the 

535 
uniqueness property of the basic transition system (see 

536 
\secref{sec:unixsingletrans}). 

537 
*} 

538 

539 
lemma transitions_nilD: "root =[]\<Rightarrow> root' \<Longrightarrow> root' = root" 

540 
by (simp add: transitions_nil_eq) 

541 

542 
lemma transitions_consD: 

18372  543 
assumes list: "root =(x # xs)\<Rightarrow> root''" 
544 
and hd: "root \<midarrow>x\<rightarrow> root'" 

545 
shows "root' =xs\<Rightarrow> root''" 

10966  546 
proof  
18372  547 
from list obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''" 
10966  548 
by cases simp_all 
18372  549 
from r' hd have "r' = root'" by (rule transition_uniq) 
10966  550 
with root'' show "root' =xs\<Rightarrow> root''" by simp 
551 
qed 

552 

553 
text {* 

554 
\medskip The following fact shows how an invariant @{term Q} of 

555 
single transitions with property @{term P} may be transferred to 

556 
iterated transitions. The proof is rather obvious by rule induction 

557 
over the definition of @{term "root =xs\<Rightarrow> root'"}. 

558 
*} 

559 

560 
lemma transitions_invariant: 

47175  561 
assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'" 
18372  562 
and trans: "root =xs\<Rightarrow> root'" 
563 
shows "Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'" 

564 
using trans 

565 
proof induct 

566 
case nil 

23463  567 
show ?case by (rule nil.prems) 
18372  568 
next 
21372  569 
case (cons root x root' xs root'') 
18372  570 
note P = `\<forall>x \<in> set (x # xs). P x` 
571 
then have "P x" by simp 

572 
with `root \<midarrow>x\<rightarrow> root'` and `Q root` have Q': "Q root'" by (rule r) 

573 
from P have "\<forall>x \<in> set xs. P x" by simp 

574 
with Q' show "Q root''" by (rule cons.hyps) 

10966  575 
qed 
576 

577 
text {* 

578 
As an example of applying the previous result, we transfer the basic 

579 
typesafety property (see \secref{sec:unixsingletrans}) from 

580 
single transitions to iterated ones, which is a rather obvious 

581 
result indeed. 

582 
*} 

583 

584 
theorem transitions_type_safe: 

16670  585 
assumes "root =xs\<Rightarrow> root'" 
586 
and "\<exists>att dir. root = Env att dir" 

587 
shows "\<exists>att dir. root' = Env att dir" 

23394  588 
using transition_type_safe and assms 
16670  589 
proof (rule transitions_invariant) 
590 
show "\<forall>x \<in> set xs. True" by blast 

10966  591 
qed 
592 

593 

594 
section {* Executable sequences *} 

595 

596 
text {* 

17455  597 
An inductively defined relation such as the one of @{text "root \<midarrow>x\<rightarrow> 
598 
root'"} (see \secref{sec:unixsyscall}) has two main aspects. First 

599 
of all, the resulting system admits a certain set of transition 

600 
rules (introductions) as given in the specification. Furthermore, 

601 
there is an explicit leastfixedpoint construction involved, which 

602 
results in induction (and caseanalysis) rules to eliminate known 

603 
transitions in an exhaustive manner. 

10966  604 

605 
\medskip Subsequently, we explore our transition system in an 

606 
experimental style, mainly using the introduction rules with basic 

607 
algebraic properties of the underlying structures. The technique 

608 
closely resembles that of Prolog combined with functional evaluation 

609 
in a very simple manner. 

610 

611 
Just as the ``closedworld assumption'' is left implicit in Prolog, 

612 
we do not refer to induction over the whole transition system here. 

613 
So this is still purely positive reasoning about possible 

614 
executions; exhaustive reasoning will be employed only later on (see 

615 
\secref{sec:unixbogosity}), when we shall demonstrate that certain 

616 
behavior is \emph{not} possible. 

617 
*} 

618 

619 

620 
subsection {* Possible transitions *} 

621 

622 
text {* 

623 
Rather obviously, a list of system operations can be executed within 

624 
a certain state if there is a result state reached by an iterated 

625 
transition. 

626 
*} 

627 

44601  628 
definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')" 
10966  629 

630 
lemma can_exec_nil: "can_exec root []" 

18730  631 
unfolding can_exec_def by (blast intro: transitions.intros) 
10966  632 

633 
lemma can_exec_cons: 

634 
"root \<midarrow>x\<rightarrow> root' \<Longrightarrow> can_exec root' xs \<Longrightarrow> can_exec root (x # xs)" 

18730  635 
unfolding can_exec_def by (blast intro: transitions.intros) 
10966  636 

637 
text {* 

638 
\medskip In case that we already know that a certain sequence can be 

639 
executed we may destruct it backwardly into individual transitions. 

640 
*} 

641 

18372  642 
lemma can_exec_snocD: "can_exec root (xs @ [y]) 
10966  643 
\<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''" 
20503  644 
proof (induct xs arbitrary: root) 
18372  645 
case Nil 
646 
then show ?case 

647 
by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq) 

648 
next 

649 
case (Cons x xs) 

650 
from `can_exec root ((x # xs) @ [y])` obtain r root'' where 

651 
x: "root \<midarrow>x\<rightarrow> r" and 

652 
xs_y: "r =(xs @ [y])\<Rightarrow> root''" 

653 
by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq) 

654 
from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'" 

18730  655 
unfolding can_exec_def by blast 
18372  656 
from x xs have "root =(x # xs)\<Rightarrow> root'" 
657 
by (rule transitions.cons) 

658 
with y show ?case by blast 

10966  659 
qed 
660 

661 

662 
subsection {* Example executions \label{sec:unixexamples} *} 

663 

664 
text {* 

665 
We are now ready to perform a few experiments within our formal 

666 
model of Unix systemcalls. The common technique is to alternate 

667 
introduction rules of the transition system (see 

668 
\secref{sec:unixtrans}), and steps to solve any emerging side 

669 
conditions using algebraic properties of the underlying filesystem 

670 
structures (see \secref{sec:unixfilesystem}). 

671 
*} 

672 

673 
lemmas eval = access_def init_def 

674 

675 
theorem "u \<in> users \<Longrightarrow> can_exec (init users) 

676 
[Mkdir u perms [u, name]]" 

677 
apply (rule can_exec_cons) 

678 
 {* backchain @{term can_exec} (of @{term [source] Cons}) *} 

679 
apply (rule mkdir) 

680 
 {* backchain @{term Mkdir} *} 

681 
apply (force simp add: eval)+ 

682 
 {* solve preconditions of @{term Mkdir} *} 

683 
apply (simp add: eval) 

684 
 {* peek at resulting dir (optional) *} 

685 
txt {* @{subgoals [display]} *} 

686 
apply (rule can_exec_nil) 

687 
 {* backchain @{term can_exec} (of @{term [source] Nil}) *} 

688 
done 

689 

690 
text {* 

691 
By inspecting the result shown just before the final step above, we 

692 
may gain confidence that our specification of Unix systemcalls 

693 
actually makes sense. Further common errors are usually exhibited 

694 
when preconditions of transition rules fail unexpectedly. 

695 

696 
\medskip Here are a few further experiments, using the same 

697 
techniques as before. 

698 
*} 

699 

700 
theorem "u \<in> users \<Longrightarrow> can_exec (init users) 

701 
[Creat u perms [u, name], 

702 
Unlink u [u, name]]" 

703 
apply (rule can_exec_cons) 

704 
apply (rule creat) 

705 
apply (force simp add: eval)+ 

706 
apply (simp add: eval) 

707 
apply (rule can_exec_cons) 

708 
apply (rule unlink) 

709 
apply (force simp add: eval)+ 

710 
apply (simp add: eval) 

711 
txt {* peek at result: @{subgoals [display]} *} 

712 
apply (rule can_exec_nil) 

713 
done 

714 

17455  715 
theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow> 
716 
Readable \<in> perms\<^isub>2 \<Longrightarrow> name\<^isub>3 \<noteq> name\<^isub>4 \<Longrightarrow> 

10966  717 
can_exec (init users) 
17455  718 
[Mkdir u perms\<^isub>1 [u, name\<^isub>1], 
719 
Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2], 

720 
Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>3], 

721 
Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>4], 

722 
Readdir u {name\<^isub>3, name\<^isub>4} [u, name\<^isub>1, name\<^isub>2]]" 

10966  723 
apply (rule can_exec_cons, rule transition.intros, 
724 
(force simp add: eval)+, (simp add: eval)?)+ 

725 
txt {* peek at result: @{subgoals [display]} *} 

726 
apply (rule can_exec_nil) 

727 
done 

728 

17455  729 
theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow> Readable \<in> perms\<^isub>3 \<Longrightarrow> 
10966  730 
can_exec (init users) 
17455  731 
[Mkdir u perms\<^isub>1 [u, name\<^isub>1], 
732 
Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2], 

733 
Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>3], 

734 
Write u' ''foo'' [u, name\<^isub>1, name\<^isub>2, name\<^isub>3], 

735 
Read u ''foo'' [u, name\<^isub>1, name\<^isub>2, name\<^isub>3]]" 

10966  736 
apply (rule can_exec_cons, rule transition.intros, 
737 
(force simp add: eval)+, (simp add: eval)?)+ 

738 
txt {* peek at result: @{subgoals [display]} *} 

739 
apply (rule can_exec_nil) 

740 
done 

741 

742 

743 
section {* Odd effects  treated formally \label{sec:unixbogosity} *} 

744 

745 
text {* 

746 
We are now ready to give a completely formal treatment of the 

747 
slightly odd situation discussed in the introduction (see 

748 
\secref{sec:unixintro}): the filesystem can easily reach a state 

749 
where a user is unable to remove his very own directory, because it 

750 
is still populated by items placed there by another user in an 

751 
uncouth manner. 

752 
*} 

753 

754 
subsection {* The general procedure \label{sec:unixinvprocedure} *} 

755 

756 
text {* 

757 
The following theorem expresses the general procedure we are 

758 
following to achieve the main result. 

759 
*} 

760 

761 
theorem general_procedure: 

18372  762 
assumes cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False" 
763 
and init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root" 

764 
and preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'" 

765 
and init_result: "init users =bs\<Rightarrow> root" 

766 
shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))" 

10966  767 
proof  
768 
{ 

769 
fix xs 

770 
assume Ps: "\<forall>x \<in> set xs. P x" 

771 
assume can_exec: "can_exec root (xs @ [y])" 

772 
then obtain root' root'' where 

773 
xs: "root =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''" 

774 
by (blast dest: can_exec_snocD) 

775 
from init_result have "Q root" by (rule init_inv) 

776 
from preserve_inv xs this Ps have "Q root'" 

777 
by (rule transitions_invariant) 

778 
from this y have False by (rule cannot_y) 

779 
} 

18372  780 
then show ?thesis by blast 
10966  781 
qed 
782 

783 
text {* 

784 
Here @{prop "P x"} refers to the restriction on filesystem 

785 
operations that are admitted after having reached the critical 

786 
configuration; according to the problem specification this will 

17455  787 
become @{prop "uid_of x = user\<^isub>1"} later on. Furthermore, 
788 
@{term y} refers to the operations we claim to be impossible to 

789 
perform afterwards, we will take @{term Rmdir} later. Moreover 

790 
@{term Q} is a suitable (auxiliary) invariant over the filesystem; 

791 
choosing @{term Q} adequately is very important to make the proof 

792 
work (see \secref{sec:unixinvlemmas}). 

10966  793 
*} 
794 

795 

12079  796 
subsection {* The particular situation *} 
10966  797 

798 
text {* 

799 
We introduce a few global declarations and axioms to describe our 

12079  800 
particular situation considered here. Thus we avoid excessive use 
801 
of local parameters in the subsequent development. 

10966  802 
*} 
803 

12079  804 
locale situation = 
805 
fixes users :: "uid set" 

17455  806 
and user\<^isub>1 :: uid 
807 
and user\<^isub>2 :: uid 

808 
and name\<^isub>1 :: name 

809 
and name\<^isub>2 :: name 

810 
and name\<^isub>3 :: name 

811 
and perms\<^isub>1 :: perms 

812 
and perms\<^isub>2 :: perms 

813 
assumes user\<^isub>1_known: "user\<^isub>1 \<in> users" 

814 
and user\<^isub>1_not_root: "user\<^isub>1 \<noteq> 0" 

815 
and users_neq: "user\<^isub>1 \<noteq> user\<^isub>2" 

816 
and perms\<^isub>1_writable: "Writable \<in> perms\<^isub>1" 

817 
and perms\<^isub>2_not_writable: "Writable \<notin> perms\<^isub>2" 

818 
notes facts = user\<^isub>1_known user\<^isub>1_not_root users_neq 

819 
perms\<^isub>1_writable perms\<^isub>2_not_writable 

21029  820 
begin 
10966  821 

21029  822 
definition 
19086  823 
"bogus = 
17455  824 
[Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1], 
825 
Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2], 

826 
Creat user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2, name\<^isub>3]]" 

21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
21372
diff
changeset

827 
definition 
19086  828 
"bogus_path = [user\<^isub>1, name\<^isub>1, name\<^isub>2]" 
10966  829 

830 
text {* 

12079  831 
The @{term bogus} operations are the ones that lead into the uncouth 
832 
situation; @{term bogus_path} is the key position within the 

833 
filesystem where things go awry. 

10966  834 
*} 
835 

836 

837 
subsection {* Invariance lemmas \label{sec:unixinvlemmas} *} 

838 

839 
text {* 

840 
The following invariant over the root filesystem describes the 

841 
bogus situation in an abstract manner: located at a certain @{term 

842 
path} within the filesystem is a nonempty directory that is 

43433  843 
neither owned nor writable by @{term user\<^isub>1}. 
10966  844 
*} 
845 

47099  846 

847 

47215
ca516aa5b6ce
"invariant" is free in main HOL (cf. 56adbf5bcc82, e64ffc96a49f);
wenzelm
parents:
47175
diff
changeset

848 
definition 
20321  849 
"invariant root path = 
10966  850 
(\<exists>att dir. 
17455  851 
access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> 
852 
user\<^isub>1 \<noteq> owner att \<and> 

853 
access root path user\<^isub>1 {Writable} = None)" 

10966  854 

855 
text {* 

856 
Following the general procedure (see 

17455  857 
\secref{sec:unixinvprocedure}) we will now establish the three key 
858 
lemmas required to yield the final result. 

10966  859 

860 
\begin{enumerate} 

861 

862 
\item The invariant is sufficiently strong to entail the 

17455  863 
pathological case that @{term user\<^isub>1} is unable to remove the 
864 
(owned) directory at @{term "[user\<^isub>1, name\<^isub>1]"}. 

10966  865 

866 
\item The invariant does hold after having executed the @{term 

867 
bogus} list of operations (starting with an initial filesystem 

868 
configuration). 

869 

870 
\item The invariant is preserved by any filesystem operation 

17455  871 
performed by @{term user\<^isub>1} alone, without any help by other 
872 
users. 

10966  873 

874 
\end{enumerate} 

875 

876 
As the invariant appears both as assumptions and conclusions in the 

877 
course of proof, its formulation is rather critical for the whole 

878 
development to work out properly. In particular, the third step is 

879 
very sensitive to the invariant being either too strong or too weak. 

880 
Moreover the invariant has to be sufficiently abstract, lest the 

881 
proof become cluttered by confusing detail. 

882 

883 
\medskip The first two lemmas are technically straight forward  

884 
we just have to inspect rather special cases. 

885 
*} 

886 

21029  887 
lemma cannot_rmdir: 
18372  888 
assumes inv: "invariant root bogus_path" 
889 
and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'" 

890 
shows False 

10966  891 
proof  
18372  892 
from inv obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file" 
18730  893 
unfolding invariant_def by blast 
10966  894 
moreover 
18372  895 
from rmdir obtain att where 
17455  896 
"access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)" 
10966  897 
by cases auto 
18372  898 
then have "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2" 
10966  899 
by (simp only: access_empty_lookup lookup_append_some) simp 
900 
ultimately show False by (simp add: bogus_path_def) 

901 
qed 

902 

21029  903 
lemma 
18372  904 
assumes init: "init users =bogus\<Rightarrow> root" 
905 
notes eval = facts access_def init_def 

906 
shows init_invariant: "invariant root bogus_path" 

907 
using init 

908 
apply (unfold bogus_def bogus_path_def) 

909 
apply (drule transitions_consD, rule transition.intros, 

10966  910 
(force simp add: eval)+, (simp add: eval)?)+ 
18372  911 
 "evaluate all operations" 
912 
apply (drule transitions_nilD) 

913 
 "reach final result" 

914 
apply (simp add: invariant_def eval) 

915 
 "check the invariant" 

916 
done 

10966  917 

918 
text {* 

919 
\medskip At last we are left with the main effort to show that the 

920 
``bogosity'' invariant is preserved by any filesystem operation 

17455  921 
performed by @{term user\<^isub>1} alone. Note that this holds for 
922 
any @{term path} given, the particular @{term bogus_path} is not 

10966  923 
required here. 
11004  924 
*} 
10966  925 

21029  926 
lemma preserve_invariant: 
18372  927 
assumes tr: "root \<midarrow>x\<rightarrow> root'" 
928 
and inv: "invariant root path" 

929 
and uid: "uid_of x = user\<^isub>1" 

930 
shows "invariant root' path" 

10966  931 
proof  
932 
from inv obtain att dir where 

17455  933 
inv1: "access root path user\<^isub>1 {} = Some (Env att dir)" and 
10966  934 
inv2: "dir \<noteq> empty" and 
17455  935 
inv3: "user\<^isub>1 \<noteq> owner att" and 
936 
inv4: "access root path user\<^isub>1 {Writable} = None" 

10966  937 
by (auto simp add: invariant_def) 
938 

939 
from inv1 have lookup: "lookup root path = Some (Env att dir)" 

940 
by (simp only: access_empty_lookup) 

941 

17455  942 
from inv1 inv3 inv4 and user\<^isub>1_not_root 
10966  943 
have not_writable: "Writable \<notin> others att" 
39224
39e0d3b86112
tuned proofs (based on fancy gutter icons in Isabelle/jEdit);
wenzelm
parents:
36862
diff
changeset

944 
by (auto simp add: access_def split: option.splits) 
10966  945 

946 
show ?thesis 

947 
proof cases 

948 
assume "root' = root" 

949 
with inv show "invariant root' path" by (simp only:) 

950 
next 

951 
assume changed: "root' \<noteq> root" 

952 
with tr obtain opt where root': "root' = update (path_of x) opt root" 

953 
by cases auto 

954 
show ?thesis 

955 
proof (rule prefix_cases) 

956 
assume "path_of x \<parallel> path" 

957 
with inv root' 

17455  958 
have "\<And>perms. access root' path user\<^isub>1 perms = access root path user\<^isub>1 perms" 
10966  959 
by (simp only: access_update_other) 
960 
with inv show "invariant root' path" 

961 
by (simp only: invariant_def) 

962 
next 

963 
assume "path_of x \<le> path" 

964 
then obtain ys where path: "path = path_of x @ ys" .. 

965 

966 
show ?thesis 

967 
proof (cases ys) 

968 
assume "ys = []" 

17455  969 
with tr uid inv2 inv3 lookup changed path and user\<^isub>1_not_root 
10966  970 
have False 
971 
by cases (auto simp add: access_empty_lookup dest: access_some_lookup) 

18372  972 
then show ?thesis .. 
10966  973 
next 
974 
fix z zs assume ys: "ys = z # zs" 

975 
have "lookup root' path = lookup root path" 

976 
proof  

977 
from inv2 lookup path ys 

978 
have look: "lookup root (path_of x @ z # zs) = Some (Env att dir)" 

979 
by (simp only:) 

980 
then obtain att' dir' file' where 

981 
look': "lookup root (path_of x) = Some (Env att' dir')" and 

982 
dir': "dir' z = Some file'" and 

983 
file': "lookup file' zs = Some (Env att dir)" 

984 
by (blast dest: lookup_some_upper) 

985 

986 
from tr uid changed look' dir' obtain att'' where 

987 
look'': "lookup root' (path_of x) = Some (Env att'' dir')" 

988 
by cases (auto simp add: access_empty_lookup lookup_update_some 

989 
dest: access_some_lookup) 

990 
with dir' file' have "lookup root' (path_of x @ z # zs) = 

991 
Some (Env att dir)" 

992 
by (simp add: lookup_append_some) 

993 
with look path ys show ?thesis 

994 
by simp 

995 
qed 

996 
with inv show "invariant root' path" 

997 
by (simp only: invariant_def access_def) 

998 
qed 

999 
next 

1000 
assume "path < path_of x" 

1001 
then obtain y ys where path: "path_of x = path @ y # ys" .. 

1002 

1003 
obtain dir' where 

1004 
lookup': "lookup root' path = Some (Env att dir')" and 

1005 
inv2': "dir' \<noteq> empty" 

1006 
proof (cases ys) 

1007 
assume "ys = []" 

1008 
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

1009 
with tr uid inv4 changed obtain "file" where 
10966  1010 
"root' = update (path_of x) (Some file) root" 
1011 
by cases auto 

10979  1012 
with lookup parent have "lookup root' path = Some (Env att (dir(y\<mapsto>file)))" 
10966  1013 
by (simp only: update_append_some update_cons_nil_env) 
1014 
moreover have "dir(y\<mapsto>file) \<noteq> empty" by simp 

1015 
ultimately show ?thesis .. 

1016 
next 

1017 
fix z zs assume ys: "ys = z # zs" 

1018 
with lookup root' path 

1019 
have "lookup root' path = Some (update (y # ys) opt (Env att dir))" 

1020 
by (simp only: update_append_some) 

1021 
also obtain file' where 

1022 
"update (y # ys) opt (Env att dir) = Env att (dir(y\<mapsto>file'))" 

1023 
proof  

1024 
have "dir y \<noteq> None" 

1025 
proof  

1026 
have "dir y = lookup (Env att dir) [y]" 

1027 
by (simp split: option.splits) 

1028 
also from lookup have "\<dots> = lookup root (path @ [y])" 

1029 
by (simp only: lookup_append_some) 

1030 
also have "\<dots> \<noteq> None" 

1031 
proof  

1032 
from ys obtain us u where rev_ys: "ys = us @ [u]" 

45671  1033 
by (cases ys rule: rev_cases) simp 
10966  1034 
with tr path 
1035 
have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or> 

1036 
lookup root ((path @ [y]) @ us) \<noteq> None" 

1037 
by cases (auto dest: access_some_lookup) 

18447  1038 
then show ?thesis 
46206  1039 
by (fastforce dest!: lookup_some_append) 
10966  1040 
qed 
1041 
finally show ?thesis . 

1042 
qed 

39224
39e0d3b86112
tuned proofs (based on fancy gutter icons in Isabelle/jEdit);
wenzelm
parents:
36862
diff
changeset

1043 
with ys show ?thesis using that by auto 
10966  1044 
qed 
1045 
also have "dir(y\<mapsto>file') \<noteq> empty" by simp 

1046 
ultimately show ?thesis .. 

1047 
qed 

1048 

17455  1049 
from lookup' have inv1': "access root' path user\<^isub>1 {} = Some (Env att dir')" 
10966  1050 
by (simp only: access_empty_lookup) 
1051 

17455  1052 
from inv3 lookup' and not_writable user\<^isub>1_not_root 
1053 
have "access root' path user\<^isub>1 {Writable} = None" 

10966  1054 
by (simp add: access_def) 
18730  1055 
with inv1' inv2' inv3 show ?thesis unfolding invariant_def by blast 
10966  1056 
qed 
1057 
qed 

1058 
qed 

1059 

1060 

1061 
subsection {* Putting it all together \label{sec:unixmainresult} *} 

1062 

1063 
text {* 

1064 
The main result is now imminent, just by composing the three 

1065 
invariance lemmas (see \secref{sec:unixinvlemmas}) according the the 

1066 
overall procedure (see \secref{sec:unixinvprocedure}). 

1067 
*} 

1068 

21029  1069 
corollary 
13380  1070 
assumes bogus: "init users =bogus\<Rightarrow> root" 
17455  1071 
shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^isub>1) \<and> 
1072 
can_exec root (xs @ [Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1]]))" 

10966  1073 
proof  
13380  1074 
from cannot_rmdir init_invariant preserve_invariant 
1075 
and bogus show ?thesis by (rule general_procedure) 

10966  1076 
qed 
1077 

1078 
end 

21029  1079 

1080 
end 