← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2003/greve-wilding-vanfleet/support/firewallspec.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2003/greve-wilding-vanfleet/support/firewallspec.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
;; Essay on formalizing "black" data.
 
4
 
 
5
;; This file introduces some concepts useful in specifying a firewall.
 
6
;; It was not immediately obvious how to formalize the correct
 
7
;; operation of a firewall.  What makes it difficult is describing
 
8
;; what it means for data not to contain sensitive information.  We
 
9
;; introduce the notion of "black", which is a predicate on a segment
 
10
;; name and a system state.  The intended interpretation is that black
 
11
;; segments do not contain sensitive information that requires
 
12
;; protection.
 
13
 
 
14
;; Mostly we leave "black" unspecified.  However, we assume that it
 
15
;; has the following properties:
 
16
 
 
17
;; 1.  If all segments in a system are black, then after the system
 
18
;;     progresses one step each segment is black.  (No "spontaneous
 
19
;;     generation".)
 
20
 
 
21
;; 2.  There exists a function "scrub" that modifies a segment so 
 
22
;;     that it is black.  
 
23
 
 
24
;; 3.  Elements of system state that are not associated with the
 
25
;;     segment are irrelevant in deciding whether a segment is black.
 
26
 
 
27
;; Is this approach to modeling reasonable?  Assume that each byte of
 
28
;; the system has associated with it a "black" bit that tells whether
 
29
;; the byte is cleared.  Any operation that produces data sets the
 
30
;; result's black bit to the "and" of all the input black bits.
 
31
 
 
32
;; Axiom one holds, since any operation will set black bits if every
 
33
;; segment in the system has its black bits set.  Note that
 
34
;; applications are not modeled at this level, but it is worth
 
35
;; considering whether this framework could model something like a
 
36
;; decryption algorithm.  Note that decryption requires keys or
 
37
;; algorithms that would not be considered "black" in this framework,
 
38
;; so this axiom would not be inconsistent with such models.
 
39
 
 
40
;; Axiom two holds since one can "scrub" a data segment by zeroizing
 
41
;; all the data and setting the black bits.  (Of course, not under
 
42
;; user control.)
 
43
 
 
44
;; Axiom three holds since it is straightforward to tell if a segment
 
45
;; is black by checking all its black bits.
 
46
 
 
47
(encapsulate
 
48
;; BLACK
 
49
;; input: segment name, machine state
 
50
;; output: boolean indicating whether segment is cleared
 
51
 
 
52
 (((black * *) => *)
 
53
 
 
54
;; SCRUB
 
55
;; input: segment name, machine state
 
56
;; output machine state in which segment is cleared and other
 
57
;;   segments are untouched
 
58
 
 
59
 ((scrub * *) => *)
 
60
)
 
61
 
 
62
;; A "black" segment contains no sensitive information
 
63
(local (defun black (segname st) (declare (ignore segname) (ignore st)) t))
 
64
 
 
65
;; A list of segments is all black
 
66
(defun blacklist (segnames st)
 
67
   (if (consp segnames)
 
68
       (and
 
69
        (black (car segnames) st)
 
70
        (blacklist (cdr segnames) st))
 
71
     t))
 
72
 
 
73
;; A segment to be "scrubbed"
 
74
(local (defun scrub (seg st) (declare (ignore seg)) st))
 
75
 
 
76
;; A list of segments to be "scrubbed"
 
77
(defun scrublist (segs st)
 
78
         (if (consp segs)
 
79
             (scrublist (cdr segs) (scrub (car segs) st))
 
80
           st))
 
81
 
 
82
(defthm scrub-commutative
 
83
  (equal
 
84
   (scrub seg1 (scrub seg2 st))
 
85
   (scrub seg2 (scrub seg1 st))))
 
86
 
 
87
(defthm segment-scrub-different
 
88
  (implies (not (equal seg1 seg2))
 
89
           (equal (select seg1 (scrub seg2 st))
 
90
                  (select seg1 st))))
 
91
(defthm black-scrub
 
92
  (equal
 
93
   (black seg1 (scrub seg2 st))
 
94
   (or
 
95
    (equal seg1 seg2)
 
96
    (black seg1 st))))
 
97
 
 
98
(defthm current-scrub
 
99
  (equal
 
100
   (current (scrub seg st))
 
101
   (current st)))
 
102
 
 
103
;; If every segment is black, then after one step an arbitrary segment
 
104
;; is black
 
105
(defthm spontaneous-generation
 
106
  (implies
 
107
   (blacklist (segslist (allparts)) st)
 
108
   (black seg (next st))))
 
109
 
 
110
;; Only the contents of a segment determine its blackness
 
111
(defthm black-function-of-segment
 
112
  (implies
 
113
   (equal (select x st1) (select x st2))
 
114
   (equal (black x st1) (black x st2)))
 
115
  :rule-classes nil)
 
116
 
 
117
)
 
118
 
 
119
 
 
120