diff options
Diffstat (limited to 'books/workshops/2003/greve-wilding-vanfleet/support')
12 files changed, 786 insertions, 0 deletions
diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/.gitignore b/books/workshops/2003/greve-wilding-vanfleet/support/.gitignore new file mode 100644 index 0000000..3a06756 --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/.gitignore @@ -0,0 +1,3 @@ +make.lisp +consistency-test.lisp +consistency-test-passed.lisp diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/Makefile b/books/workshops/2003/greve-wilding-vanfleet/support/Makefile new file mode 100644 index 0000000..3be5d36 --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/Makefile @@ -0,0 +1,45 @@ +include ../../../../Makefile-generic +BOOKS = firewallworks + +# Avoid provisional certification since we are not using Makefile-deps, +# which is because there is a generated .lisp file. +override ACL2_PCERT = + +separation.cert: separation.lisp + +firewallspec.cert: separation.cert firewallspec.lisp + +consistency-test.lisp: separation.lisp firewallspec.lisp firewallworks.lisp make-consistency-test.lisp + rm -f make.lisp + rm -f consistency-test.lisp + echo "(value :q)" > make.lisp + echo "(load \"make-consistency-test.lisp\")" >> make.lisp + echo "(make-test \"consistency-test.lisp\")" >> make.lisp +# Deleted by Matt K., May 2006, to avoid STATE warning in CMUCL. +# echo '(acl2::value :q)' >> make.lisp + echo '(acl2::exit-lisp)' >> make.lisp + $(ACL2) < make.lisp > consistency.out + +## This book will be certified if the axioms are proved consistent +consistency-test-passed.cert: consistency-test.lisp + rm -f make.lisp + rm -f consistency-test-passed.lisp + rm -f consistency-test-passed.cert + echo "(in-package \"ACL2\")" >> consistency-test-passed.lisp + echo "(value :q) (lp)" > make.lisp + echo "(ld \"consistency-test.lisp\" :ld-error-triples t :ld-error-action :error)" >> make.lisp + echo '(acl2::value :q)' >> make.lisp + echo '(acl2::exit-lisp)' >> make.lisp + $(ACL2) < make.lisp > consistency-test-passed.out + +## This book will be certified if the axioms are proved consistent +compatible.cert: compatible.lisp separation.cert + +## Note: this will fail if the consistency-check is not passed, or the compatibility +## test did not work +firewallworks.cert: firewallspec.cert firewallworks.lisp consistency-test-passed.cert compatible.cert + +newclean: + rm -f consistency-test.lisp make.lisp consistency-test-passed.lisp + +clean: newclean diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/cert_pl_exclude b/books/workshops/2003/greve-wilding-vanfleet/support/cert_pl_exclude new file mode 100644 index 0000000..833501d --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/cert_pl_exclude @@ -0,0 +1,2 @@ +This directory has a custom Makefile, so it is excluded from +certification based on cert.pl. diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/compatible.acl2 b/books/workshops/2003/greve-wilding-vanfleet/support/compatible.acl2 new file mode 100644 index 0000000..178d743 --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/compatible.acl2 @@ -0,0 +1,4 @@ +(value :q) +(lp) +(include-book "separation") +(certify-book "compatible" ? t) diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/compatible.lisp b/books/workshops/2003/greve-wilding-vanfleet/support/compatible.lisp new file mode 100644 index 0000000..6217937 --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/compatible.lisp @@ -0,0 +1,87 @@ +(in-package "ACL2") + +;; This file demonstrates that our notion of separation implies the +;; "standard" notion presented to us by Vanfleet and derived from +;; previous work. These separation notions are: infiltration, +;; exfiltration, and mediation. +;; +;; Matt July 2002 + +;; Requires: +;; (include-book "separation") + +(defthm subsetp-intersection-equal + (and + (subsetp (intersection-equal a b) a) + (subsetp (intersection-equal a b) b))) + +(defthm member-selectlist-means + (implies + (and + (equal (selectlist l l1) (selectlist l l2)) + (member x l)) + (iff (equal (select x l1) (select x l2)) t)) + :rule-classes :forward-chaining) + +(defthm selectlist-subset + (implies + (and + (equal (selectlist y l1) (selectlist y l2)) + (subsetp x y)) + (iff (equal (selectlist x l1) (selectlist x l2)) t))) + +(defthm infiltration + (implies + (and + (equal (current st1) (current st2)) + (equal (selectlist (segs (current st1)) st1) + (selectlist (segs (current st2)) st2)) + (member x (segs (current st1)))) + (equal (select x (next st1)) + (select x (next st2)))) + :hints (("goal" :use (:instance separation (seg x))))) + +;; Our initial version of exfiltration was quite strong: the segment +;; in question was unchanged assuming that the current partition had +;; no dia segments. This version using these functions would be +;; something like: + +;(defthm exfiltration +; (implies +; (not (intersection-equal (dia y) (segs (current st)))) +; (equal (select y (next st)) +; (select y st))) +; :hints (("goal" :use (:instance separation (seg y))))) + +;; Unfortunately, this formulation forecloses the possibility of +;; free-running counters, interrupt handlers, etc. that change the +;; state of y in a way not dependant on the current partition. This +;; kind of behavior ought to be allowed by this formalization, so we +;; weaken it somewhat. + +; Matt K., after v4-2: +; Commenting out the following rule, which rewrites a term to itself! +#|| +(defthm exfiltration + (implies + (and + (equal (current st1) (current st2)) + (not (intersection-equal (dia y) (segs (current st1))))) + (equal (select y (next st2)) + (select y (next st2)))) + :hints (("goal" :use (:instance separation (seg y))))) +||# + +(defthm mediation + (implies + (and + (equal (current st1) (current st2)) + (equal (selectlist (segs (current st1)) st1) + (selectlist (segs (current st2)) st2)) + (equal (select x st1) (select x st2))) + (equal (select x (next st1)) (select x (next st2)))) + :hints (("goal" :use (:instance separation (seg x))))) + + + + diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/firewallspec.acl2 b/books/workshops/2003/greve-wilding-vanfleet/support/firewallspec.acl2 new file mode 100644 index 0000000..e6aab8a --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/firewallspec.acl2 @@ -0,0 +1,4 @@ +(value :q) +(lp) +(include-book "separation") +(certify-book "firewallspec" ? t) diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/firewallspec.lisp b/books/workshops/2003/greve-wilding-vanfleet/support/firewallspec.lisp new file mode 100644 index 0000000..0dc35f0 --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/firewallspec.lisp @@ -0,0 +1,120 @@ +(in-package "ACL2") + +;; Essay on formalizing "black" data. + +;; This file introduces some concepts useful in specifying a firewall. +;; It was not immediately obvious how to formalize the correct +;; operation of a firewall. What makes it difficult is describing +;; what it means for data not to contain sensitive information. We +;; introduce the notion of "black", which is a predicate on a segment +;; name and a system state. The intended interpretation is that black +;; segments do not contain sensitive information that requires +;; protection. + +;; Mostly we leave "black" unspecified. However, we assume that it +;; has the following properties: + +;; 1. If all segments in a system are black, then after the system +;; progresses one step each segment is black. (No "spontaneous +;; generation".) + +;; 2. There exists a function "scrub" that modifies a segment so +;; that it is black. + +;; 3. Elements of system state that are not associated with the +;; segment are irrelevant in deciding whether a segment is black. + +;; Is this approach to modeling reasonable? Assume that each byte of +;; the system has associated with it a "black" bit that tells whether +;; the byte is cleared. Any operation that produces data sets the +;; result's black bit to the "and" of all the input black bits. + +;; Axiom one holds, since any operation will set black bits if every +;; segment in the system has its black bits set. Note that +;; applications are not modeled at this level, but it is worth +;; considering whether this framework could model something like a +;; decryption algorithm. Note that decryption requires keys or +;; algorithms that would not be considered "black" in this framework, +;; so this axiom would not be inconsistent with such models. + +;; Axiom two holds since one can "scrub" a data segment by zeroizing +;; all the data and setting the black bits. (Of course, not under +;; user control.) + +;; Axiom three holds since it is straightforward to tell if a segment +;; is black by checking all its black bits. + +(encapsulate +;; BLACK +;; input: segment name, machine state +;; output: boolean indicating whether segment is cleared + + (((black * *) => *) + +;; SCRUB +;; input: segment name, machine state +;; output machine state in which segment is cleared and other +;; segments are untouched + + ((scrub * *) => *) +) + +;; A "black" segment contains no sensitive information +(local (defun black (segname st) (declare (ignore segname) (ignore st)) t)) + +;; A list of segments is all black +(defun blacklist (segnames st) + (if (consp segnames) + (and + (black (car segnames) st) + (blacklist (cdr segnames) st)) + t)) + +;; A segment to be "scrubbed" +(local (defun scrub (seg st) (declare (ignore seg)) st)) + +;; A list of segments to be "scrubbed" +(defun scrublist (segs st) + (if (consp segs) + (scrublist (cdr segs) (scrub (car segs) st)) + st)) + +(defthm scrub-commutative + (equal + (scrub seg1 (scrub seg2 st)) + (scrub seg2 (scrub seg1 st)))) + +(defthm segment-scrub-different + (implies (not (equal seg1 seg2)) + (equal (select seg1 (scrub seg2 st)) + (select seg1 st)))) +(defthm black-scrub + (equal + (black seg1 (scrub seg2 st)) + (or + (equal seg1 seg2) + (black seg1 st)))) + +(defthm current-scrub + (equal + (current (scrub seg st)) + (current st))) + +;; If every segment is black, then after one step an arbitrary segment +;; is black +(defthm spontaneous-generation + (implies + (blacklist (segslist (allparts)) st) + (black seg (next st)))) + +;; Only the contents of a segment determine its blackness +(defthm black-function-of-segment + (implies + (equal (select x st1) (select x st2)) + (equal (black x st1) (black x st2))) + :rule-classes nil) + +) + + + diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/firewallworks.acl2 b/books/workshops/2003/greve-wilding-vanfleet/support/firewallworks.acl2 new file mode 100644 index 0000000..e977fb1 --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/firewallworks.acl2 @@ -0,0 +1,12 @@ +(in-package "ACL2") +(include-book "firewallspec") + +;; [Jared] BOZO wtf...? + +(include-book "consistency-test-passed" :uncertified-okp nil) +:u +(include-book "compatible" :uncertified-okp nil) +:u + +; cert-flags: ? t :defaxioms-okp t +(certify-book "firewallworks" ? t :defaxioms-okp t) diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/firewallworks.lisp b/books/workshops/2003/greve-wilding-vanfleet/support/firewallworks.lisp new file mode 100644 index 0000000..64c7279 --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/firewallworks.lisp @@ -0,0 +1,340 @@ +(in-package "ACL2") + +;; (include-book "firewallspec") + +;; Firewall works + +;; We formalize a particular firewall system and use the separation +;; axiom to show that it works. We use the notion of "black" data to +;; describe what is and what is not cleared. + +;; We introduce the firewall system using three axioms. + +;; Note about the axioms consistency +;; --------------------------------- +;; We would like to show that the axioms we've added here are +;; consistent with the axioms added using encapsulate. Although doing +;; this does not guarantee that we've axiomitized things properly, +;; since it's a check on our axioms we'd like to do it. +;; Unfortunately, there seems to be no way to accomplish this +;; conveniently using ACL2 2.6. + +;; So, we do it manually, using code written to work with a Makefile. +;; The makefile is arranged so that if these axioms are inconsistent +;; with the axioms added previously, then an error occurs. We use the +;; witnesses introduced by the encapsulate, which is not the most +;; robust way to do this since it requires foresight when introducing +;; the encapsulates and may limit their use. (Better to have a +;; mechanism that allows a new witness to be introduced when the +;; consistency check is being accomplished.) + +;; We would of course prefer ACL2 to support doing this, and we have +;; suggested this to the ACL2 authors and others. + +;; b, and f are partitions. Their names are meant to suggest "black" +;; and "firewall". +(defaxiom allparts-includes + (and + (member 'b (allparts)) + (member 'f (allparts)))) + +;; When the system is executing partition f, the contents of memory +;; segment "outbox" does not unblacken +(defaxiom firewall-blackens + (implies + (and + (equal (current st) 'f) + (black 'outbox st)) + (black 'outbox (next st)))) + +;; If there is a segment in partition B that is writable from a +;; segment in a non-B partition, then it is called "outbox" and it is +;; only writable from segments that are in partition F and not in +;; partition B. +(defaxiom dia-setup + (implies + (and + (member seg1 (dia seg2)) + (member seg2 (segs 'b)) + (member seg1 (segs p)) + (not (equal p 'b))) + (and + (equal seg2 'outbox) + (equal p 'f) + (not (member seg1 (segs 'b))))) + :rule-classes nil) + +;; Some of the recursive functions we have introduced were added in +;; the scope of an encapsulate. ACL2 will not allow us to use their +;; recursive structure in inductive proofs, because we might have done +;; something fishy. We now provide ACL2 some recursive functions to +;; guide its choice of induction schemes on a few of these functions. + +(defun scrublist-induct (segs st) + (if (consp segs) + (scrublist-induct (cdr segs) (scrub (car segs) st)) + st)) + +(defthm scrublist-induction-scheme + t + :rule-classes ((:induction :pattern (scrublist segs st) + :scheme (scrublist-induct segs st)))) + +(defthm blacklist-induction-scheme + t + :rule-classes ((:induction :pattern (blacklist segs st) + :scheme (len segs)))) + +(defun run-induct (st n) + (if (zp n) st (run-induct (next st) (1- n)))) + +(defthm run-induction-scheme + t + :rule-classes ((:induction :pattern (run st n) + :scheme (run-induct st n)))) + +;; We introduce some underlying useful theorems about our functions + +(defthm remains-black-after-scrublist + (implies + (black seg st) + (black seg (scrublist segs st)))) + +(defthm black-scrublist + (iff + (black x (scrublist list st)) + (or + (member x list) + (black x st)))) + +(defthm scrublist-scrub + (equal + (scrublist list (scrub x st)) + (scrub x (scrublist list st)))) + +(defthm blacklist-scrub + (implies + (blacklist x list) + (blacklist x (scrub y list)))) + +;; Scrubbing the non-black elements yields a system state with all +;; black elements +(defthm scrub-nonblack-means-black + (implies + (blacklist y st) + (blacklist x (scrublist (set-difference-equal x y) st)))) + +; [Removed by Matt K. to handle changes to member, assoc, etc. after ACL2 4.2.] +; (defthm member-equal-is-member +; (equal (member-equal a l) (member a l))) + +(defthm intersection-equal-dia-b-segs-f-helper + (implies + (and + (member x (segs 'b)) + (not (equal x 'outbox)) + (subsetp z (dia x))) + (equal (intersection-equal z (segs 'f)) nil)) + :hints + (("Subgoal *1/3'4'" :use (:instance dia-setup (seg1 z1) (seg2 x) (p 'f)))) + :rule-classes nil) + +(defthm subsetp-append + (subsetp x (append a x))) + +(defthm subsetp-x-x + (subsetp x x) + :hints (("goal" :use (:instance subsetp-append (a nil)) + :in-theory (disable subsetp-append)))) + +(defthm intersection-equal-dia-b-segs-f + (implies + (and + (member x (segs 'b)) + (not (equal x 'outbox))) + (equal (intersection-equal (dia x) (segs 'f)) nil)) + :hints (("goal" :use (:instance intersection-equal-dia-b-segs-f-helper + (z (dia x)))))) + +(defthm select-scrublist + (implies + (not (member a l)) + (equal (select a (scrublist l st)) + (select a st)))) + +(defthm current-scrublist + (equal + (current (scrublist segs st)) + (current st))) + +(defthm selectlist-scrublist + (implies + (equal (intersection-equal x y) nil) + (equal + (selectlist x (scrublist y st)) + (selectlist x st)))) + +(defthm member-set-difference-equal + (iff + (member e (set-difference-equal l1 l2)) + (and + (member e l1) + (not (member e l2))))) + +(defthm intersection-equal-set-difference + (equal + (intersection-equal + (intersection-equal a b) + (set-difference-equal c b)) + nil)) + +;; We will prove that the firewall works by casesplitting on which +;; partition is the current partition. For each of the cases we use +;; the separation axiom to posit a state that is "equivalent" to the +;; actual state with respect to an arbitrary memory segment of b. The +;; following rule helps that proof along by using a free variable +;; match of the equivalent state. + +(defthm black-from-equivalent-allblack + (implies + (and + (equal (select seg (next st)) (select seg (next st2))) + (blacklist (segslist (allparts)) st2)) + (black seg (next st))) + :hints (("goal" :use (:instance black-function-of-segment + (st1 (next st)) + (st2 (next st2)) + (x seg))))) + +;; Now, each of the cases. The current partition is either b, f, or +;; some other partition, and we prove a lemma about each case + +;(defthm firewall-step-kernel +; (implies (and (subsetp segs (segs 'b)) +; (blacklist segs st) +; (equal (current st) (kernel-name))) +; (blacklist segs (next st))) +; :hints (("Subgoal *1/3'" :use +; (:instance separation (seg (car segs)) +; (st1 st) +; (st2 (scrublist (set-difference-equal +; (segslist (allparts)) +; segs) +; st)))))) + +(defthm firewall-step-firewall-helper + (implies (and (subsetp segs (segs 'b)) + (blacklist segs st) + (equal (current st) 'f)) + (blacklist segs (next st))) + :hints (("Subgoal *1/3'" :cases ((equal (car segs) 'outbox))) + ("Subgoal *1/3.2" :use + (:instance separation (seg (car segs)) + (st1 st) + (st2 (scrublist (set-difference-equal + (segslist (allparts)) + segs) + st)))))) + +(defthm firewall-step-firewall + (implies (and (blacklist (segs 'b) st) + (equal (current st) 'f)) + (blacklist (segs 'b) (next st))) + :hints (("goal" :use (:instance firewall-step-firewall-helper + (segs (segs 'b)))))) + + +(defthm firewall-step-black-helper + (implies (and (blacklist (segs 'b) st) + (equal (current st) 'b) + (subsetp segs (segs 'b))) + (blacklist segs (next st))) + :hints (("Subgoal *1/2'" :use + (:instance separation (seg (car segs)) + (st1 st) + (st2 (scrublist (set-difference-equal + (segslist (allparts)) + (segs 'b)) + st)))))) + +(defthm firewall-step-black + (implies (and (blacklist (segs 'b) st) + (equal (current st) 'b)) + (blacklist (segs 'b) (next st))) + :hints (("goal" :use (:instance firewall-step-black-helper + (segs (segs 'b)))))) + +(defthm intersection-equal-segs-b-segs-other-helper + (implies + (and + (not (equal other 'b)) + (not (equal other 'f)) +; (not (equal other (kernel-name))) + (member x (segs 'b)) + (member other (allparts)) + (subsetp z (dia x))) + (equal (intersection-equal z (segs other)) nil)) + :hints (("Subgoal *1/3''" + :use (:instance dia-setup (seg2 x) (seg1 (car z)) + (p other) + ;; (p2 other) obsolete + ))) + :rule-classes nil) + +(defthm intersection-equal-segs-b-segs-other + (implies + (and + (not (equal other 'b)) + (not (equal other 'f)) +; (not (equal other (kernel-name))) + (member x (segs 'b)) + (member other (allparts))) + (equal (intersection-equal (dia x) (segs other)) nil)) + :hints (("goal" :use + (:instance intersection-equal-segs-b-segs-other-helper + (z (dia x)))))) + +(defthm firewall-step-other-helper + (implies (and (blacklist (segs 'b) st) +; (not (equal (current st) (kernel-name))) + (not (equal (current st) 'f)) + (not (equal (current st) 'b)) + (member (current st) (allparts)) + (subsetp segs (segs 'b))) + (blacklist segs (next st))) + :hints (("Subgoal *1/2'" :use + (:instance separation (seg (car segs)) + (st1 st) + (st2 (scrublist (set-difference-equal + (segslist (allparts)) + (segs 'b)) + st)))))) +(defthm firewall-step-other + (implies (and (blacklist (segs 'b) st) +; (not (equal (current st) (kernel-name))) + (not (equal (current st) 'f)) + (not (equal (current st) 'b)) + (member (current st) (allparts))) + (blacklist (segs 'b) (next st))) + :hints (("goal" :use (:instance firewall-step-other-helper + (segs (segs 'b)))))) + + +;; We combine the sublemmas about a single step into a single lemma +;; about a single step +(defthm firewall-step + (implies + (blacklist (segs 'b) st) + (blacklist (segs 'b) (next st))) + :hints (("goal" :use ( ;firewall-step-kernel + firewall-step-black + firewall-step-firewall + firewall-step-other)))) + +;; +;; The firewall system works: Data in partition b is always black +;; +(defthm firewall-works + (implies + (blacklist (segs 'b) st) + (blacklist (segs 'b) (run st n)))) diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/make-consistency-test.lisp b/books/workshops/2003/greve-wilding-vanfleet/support/make-consistency-test.lisp new file mode 100644 index 0000000..0fbc2a5 --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/make-consistency-test.lisp @@ -0,0 +1,47 @@ + + +;; This code sets up a file that tests whether the axioms of the file +;; firewallworks.lisp are consistent with the axioms introduced in the +;; encapsulates of the files separation.lisp and firewallspec.lisp. + +;; It would be better if ACL2 provided this capability directly, but +;; with some sneaky coding we arrange things so that ACL2 checks that +;; the axioms are consistent. + +(defun read-forms (ifile) + (let ((form (read ifile nil nil))) + (and + form + (cons form (read-forms ifile))))) + +(defun read-all-forms (file) + (with-open-file + (ifile file :direction :input) + (read-forms ifile))) + +;; The forms we need to execute in the consistency test +(defun test-forms () + `( + (include-book "../../../../data-structures/set-theory") + (ld "separation.lisp") + (puff :x) + (ld "firewallspec.lisp") + (puff :x) + + ;; load all the axioms from the file, changing the axioms to defthms + ,@(remove nil + (mapcar + #'(lambda (x) + (if (equal (car x) 'defaxiom) + `(defthm ,@(cdr x)) + nil)) + (read-all-forms "firewallworks.lisp"))) + (ubt! 1) + (certify-book "consistency-test-passed"))) + +(defun make-test (file) + (with-open-file + (ofile file :direction :output) + (mapcar #'(lambda (x) (format ofile "~%~S" x)) (test-forms)))) + + diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/separation.acl2 b/books/workshops/2003/greve-wilding-vanfleet/support/separation.acl2 new file mode 100644 index 0000000..863bcdf --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/separation.acl2 @@ -0,0 +1,4 @@ +(value :q) +(lp) +(include-book "../../../../data-structures/set-theory") +(certify-book "separation" ? t) diff --git a/books/workshops/2003/greve-wilding-vanfleet/support/separation.lisp b/books/workshops/2003/greve-wilding-vanfleet/support/separation.lisp new file mode 100644 index 0000000..bff2596 --- /dev/null +++ b/books/workshops/2003/greve-wilding-vanfleet/support/separation.lisp @@ -0,0 +1,118 @@ +(in-package "ACL2") + +;; Requires set-theory book +;; (include-book "/accts/dagreve/local/src/acl2-2.6/gcl/books/data-structures/set-theory") + +(encapsulate + +;; DIA +;; input: memory segment +;; output: list of memory segments from which direct interaction +;; is allowed + (((dia *) => *) + +;; CURRENT +;; input: machine state +;; output: name of current partition + ((current *) => *) + +;; ALLPARTS +;; input: none +;; output: list of partition names + ((allparts) => *) + +;; KERNEL-NAME +;; input: none +;; output: name of kernel partition +;; ((kernel-name) => *) + +;; SELECT +;; input: memory segment name, machine state +;; output: memory segment values associated segment name + ((select * *) => *) + +;; NEXT +;; input: machine state +;; output: machine state after one step + ((next *) => *) + +;; SEGS +;; input: partition name +;; output: list of memory segment names associated with partition + ((segs *) => *) + + ) + +;; direct interation allowed: list of segments that can communicate +;; directly with seg +(local (defun dia (seg) (list seg))) + +; (local (defun kernel-name () 'k)) + +;; current partition name of st +(local (defun current (st) (declare (ignore st)) 'b)) + +;; list of partition names in st +(local (defun allparts () '(b f))) + +(defthm current-is-partition + (member (current st) (allparts))) + +;(defthm kernel-is-partition +; (member (kernel-name) (allparts))) + +;; Select a segment from state +(local (defun select (seg st) (declare (ignore seg st)) nil)) + +;; Select a list of segments given a list of segment names +(defun selectlist (segs st) + (if (consp segs) + (cons + (select (car segs) st) + (selectlist (cdr segs) st)) + nil)) + +(local (defun next (st) st)) + +(defun run (st n) + (if (zp n) + st + (run (next st) (1- n)))) + +;; The segments associated with a partition name +(local (defun segs (partname) (declare (ignore partname)) nil)) + +;; The segments associated with a list of partition names +(defun segslist (partnamelist) + (if (consp partnamelist) + (append + (segs (car partnamelist)) + (segslist (cdr partnamelist))) + nil)) + +;; Correctness of underlying separation system +(defthm separation + (let ((segs (intersection-equal (dia seg) (segs (current st1))))) + (implies + (and + (equal (selectlist segs st1) (selectlist segs st2)) + (equal (current st1) (current st2)) + (equal (select seg st1) (select seg st2))) + (equal + (select seg (next st1)) + (select seg (next st2)))))) + +;;; The "kernel" partition is the partition switch code. It is special +;;; in several ways. Part of the specification of its correctness is +;;; that it does not change the state of any of the other partitions. + +;(defthm kernel-touches-nothing +; (implies +; (and +; (member seg (segs p)) +; (not (equal p (kernel-name)))) +; (equal +; (intersection-equal (dia seg) (segs (kernel-name))) +; nil))) + +) |