summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Unix/Unix.thy

author | wenzelm |

Sat Apr 08 22:51:06 2006 +0200 (2006-04-08) | |

changeset 19363 | 667b5ea637dd |

parent 19086 | 1b3780be6cc2 |

child 20321 | b7c0bf788f50 |

permissions | -rw-r--r-- |

refined 'abbreviation';

1 (* Title: HOL/Unix/Unix.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

4 *)

6 header {* Unix file-systems \label{sec:unix-file-system} *}

8 theory Unix

9 imports Nested_Environment List_Prefix

10 begin

12 text {*

13 We give a simple mathematical model of the basic structures

14 underlying the Unix file-system, together with a few fundamental

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

16 Unix kernel. This forms the basis for the set of Unix system-calls

17 to be introduced later (see \secref{sec:unix-trans}), which are the

18 actual interface offered to processes running in user-space.

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

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

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

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

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

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

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

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

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

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

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

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

33 file-systems to be discussed here. First of all, we ignore

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

35 symbolic links, and mount points.

36 *}

39 subsection {* Names *}

41 text {*

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

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

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

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

46 *}

48 types

49 uid = nat

50 name = nat

51 path = "name list"

54 subsection {* Attributes *}

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).

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

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

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

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

66 to figure out some exotic arrangements of a real-world Unix

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

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

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

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

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

72 user group structures and related issues is given in

73 \cite{Naraschewski:2001}.}

74 *}

76 datatype perm =

77 Readable

78 | Writable

79 | Executable -- "(ignored)"

81 types perms = "perm set"

83 record att =

84 owner :: uid

85 others :: perms

87 text {*

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

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

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

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

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

93 sub-directories).

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

96 permission altogether. In reality it would indicate executable

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

98 of directory entries (recall that mere directory browsing is

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

100 in order to perform any file-system operation whatsoever, all

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

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

103 give @{term Executable} permission to anybody.

104 *}

107 subsection {* Files *}

109 text {*

110 In order to model the general tree structure of a Unix file-system

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

112 from the standard library of Isabelle/HOL

113 \cite{Bauer-et-al:2002:HOL-Library}. This type provides

114 constructors @{term Val} and @{term Env} as follows:

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

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 *}

133 types

134 "file" = "(att \<times> string, att, name) env"

136 text {*

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

138 update} operations for general tree structures with the subsequent

139 primitive recursive characterizations.

141 \medskip

142 {\def\isastyleminor{\isastyle}

143 \begin{tabular}{l}

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

145 @{term [source]

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

147 \end{tabular}}

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

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

152 Several further properties of these operations are proven in

153 \cite{Bauer-et-al:2002:HOL-Library}. These will be routinely used

154 later on without further notice.

156 \bigskip Apparently, the elements of type @{typ "file"} contain an

157 @{typ att} component in either case. We now define a few auxiliary

158 operations to manipulate this field uniformly, following the

159 conventions for record types in Isabelle/HOL

160 \cite{Nipkow-et-al:2000:HOL}.

161 *}

163 definition

164 "attributes file =

165 (case file of

166 Val (att, text) \<Rightarrow> att

167 | Env att dir \<Rightarrow> att)"

169 "attributes_update att file =

170 (case file of

171 Val (att', text) \<Rightarrow> Val (att, text)

172 | Env att' dir \<Rightarrow> Env att dir)"

174 lemma [simp]: "attributes (Val (att, text)) = att"

175 by (simp add: attributes_def)

177 lemma [simp]: "attributes (Env att dir) = att"

178 by (simp add: attributes_def)

180 lemma [simp]: "attributes (file \<lparr>attributes := att\<rparr>) = att"

181 by (cases "file") (simp_all add: attributes_def attributes_update_def

182 split_tupled_all)

184 lemma [simp]: "(Val (att, text)) \<lparr>attributes := att'\<rparr> = Val (att', text)"

185 by (simp add: attributes_update_def)

187 lemma [simp]: "(Env att dir) \<lparr>attributes := att'\<rparr> = Env att' dir"

188 by (simp add: attributes_update_def)

191 subsection {* Initial file-systems *}

193 text {*

194 Given a set of \emph{known users} a file-system shall be initialized

195 by providing an empty home directory for each user, with read-only

196 access for everyone else. (Note that we may directly use the user

197 id as home directory name, since both types have been identified.)

198 Certainly, the very root directory is owned by the super user (who

199 has user id 0).

200 *}

202 definition

203 "init users =

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)"

209 subsection {* Accessing file-systems *}

211 text {*

212 The main internal file-system operation is access of a file by a

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

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 file-system.

218 Note that by the rules of Unix file-system security (e.g.\

219 \cite{Tanenbaum:1992}) both the super-user and owner may always

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

221 *}

223 definition

224 "access root path uid perms \<equiv>

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)"

234 text {*

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

236 prerequisite for system-calls to be applicable (cf.\

237 \secref{sec:unix-trans}). Any modification of the file-system is

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

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 *}

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

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

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)

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"

257 proof -

258 from parallel obtain y z xs ys zs where

259 "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"

260 by (blast dest: parallel_decomp)

261 then have "lookup (update path' opt root) path = lookup root path"

262 by (blast intro: lookup_update_other)

263 then show ?thesis by (simp only: access_def)

264 qed

267 section {* File-system transitions \label{sec:unix-trans} *}

269 subsection {* Unix system calls \label{sec:unix-syscall} *}

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{system-calls}. 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 ``LCF-style'' theorem proving system according to Milner's

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

279 itself.}

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

282 operation} for the syntax of system-calls, together with an

283 inductive definition of file-system state transitions of the form

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

285 *}

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

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 system-calls.

303 *}

305 consts

306 uid_of :: "operation \<Rightarrow> uid"

307 primrec

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

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

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

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

312 "uid_of (Unlink uid path) = uid"

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

314 "uid_of (Rmdir uid path) = uid"

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

317 consts

318 path_of :: "operation \<Rightarrow> path"

319 primrec

320 "path_of (Read uid text path) = path"

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

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

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

324 "path_of (Unlink uid path) = path"

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

326 "path_of (Rmdir uid path) = path"

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

329 text {*

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

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

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

333 basically treated actual sequences of real system-calls @{text

334 "open"}--@{text read}/@{text write}--@{text close} as atomic.

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

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

338 Unix system the exact scheduling of concurrent @{text "open"} and

339 @{text close} operations does \emph{not} directly affect the success

340 of corresponding @{text read} or @{text write}. Unix allows several

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

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

343 predict, but the system-calls involved here will succeed in any

344 case.

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

347 via transitions of the file-system configuration. This is expressed

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

349 involved here).

350 *}

352 consts

353 transition :: "(file \<times> operation \<times> file) set"

355 abbreviation

356 transition_rel ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)

357 "root \<midarrow>x\<rightarrow> root' \<equiv> (root, x, root') \<in> transition"

359 inductive transition

360 intros

362 read:

363 "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>

364 root \<midarrow>(Read uid text path)\<rightarrow> root"

365 write:

366 "access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow>

367 root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"

369 chmod:

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

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

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

373 (Some (file \<lparr>attributes := attributes file \<lparr>others := perms\<rparr>\<rparr>)) root"

375 creat:

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

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

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

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

380 (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"

381 unlink:

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

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

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

385 root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"

387 mkdir:

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

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

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

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

392 (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"

393 rmdir:

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

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

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

397 root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"

399 readdir:

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

401 names = dom dir \<Longrightarrow>

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

404 text {*

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

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

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

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

409 ``reality-check'' of a formal model is the well-known problem of

410 \emph{validation}.

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

413 informal specifications given the corresponding Unix man pages, or

414 even peek at an actual implementation such as

415 \cite{Torvalds-et-al:Linux}. Another common way to gain confidence

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

417 \secref{sec:unix-examples}), and check the results with that of

418 experiments performed on a real Unix system.

419 *}

422 subsection {* Basic properties of single transitions \label{sec:unix-single-trans} *}

424 text {*

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

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

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

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

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

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

431 relation.

432 *}

434 theorem transition_uniq:

435 assumes root': "root \<midarrow>x\<rightarrow> root'"

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

437 shows "root' = root''"

438 using root''

439 proof cases

440 case read

441 with root' show ?thesis by cases auto

442 next

443 case write

444 with root' show ?thesis by cases auto

445 next

446 case chmod

447 with root' show ?thesis by cases auto

448 next

449 case creat

450 with root' show ?thesis by cases auto

451 next

452 case unlink

453 with root' show ?thesis by cases auto

454 next

455 case mkdir

456 with root' show ?thesis by cases auto

457 next

458 case rmdir

459 with root' show ?thesis by cases auto

460 next

461 case readdir

462 with root' show ?thesis by cases fastsimp+

463 qed

465 text {*

466 \medskip Apparently, file-system transitions are \emph{type-safe} in

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

468 again a directory.

469 *}

471 theorem transition_type_safe:

472 assumes tr: "root \<midarrow>x\<rightarrow> root'"

473 and inv: "\<exists>att dir. root = Env att dir"

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

475 proof (cases "path_of x")

476 case Nil

477 with tr inv show ?thesis

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

479 next

480 case Cons

481 from tr obtain opt where

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

483 by cases auto

484 with inv Cons show ?thesis

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

486 qed

488 text {*

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

490 file-system state that is enforced by any proper kernel

491 implementation. So user processes --- being bound to the

492 system-call interface --- may never mess up a file-system such that

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

494 a strange situation indeed.

495 *}

498 subsection {* Iterated transitions *}

500 text {*

501 Iterated system transitions via finite sequences of system

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

503 relation describes the cumulative effect of the sequence of

504 system-calls issued by a number of running processes over a finite

505 amount of time.

506 *}

508 consts

509 transitions :: "(file \<times> operation list \<times> file) set"

511 abbreviation

512 transitions_rel ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)

513 "root =xs\<Rightarrow> root' \<equiv> (root, xs, root') \<in> transitions"

515 inductive transitions

516 intros

517 nil: "root =[]\<Rightarrow> root"

518 cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''"

520 text {*

521 \medskip We establish a few basic facts relating iterated

522 transitions with single ones, according to the recursive structure

523 of lists.

524 *}

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

527 proof

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

529 then show "root = root'" by cases simp_all

530 next

531 assume "root = root'"

532 then show "root =[]\<Rightarrow> root'" by (simp only: transitions.nil)

533 qed

535 lemma transitions_cons_eq:

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

537 proof

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

539 then show "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"

540 by cases auto

541 next

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

543 then show "root =(x # xs)\<Rightarrow> root''"

544 by (blast intro: transitions.cons)

545 qed

547 text {*

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

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

550 uniqueness property of the basic transition system (see

551 \secref{sec:unix-single-trans}).

552 *}

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

555 by (simp add: transitions_nil_eq)

557 lemma transitions_consD:

558 assumes list: "root =(x # xs)\<Rightarrow> root''"

559 and hd: "root \<midarrow>x\<rightarrow> root'"

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

561 proof -

562 from list obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''"

563 by cases simp_all

564 from r' hd have "r' = root'" by (rule transition_uniq)

565 with root'' show "root' =xs\<Rightarrow> root''" by simp

566 qed

568 text {*

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

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

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

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

573 *}

575 lemma transitions_invariant:

576 assumes r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"

577 and trans: "root =xs\<Rightarrow> root'"

578 shows "Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"

579 using trans

580 proof induct

581 case nil

582 show ?case by assumption

583 next

584 case (cons root root' root'' x xs)

585 note P = `\<forall>x \<in> set (x # xs). P x`

586 then have "P x" by simp

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

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

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

590 qed

592 text {*

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

594 type-safety property (see \secref{sec:unix-single-trans}) from

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

596 result indeed.

597 *}

599 theorem transitions_type_safe:

600 assumes "root =xs\<Rightarrow> root'"

601 and "\<exists>att dir. root = Env att dir"

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

603 using transition_type_safe and prems

604 proof (rule transitions_invariant)

605 show "\<forall>x \<in> set xs. True" by blast

606 qed

609 section {* Executable sequences *}

611 text {*

612 An inductively defined relation such as the one of @{text "root \<midarrow>x\<rightarrow>

613 root'"} (see \secref{sec:unix-syscall}) has two main aspects. First

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

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

616 there is an explicit least-fixed-point construction involved, which

617 results in induction (and case-analysis) rules to eliminate known

618 transitions in an exhaustive manner.

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

621 experimental style, mainly using the introduction rules with basic

622 algebraic properties of the underlying structures. The technique

623 closely resembles that of Prolog combined with functional evaluation

624 in a very simple manner.

626 Just as the ``closed-world assumption'' is left implicit in Prolog,

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

628 So this is still purely positive reasoning about possible

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

630 \secref{sec:unix-bogosity}), when we shall demonstrate that certain

631 behavior is \emph{not} possible.

632 *}

635 subsection {* Possible transitions *}

637 text {*

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

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

640 transition.

641 *}

643 definition

644 "can_exec root xs \<equiv> \<exists>root'. root =xs\<Rightarrow> root'"

646 lemma can_exec_nil: "can_exec root []"

647 unfolding can_exec_def by (blast intro: transitions.intros)

649 lemma can_exec_cons:

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

651 unfolding can_exec_def by (blast intro: transitions.intros)

653 text {*

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

655 executed we may destruct it backwardly into individual transitions.

656 *}

658 lemma can_exec_snocD: "can_exec root (xs @ [y])

659 \<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''"

660 proof (induct xs fixing: root)

661 case Nil

662 then show ?case

663 by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)

664 next

665 case (Cons x xs)

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

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

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

669 by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)

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

671 unfolding can_exec_def by blast

672 from x xs have "root =(x # xs)\<Rightarrow> root'"

673 by (rule transitions.cons)

674 with y show ?case by blast

675 qed

678 subsection {* Example executions \label{sec:unix-examples} *}

680 text {*

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

682 model of Unix system-calls. The common technique is to alternate

683 introduction rules of the transition system (see

684 \secref{sec:unix-trans}), and steps to solve any emerging side

685 conditions using algebraic properties of the underlying file-system

686 structures (see \secref{sec:unix-file-system}).

687 *}

689 lemmas eval = access_def init_def

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

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

693 apply (rule can_exec_cons)

694 -- {* back-chain @{term can_exec} (of @{term [source] Cons}) *}

695 apply (rule mkdir)

696 -- {* back-chain @{term Mkdir} *}

697 apply (force simp add: eval)+

698 -- {* solve preconditions of @{term Mkdir} *}

699 apply (simp add: eval)

700 -- {* peek at resulting dir (optional) *}

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

702 apply (rule can_exec_nil)

703 -- {* back-chain @{term can_exec} (of @{term [source] Nil}) *}

704 done

706 text {*

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

708 may gain confidence that our specification of Unix system-calls

709 actually makes sense. Further common errors are usually exhibited

710 when preconditions of transition rules fail unexpectedly.

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

713 techniques as before.

714 *}

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

717 [Creat u perms [u, name],

718 Unlink u [u, name]]"

719 apply (rule can_exec_cons)

720 apply (rule creat)

721 apply (force simp add: eval)+

722 apply (simp add: eval)

723 apply (rule can_exec_cons)

724 apply (rule unlink)

725 apply (force simp add: eval)+

726 apply (simp add: eval)

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

728 apply (rule can_exec_nil)

729 done

731 theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow>

732 Readable \<in> perms\<^isub>2 \<Longrightarrow> name\<^isub>3 \<noteq> name\<^isub>4 \<Longrightarrow>

733 can_exec (init users)

734 [Mkdir u perms\<^isub>1 [u, name\<^isub>1],

735 Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2],

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

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

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

739 apply (rule can_exec_cons, rule transition.intros,

740 (force simp add: eval)+, (simp add: eval)?)+

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

742 apply (rule can_exec_nil)

743 done

745 theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow> Readable \<in> perms\<^isub>3 \<Longrightarrow>

746 can_exec (init users)

747 [Mkdir u perms\<^isub>1 [u, name\<^isub>1],

748 Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2],

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

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

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

752 apply (rule can_exec_cons, rule transition.intros,

753 (force simp add: eval)+, (simp add: eval)?)+

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

755 apply (rule can_exec_nil)

756 done

759 section {* Odd effects --- treated formally \label{sec:unix-bogosity} *}

761 text {*

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

763 slightly odd situation discussed in the introduction (see

764 \secref{sec:unix-intro}): the file-system can easily reach a state

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

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

767 uncouth manner.

768 *}

770 subsection {* The general procedure \label{sec:unix-inv-procedure} *}

772 text {*

773 The following theorem expresses the general procedure we are

774 following to achieve the main result.

775 *}

777 theorem general_procedure:

778 assumes cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False"

779 and init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root"

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

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

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

783 proof -

784 {

785 fix xs

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

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

788 then obtain root' root'' where

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

790 by (blast dest: can_exec_snocD)

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

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

793 by (rule transitions_invariant)

794 from this y have False by (rule cannot_y)

795 }

796 then show ?thesis by blast

797 qed

799 text {*

800 Here @{prop "P x"} refers to the restriction on file-system

801 operations that are admitted after having reached the critical

802 configuration; according to the problem specification this will

803 become @{prop "uid_of x = user\<^isub>1"} later on. Furthermore,

804 @{term y} refers to the operations we claim to be impossible to

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

806 @{term Q} is a suitable (auxiliary) invariant over the file-system;

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

808 work (see \secref{sec:unix-inv-lemmas}).

809 *}

812 subsection {* The particular situation *}

814 text {*

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

816 particular situation considered here. Thus we avoid excessive use

817 of local parameters in the subsequent development.

818 *}

820 locale situation =

821 fixes users :: "uid set"

822 and user\<^isub>1 :: uid

823 and user\<^isub>2 :: uid

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

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

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

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

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

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

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

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

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

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

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

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

837 definition (in situation)

838 "bogus =

839 [Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1],

840 Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2],

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

842 "bogus_path = [user\<^isub>1, name\<^isub>1, name\<^isub>2]"

844 text {*

845 The @{term bogus} operations are the ones that lead into the uncouth

846 situation; @{term bogus_path} is the key position within the

847 file-system where things go awry.

848 *}

851 subsection {* Invariance lemmas \label{sec:unix-inv-lemmas} *}

853 text {*

854 The following invariant over the root file-system describes the

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

856 path} within the file-system is a non-empty directory that is

857 neither owned and nor writable by @{term user\<^isub>1}.

858 *}

860 definition (in situation)

861 "invariant root path \<equiv>

862 (\<exists>att dir.

863 access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>

864 user\<^isub>1 \<noteq> owner att \<and>

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

867 text {*

868 Following the general procedure (see

869 \secref{sec:unix-inv-procedure}) we will now establish the three key

870 lemmas required to yield the final result.

872 \begin{enumerate}

874 \item The invariant is sufficiently strong to entail the

875 pathological case that @{term user\<^isub>1} is unable to remove the

876 (owned) directory at @{term "[user\<^isub>1, name\<^isub>1]"}.

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

879 bogus} list of operations (starting with an initial file-system

880 configuration).

882 \item The invariant is preserved by any file-system operation

883 performed by @{term user\<^isub>1} alone, without any help by other

884 users.

886 \end{enumerate}

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

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

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

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

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

893 proof become cluttered by confusing detail.

895 \medskip The first two lemmas are technically straight forward ---

896 we just have to inspect rather special cases.

897 *}

899 lemma (in situation) cannot_rmdir:

900 assumes inv: "invariant root bogus_path"

901 and rmdir: "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"

902 shows False

903 proof -

904 from inv obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"

905 unfolding invariant_def by blast

906 moreover

907 from rmdir obtain att where

908 "access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)"

909 by cases auto

910 then have "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"

911 by (simp only: access_empty_lookup lookup_append_some) simp

912 ultimately show False by (simp add: bogus_path_def)

913 qed

915 lemma (in situation)

916 assumes init: "init users =bogus\<Rightarrow> root"

917 notes eval = facts access_def init_def

918 shows init_invariant: "invariant root bogus_path"

919 using init

920 apply (unfold bogus_def bogus_path_def)

921 apply (drule transitions_consD, rule transition.intros,

922 (force simp add: eval)+, (simp add: eval)?)+

923 -- "evaluate all operations"

924 apply (drule transitions_nilD)

925 -- "reach final result"

926 apply (simp add: invariant_def eval)

927 -- "check the invariant"

928 done

930 text {*

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

932 ``bogosity'' invariant is preserved by any file-system operation

933 performed by @{term user\<^isub>1} alone. Note that this holds for

934 any @{term path} given, the particular @{term bogus_path} is not

935 required here.

936 *}

938 lemma (in situation) preserve_invariant:

939 assumes tr: "root \<midarrow>x\<rightarrow> root'"

940 and inv: "invariant root path"

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

942 shows "invariant root' path"

943 proof -

944 from inv obtain att dir where

945 inv1: "access root path user\<^isub>1 {} = Some (Env att dir)" and

946 inv2: "dir \<noteq> empty" and

947 inv3: "user\<^isub>1 \<noteq> owner att" and

948 inv4: "access root path user\<^isub>1 {Writable} = None"

949 by (auto simp add: invariant_def)

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

952 by (simp only: access_empty_lookup)

954 from inv1 inv3 inv4 and user\<^isub>1_not_root

955 have not_writable: "Writable \<notin> others att"

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

958 show ?thesis

959 proof cases

960 assume "root' = root"

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

962 next

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

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

965 by cases auto

966 show ?thesis

967 proof (rule prefix_cases)

968 assume "path_of x \<parallel> path"

969 with inv root'

970 have "\<And>perms. access root' path user\<^isub>1 perms = access root path user\<^isub>1 perms"

971 by (simp only: access_update_other)

972 with inv show "invariant root' path"

973 by (simp only: invariant_def)

974 next

975 assume "path_of x \<le> path"

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

978 show ?thesis

979 proof (cases ys)

980 assume "ys = []"

981 with tr uid inv2 inv3 lookup changed path and user\<^isub>1_not_root

982 have False

983 by cases (auto simp add: access_empty_lookup dest: access_some_lookup)

984 then show ?thesis ..

985 next

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

987 have "lookup root' path = lookup root path"

988 proof -

989 from inv2 lookup path ys

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

991 by (simp only:)

992 then obtain att' dir' file' where

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

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

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

996 by (blast dest: lookup_some_upper)

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

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

1000 by cases (auto simp add: access_empty_lookup lookup_update_some

1001 dest: access_some_lookup)

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

1003 Some (Env att dir)"

1004 by (simp add: lookup_append_some)

1005 with look path ys show ?thesis

1006 by simp

1007 qed

1008 with inv show "invariant root' path"

1009 by (simp only: invariant_def access_def)

1010 qed

1011 next

1012 assume "path < path_of x"

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

1015 obtain dir' where

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

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

1018 proof (cases ys)

1019 assume "ys = []"

1020 with path have parent: "path_of x = path @ [y]" by simp

1021 with tr uid inv4 changed obtain "file" where

1022 "root' = update (path_of x) (Some file) root"

1023 by cases auto

1024 with lookup parent have "lookup root' path = Some (Env att (dir(y\<mapsto>file)))"

1025 by (simp only: update_append_some update_cons_nil_env)

1026 moreover have "dir(y\<mapsto>file) \<noteq> empty" by simp

1027 ultimately show ?thesis ..

1028 next

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

1030 with lookup root' path

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

1032 by (simp only: update_append_some)

1033 also obtain file' where

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

1035 proof -

1036 have "dir y \<noteq> None"

1037 proof -

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

1039 by (simp split: option.splits)

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

1041 by (simp only: lookup_append_some)

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

1043 proof -

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

1045 by (cases ys rule: rev_cases) fastsimp+

1046 with tr path

1047 have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>

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

1049 by cases (auto dest: access_some_lookup)

1050 then show ?thesis

1051 by (simp, blast dest!: lookup_some_append)

1052 qed

1053 finally show ?thesis .

1054 qed

1055 with ys show ?thesis

1056 by (insert that, auto simp add: update_cons_cons_env)

1057 qed

1058 also have "dir(y\<mapsto>file') \<noteq> empty" by simp

1059 ultimately show ?thesis ..

1060 qed

1062 from lookup' have inv1': "access root' path user\<^isub>1 {} = Some (Env att dir')"

1063 by (simp only: access_empty_lookup)

1065 from inv3 lookup' and not_writable user\<^isub>1_not_root

1066 have "access root' path user\<^isub>1 {Writable} = None"

1067 by (simp add: access_def)

1068 with inv1' inv2' inv3 show ?thesis unfolding invariant_def by blast

1069 qed

1070 qed

1071 qed

1074 subsection {* Putting it all together \label{sec:unix-main-result} *}

1076 text {*

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

1078 invariance lemmas (see \secref{sec:unix-inv-lemmas}) according the the

1079 overall procedure (see \secref{sec:unix-inv-procedure}).

1080 *}

1082 corollary (in situation)

1083 assumes bogus: "init users =bogus\<Rightarrow> root"

1084 shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^isub>1) \<and>

1085 can_exec root (xs @ [Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1]]))"

1086 proof -

1087 from cannot_rmdir init_invariant preserve_invariant

1088 and bogus show ?thesis by (rule general_procedure)

1089 qed

1091 end