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

src/HOL/Unix/Unix.thy

author | huffman |

Thu Aug 11 09:11:15 2011 -0700 (2011-08-11) | |

changeset 44165 | d26a45f3c835 |

parent 43433 | f67364f35789 |

child 44236 | b73b7832b384 |

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

remove lemma stupid_ext

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

2 Author: Markus Wenzel, TU Muenchen

3 *)

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

7 theory Unix

8 imports

9 Main

10 "~~/src/HOL/Library/Nested_Environment"

11 "~~/src/HOL/Library/List_Prefix"

12 begin

14 text {*

15 We give a simple mathematical model of the basic structures

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

37 symbolic links, and mount points.

38 *}

41 subsection {* Names *}

43 text {*

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

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

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

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

48 *}

50 type_synonym uid = nat

51 type_synonym name = nat

52 type_synonym path = "name list"

55 subsection {* Attributes *}

57 text {*

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

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

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

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

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

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

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

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

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

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

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

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

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

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

73 user group structures and related issues is given in

74 \cite{Naraschewski:2001}.}

75 *}

77 datatype perm =

78 Readable

79 | Writable

80 | Executable -- "(ignored)"

82 type_synonym perms = "perm set"

84 record att =

85 owner :: uid

86 others :: perms

88 text {*

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

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

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

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

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

94 sub-directories).

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

97 permission altogether. In reality it would indicate executable

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

99 of directory entries (recall that mere directory browsing is

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

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

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

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

104 give @{term Executable} permission to anybody.

105 *}

108 subsection {* Files *}

110 text {*

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

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

113 from the standard library of Isabelle/HOL

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

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

117 \medskip

118 {\def\isastyleminor{\isastyle}

119 \begin{tabular}{l}

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

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

122 \end{tabular}}

123 \medskip

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

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

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

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

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

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

131 of directory nodes).

132 *}

134 type_synonym "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 definition

170 "map_attributes f file =

171 (case file of

172 Val (att, text) \<Rightarrow> Val (f att, text)

173 | Env att dir \<Rightarrow> Env (f att) dir)"

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

176 by (simp add: attributes_def)

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

179 by (simp add: attributes_def)

181 lemma [simp]: "attributes (map_attributes f file) = f (attributes file)"

182 by (cases "file") (simp_all add: attributes_def map_attributes_def

183 split_tupled_all)

185 lemma [simp]: "map_attributes f (Val (att, text)) = Val (f att, text)"

186 by (simp add: map_attributes_def)

188 lemma [simp]: "map_attributes f (Env att dir) = Env (f att) dir"

189 by (simp add: map_attributes_def)

192 subsection {* Initial file-systems *}

194 text {*

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

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

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

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

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

200 has user id 0).

201 *}

203 definition

204 "init users =

205 Env \<lparr>owner = 0, others = {Readable}\<rparr>

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

207 else None)"

210 subsection {* Accessing file-systems *}

212 text {*

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

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

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

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

217 permissions recorded within the file-system.

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

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

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

222 *}

224 definition

225 "access root path uid perms =

226 (case lookup root path of

227 None \<Rightarrow> None

228 | Some file \<Rightarrow>

229 if uid = 0

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

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

232 then Some file

233 else None)"

235 text {*

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

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

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

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

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

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

243 attributes. Subsequently we establish a few auxiliary facts that

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

245 *}

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

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

250 lemma access_some_lookup:

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

252 lookup root path = Some file"

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

255 lemma access_update_other:

256 assumes parallel: "path' \<parallel> path"

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

258 proof -

259 from parallel obtain y z xs ys zs where

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

261 by (blast dest: parallel_decomp)

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

263 by (blast intro: lookup_update_other)

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

265 qed

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

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

272 text {*

273 According to established operating system design (cf.\

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

275 operations by a fixed set of \emph{system-calls}. This enables the

276 kernel to enforce certain security policies in the first

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

278 by any ``LCF-style'' theorem proving system according to Milner's

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

280 itself.}

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

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

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

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

286 *}

288 datatype operation =

289 Read uid string path

290 | Write uid string path

291 | Chmod uid perms path

292 | Creat uid perms path

293 | Unlink uid path

294 | Mkdir uid perms path

295 | Rmdir uid path

296 | Readdir uid "name set" path

298 text {*

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

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

301 model never mentions processes explicitly. The other parameters are

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

303 to all kinds of system-calls.

304 *}

306 primrec

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

308 where

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

310 | "uid_of (Write uid text path) = uid"

311 | "uid_of (Chmod uid perms path) = uid"

312 | "uid_of (Creat uid perms path) = uid"

313 | "uid_of (Unlink uid path) = uid"

314 | "uid_of (Mkdir uid path perms) = uid"

315 | "uid_of (Rmdir uid path) = uid"

316 | "uid_of (Readdir uid names path) = uid"

318 primrec

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

320 where

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

322 | "path_of (Write uid text path) = path"

323 | "path_of (Chmod uid perms path) = path"

324 | "path_of (Creat uid perms path) = path"

325 | "path_of (Unlink uid path) = path"

326 | "path_of (Mkdir uid perms path) = path"

327 | "path_of (Rmdir uid path) = path"

328 | "path_of (Readdir uid names path) = path"

330 text {*

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

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

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

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

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

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

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

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

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

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

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

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

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

345 case.

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

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

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

350 involved here).

351 *}

353 inductive

354 transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"

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

356 where

358 read:

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

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

361 "write":

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

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

365 chmod:

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

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

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

369 (Some (map_attributes (others_update (\<lambda>_. perms)) file)) root" |

371 creat:

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

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

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

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

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

377 unlink:

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

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

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

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

383 mkdir:

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

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

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

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

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

389 rmdir:

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

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

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

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

395 readdir:

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

397 names = dom dir \<Longrightarrow>

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

400 text {*

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

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

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

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

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

406 \emph{validation}.

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

409 informal specifications given the corresponding Unix man pages, or

410 even peek at an actual implementation such as

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

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

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

414 experiments performed on a real Unix system.

415 *}

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

420 text {*

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

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

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

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

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

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

427 relation.

428 *}

430 theorem transition_uniq:

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

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

433 shows "root' = root''"

434 using root''

435 proof cases

436 case read

437 with root' show ?thesis by cases auto

438 next

439 case "write"

440 with root' show ?thesis by cases auto

441 next

442 case chmod

443 with root' show ?thesis by cases auto

444 next

445 case creat

446 with root' show ?thesis by cases auto

447 next

448 case unlink

449 with root' show ?thesis by cases auto

450 next

451 case mkdir

452 with root' show ?thesis by cases auto

453 next

454 case rmdir

455 with root' show ?thesis by cases auto

456 next

457 case readdir

458 with root' show ?thesis by cases fastsimp+

459 qed

461 text {*

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

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

464 again a directory.

465 *}

467 theorem transition_type_safe:

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

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

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

471 proof (cases "path_of x")

472 case Nil

473 with tr inv show ?thesis

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

475 next

476 case Cons

477 from tr obtain opt where

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

479 by cases auto

480 with inv Cons show ?thesis

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

482 qed

484 text {*

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

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

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

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

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

490 a strange situation indeed.

491 *}

494 subsection {* Iterated transitions *}

496 text {*

497 Iterated system transitions via finite sequences of system

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

499 relation describes the cumulative effect of the sequence of

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

501 amount of time.

502 *}

504 inductive

505 transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"

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

507 where

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

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

511 text {*

512 \medskip We establish a few basic facts relating iterated

513 transitions with single ones, according to the recursive structure

514 of lists.

515 *}

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

518 proof

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

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

521 next

522 assume "root = root'"

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

524 qed

526 lemma transitions_cons_eq:

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

528 proof

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

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

531 by cases auto

532 next

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

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

535 by (blast intro: transitions.cons)

536 qed

538 text {*

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

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

541 uniqueness property of the basic transition system (see

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

543 *}

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

546 by (simp add: transitions_nil_eq)

548 lemma transitions_consD:

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

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

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

552 proof -

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

554 by cases simp_all

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

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

557 qed

559 text {*

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

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

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

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

564 *}

566 lemma transitions_invariant:

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

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

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

570 using trans

571 proof induct

572 case nil

573 show ?case by (rule nil.prems)

574 next

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

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

577 then have "P x" by simp

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

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

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

581 qed

583 text {*

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

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

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

587 result indeed.

588 *}

590 theorem transitions_type_safe:

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

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

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

594 using transition_type_safe and assms

595 proof (rule transitions_invariant)

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

597 qed

600 section {* Executable sequences *}

602 text {*

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

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

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

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

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

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

609 transitions in an exhaustive manner.

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

612 experimental style, mainly using the introduction rules with basic

613 algebraic properties of the underlying structures. The technique

614 closely resembles that of Prolog combined with functional evaluation

615 in a very simple manner.

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

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

619 So this is still purely positive reasoning about possible

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

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

622 behavior is \emph{not} possible.

623 *}

626 subsection {* Possible transitions *}

628 text {*

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

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

631 transition.

632 *}

634 definition

635 "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')"

637 lemma can_exec_nil: "can_exec root []"

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

640 lemma can_exec_cons:

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

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

644 text {*

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

646 executed we may destruct it backwardly into individual transitions.

647 *}

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

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

651 proof (induct xs arbitrary: root)

652 case Nil

653 then show ?case

654 by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)

655 next

656 case (Cons x xs)

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

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

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

660 by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)

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

662 unfolding can_exec_def by blast

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

664 by (rule transitions.cons)

665 with y show ?case by blast

666 qed

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

671 text {*

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

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

674 introduction rules of the transition system (see

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

676 conditions using algebraic properties of the underlying file-system

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

678 *}

680 lemmas eval = access_def init_def

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

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

684 apply (rule can_exec_cons)

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

686 apply (rule mkdir)

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

688 apply (force simp add: eval)+

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

690 apply (simp add: eval)

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

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

693 apply (rule can_exec_nil)

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

695 done

697 text {*

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

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

700 actually makes sense. Further common errors are usually exhibited

701 when preconditions of transition rules fail unexpectedly.

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

704 techniques as before.

705 *}

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

708 [Creat u perms [u, name],

709 Unlink u [u, name]]"

710 apply (rule can_exec_cons)

711 apply (rule creat)

712 apply (force simp add: eval)+

713 apply (simp add: eval)

714 apply (rule can_exec_cons)

715 apply (rule unlink)

716 apply (force simp add: eval)+

717 apply (simp add: eval)

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

719 apply (rule can_exec_nil)

720 done

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

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

724 can_exec (init users)

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

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

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

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

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

730 apply (rule can_exec_cons, rule transition.intros,

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

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

733 apply (rule can_exec_nil)

734 done

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

737 can_exec (init users)

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

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

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

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

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

743 apply (rule can_exec_cons, rule transition.intros,

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

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

746 apply (rule can_exec_nil)

747 done

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

752 text {*

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

754 slightly odd situation discussed in the introduction (see

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

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

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

758 uncouth manner.

759 *}

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

763 text {*

764 The following theorem expresses the general procedure we are

765 following to achieve the main result.

766 *}

768 theorem general_procedure:

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

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

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

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

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

774 proof -

775 {

776 fix xs

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

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

779 then obtain root' root'' where

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

781 by (blast dest: can_exec_snocD)

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

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

784 by (rule transitions_invariant)

785 from this y have False by (rule cannot_y)

786 }

787 then show ?thesis by blast

788 qed

790 text {*

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

792 operations that are admitted after having reached the critical

793 configuration; according to the problem specification this will

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

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

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

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

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

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

800 *}

803 subsection {* The particular situation *}

805 text {*

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

807 particular situation considered here. Thus we avoid excessive use

808 of local parameters in the subsequent development.

809 *}

811 locale situation =

812 fixes users :: "uid set"

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

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

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

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

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

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

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

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

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

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

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

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

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

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

827 begin

829 definition

830 "bogus =

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

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

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

834 definition

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

837 text {*

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

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

840 file-system where things go awry.

841 *}

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

846 text {*

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

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

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

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

851 *}

853 definition

854 "invariant root path =

855 (\<exists>att dir.

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

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

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

860 text {*

861 Following the general procedure (see

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

863 lemmas required to yield the final result.

865 \begin{enumerate}

867 \item The invariant is sufficiently strong to entail the

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

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

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

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

873 configuration).

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

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

877 users.

879 \end{enumerate}

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

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

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

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

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

886 proof become cluttered by confusing detail.

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

889 we just have to inspect rather special cases.

890 *}

892 lemma cannot_rmdir:

893 assumes inv: "invariant root bogus_path"

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

895 shows False

896 proof -

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

898 unfolding invariant_def by blast

899 moreover

900 from rmdir obtain att where

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

902 by cases auto

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

904 by (simp only: access_empty_lookup lookup_append_some) simp

905 ultimately show False by (simp add: bogus_path_def)

906 qed

908 lemma

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

910 notes eval = facts access_def init_def

911 shows init_invariant: "invariant root bogus_path"

912 using init

913 apply (unfold bogus_def bogus_path_def)

914 apply (drule transitions_consD, rule transition.intros,

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

916 -- "evaluate all operations"

917 apply (drule transitions_nilD)

918 -- "reach final result"

919 apply (simp add: invariant_def eval)

920 -- "check the invariant"

921 done

923 text {*

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

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

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

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

928 required here.

929 *}

931 lemma preserve_invariant:

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

933 and inv: "invariant root path"

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

935 shows "invariant root' path"

936 proof -

937 from inv obtain att dir where

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

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

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

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

942 by (auto simp add: invariant_def)

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

945 by (simp only: access_empty_lookup)

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

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

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

951 show ?thesis

952 proof cases

953 assume "root' = root"

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

955 next

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

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

958 by cases auto

959 show ?thesis

960 proof (rule prefix_cases)

961 assume "path_of x \<parallel> path"

962 with inv root'

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

964 by (simp only: access_update_other)

965 with inv show "invariant root' path"

966 by (simp only: invariant_def)

967 next

968 assume "path_of x \<le> path"

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

971 show ?thesis

972 proof (cases ys)

973 assume "ys = []"

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

975 have False

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

977 then show ?thesis ..

978 next

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

980 have "lookup root' path = lookup root path"

981 proof -

982 from inv2 lookup path ys

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

984 by (simp only:)

985 then obtain att' dir' file' where

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

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

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

989 by (blast dest: lookup_some_upper)

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

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

993 by cases (auto simp add: access_empty_lookup lookup_update_some

994 dest: access_some_lookup)

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

996 Some (Env att dir)"

997 by (simp add: lookup_append_some)

998 with look path ys show ?thesis

999 by simp

1000 qed

1001 with inv show "invariant root' path"

1002 by (simp only: invariant_def access_def)

1003 qed

1004 next

1005 assume "path < path_of x"

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

1008 obtain dir' where

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

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

1011 proof (cases ys)

1012 assume "ys = []"

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

1014 with tr uid inv4 changed obtain "file" where

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

1016 by cases auto

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

1018 by (simp only: update_append_some update_cons_nil_env)

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

1020 ultimately show ?thesis ..

1021 next

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

1023 with lookup root' path

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

1025 by (simp only: update_append_some)

1026 also obtain file' where

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

1028 proof -

1029 have "dir y \<noteq> None"

1030 proof -

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

1032 by (simp split: option.splits)

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

1034 by (simp only: lookup_append_some)

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

1036 proof -

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

1038 by (cases ys rule: rev_cases) fastsimp+

1039 with tr path

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

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

1042 by cases (auto dest: access_some_lookup)

1043 then show ?thesis

1044 by (simp, blast dest!: lookup_some_append)

1045 qed

1046 finally show ?thesis .

1047 qed

1048 with ys show ?thesis using that by auto

1049 qed

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

1051 ultimately show ?thesis ..

1052 qed

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

1055 by (simp only: access_empty_lookup)

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

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

1059 by (simp add: access_def)

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

1061 qed

1062 qed

1063 qed

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

1068 text {*

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

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

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

1072 *}

1074 corollary

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

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

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

1078 proof -

1079 from cannot_rmdir init_invariant preserve_invariant

1080 and bogus show ?thesis by (rule general_procedure)

1081 qed

1083 end

1085 end