65 |
65 |
66 notation (Axiom output) |
66 notation (Axiom output) |
67 "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") |
67 "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") |
68 |
68 |
69 notation (IfThen output) |
69 notation (IfThen output) |
70 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
70 "Pure.imp" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
71 syntax (IfThen output) |
71 syntax (IfThen output) |
72 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
72 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
73 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
73 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
74 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
74 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
75 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
75 "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>") |
76 |
76 |
77 notation (IfThenNoBox output) |
77 notation (IfThenNoBox output) |
78 "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
78 "Pure.imp" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
79 syntax (IfThenNoBox output) |
79 syntax (IfThenNoBox output) |
80 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
80 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
81 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
81 ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") |
82 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
82 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") |
83 "_asm" :: "prop \<Rightarrow> asms" ("_") |
83 "_asm" :: "prop \<Rightarrow> asms" ("_") |
314 It installs a reference monitor to restrict access to system resources. |
314 It installs a reference monitor to restrict access to system resources. |
315 They model a dynamic semantics of the operating system with four rules dealing with |
315 They model a dynamic semantics of the operating system with four rules dealing with |
316 executing a file, setting a role and setting an UID as well as GID. |
316 executing a file, setting a role and setting an UID as well as GID. |
317 These rules are parametrerised by an arbitrary but fixed access policy. |
317 These rules are parametrerised by an arbitrary but fixed access policy. |
318 Although, there are only four rules, their state-space is in general |
318 Although, there are only four rules, their state-space is in general |
319 infinite, like in our work. They therfore give an abstracted semantics, |
319 infinite, like in our work. They therefore give an abstracted semantics, |
320 which gives them a finite state-space. For example the abstracted |
320 which gives them a finite state-space. For example the abstracted |
321 semantics dispenses with users and roles by introducing |
321 semantics dispenses with users and roles by introducing |
322 abstract users and abstract roles. They obtain a soundness result |
322 abstract users and abstract roles. They obtain a soundness result |
323 for their abstract semantics and under some weak assumptions |
323 for their abstract semantics and under some weak assumptions |
324 also a completeness result. Comparing this to our work, we will have a much |
324 also a completeness result. Comparing this to our work, we will have a much |