[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: EXPAND and IF-THEN?
- To: pvs-help@csl.sri.com
- Subject: Re: EXPAND and IF-THEN?
- From: Darryl Scott Dieckman <ddieckma@ececs.uc.edu>
- Date: Wed, 28 Jan 1998 16:26:19 -0500 (EST)
- In-Reply-To: <199801272314.RAA12986@mishra.sctc.com> from "John Hoffman" at Jan 27, 98 05:14:14 pm
>
> >
> >
> > I am running into some problems when I use EXPAND. Basically each
> > time I expand a certain sequence of terms, PVS gets slower and slower,
> > and eventually never returns from a call to EXPAND. If I use EXPAND
> > with the :ASSERT NONE option, the EXPAND command works just fine,
> > however, I eventually have to ASSERT/SIMPLIFY, and then PVS never
> > returns. I still consider myself a new user to PVS, so I am looking
> > for some quick advice or guidance to help me figure out what is really
> > going on.
> >
> > The term that I am expanding, expands into an IF-THEN statment. If I
> > make the IF-THEN statement inert by making the THEN and ELSE clauses
> > the same, the prover runs through my proof at an acceptable rate.
> > However, if the THEN and ELSE clauses are different, the prover never
> > returns. It may also be useful to know that all of these terms that I
> > am expanding manipulate a record which represents the state of my
> > system.
> >
> > Any help on the following questions would be great:
> > 1. Why does EXPAND keep getting slower and slower?
> > 2. How can I tell what PVS is doing when it is slow?
> > 3. Is it common for people to use records to represent the state of a
> > system, or are there a number of problems that I will be running into
> > later?
> >
> > Thanks.
> >
> > Darryl Dieckman
> >
>
> I'm guessing the specific problem is connected with what your record
> update functions look like. Look at the theorem (the version you get
> when you use the :ASSERT NONE option) and see how many different cases
> might have to be dealt with in simplyfing your expressions. Depending
> on how you've specified things, you could be getting into exponential
> numbers of cases in your theorem. Thus explaining the length of time
> in the assert. Perhaps you need to change the way you've specified
> your record updates.
>
> We've use records for a number of rather large specs (rather large =
> 10k lines) and not had difficulties. For complicated updates, we tend
> to localize for specific fields into individual functions, and prove
> lemmas that show that changes in portions of the state do not affect
> the desired theorem.
>
> If you could give us a specific example, it would help quite a bit.
>
> Don't have an answer for 2.
>
I am attaching the PVS dump file for my theories. Within the Sane
theory, I was trying to prove the aegis_secure theorem. The partial
proof included runs find on both linux and solaris machines. However,
if after running the partial proof, you execute
(postpone)
(expand "governService")
PVS goes off, and never comes back (never being greater than 45
minutes).
%Patch files loaded: patch2 version 2.414
$$$pvs-strategies
(defstep expand-governservice ()
(repeat (try (expand "governService" :OCCURRENCE 1)
(try (lift-if)
(try (expand "svcCanBeGoverned")
(skip)
(skip))
(skip))
(skip)))
;;(lift-if)(expand "svcCanBeGoverned"))
"Strategy used to eliminate governService from terms"
"Expanding governService, if-lifting, expanding svcCanBeGoverned")
(defstep expand-installservice ()
(repeat (try (expand "installService" :occurrence 1)
(try (expand "governService" :occurrence 1)
(try (lift-if) (skip) (skip))
(skip))
(skip)))
"Strategy used to eliminate installService from terms"
"Expanding governService, if-lifting, expanding svcCanBeGoverned")
$$$Sane.pvs
Sane : THEORY
BEGIN
IMPORTING InitNodes
IMPORTING DSA
BootLevel : TYPE = {
levelZero,
levelOne,
levelTwo,
levelThree,
levelFour,
levelFive
}
getBootLevelResource(level : BootLevel) : Resource =
CASES level OF
levelZero:
levelZeroCert,
levelOne:
levelOneCert,
levelTwo:
levelTwoCert,
levelThree:
levelThreeCert,
levelFour:
levelFourCert,
levelFive:
levelFiveCert
ENDCASES
integrityValid(level : BootLevel, node : Node) : bool =
validCertificate =
getResource(getBootLevelResource(level), node)
executeBootSequence(node : Node) : Node =
LET pkt = nullPacket IN
executeService(levelZeroBootSvc, pkt, node)
%
% Integrity Failure recovery procedure
%
recover(level : BootLevel, node : Node) : Node =
LET res : Resource = getBootLevelResource(level) IN
executeBootSequence(setResource(res, validCertificate, node))
% The integrity of a layer can only be guaranteed if and only if:
% (1) the integrity of the lower layers is checked, and
% (2) transitions to higher layers occur only after integrity checks
% them are complete.
% The resulting integrity "chain" inductively guarantees system
% integrity. This is called the Chaining Layered Integrity Checks
% (CLIC) model.
% AEGIS Boot Process
%
%
% Services
% Every level has a boot service associated with it. This service
% specifies the pre/post conditions associated with execution of
% that step within the boot sequence.
%
% Policies
% Every level has a boot policy associated with it. This policy
% determines if the boot service for the level can be accessed.
%
% Security Requirements
%
% 1. When the boot sequence is completed, the security requirements for
% all boot levels must be satisfied.
% 2. If during the boot sequence, the node is determined to be insecure,
% then the node must only execute packets received from a trusted
% source.
%
bootPolicyGovernFunc(svc: Service, pol : Policy) : bool = false;
bootPolicyAccessFunc(pkt: Packet, svc: Service) : bool = true;
levelZeroBoot(node : Node, pkt: Packet) : Node =
IF integrityValid(levelOne, node) THEN
executeService(levelOneBootSvc, pkt, node)
ELSE
recover(levelOne, node)
ENDIF
% Level 1
% Contains remainder of BIOS code and CMOS
%
levelOneBoot(node : Node, pkt: Packet) : Node =
IF integrityValid(levelTwo, node) THEN
executeService(levelTwoBootSvc, pkt, node)
ELSE
recover(levelTwo, node)
ENDIF
% Level 2
% Contains all expansion cards, and their associated ROMs
%
levelTwoBoot(node : Node, pkt: Packet) : Node =
IF integrityValid(levelThree, node) THEN
executeService(levelThreeBootSvc, pkt, node)
ELSE
recover(levelThree, node)
ENDIF
% Level 3
% Contains operating system boot blocks. These are resident on the
% bootable device and are responsible for loading the operating
% system kernel.
%
levelThreeBoot(node : Node, pkt: Packet) : Node =
IF integrityValid(levelFour, node) THEN
executeService(levelFourBootSvc, pkt, node)
ELSE
recover(levelFour, node)
ENDIF
% Level 4
% Contains the operating system
%
levelFourBoot(node : Node, pkt: Packet) : Node =
IF integrityValid(levelFive, node) THEN
executeService(levelFiveBootSvc, pkt, node)
ELSE
recover(levelFive, node)
ENDIF
% Level 5
% Contains user level programs and any network hosts
%
levelFiveBoot(node : Node, pkt: Packet) : Node =
node WITH [
status := BOOT
]
%
% Install resources present within a node prior to execution of
% the boot sequence
%
installAEGISResources(node : Node) : Node =
installResource(levelFiveCert,
installResource(levelFourCert,
installResource(levelThreeCert,
installResource(levelTwoCert,
installResource(levelOneCert,
installResource(levelZeroCert,node))))))
%
% Install security policies for each of the boot levels
%
installAEGISPolicies(node : Node) : Node =
installPolicy(bootPolicy, address(node),
bootPolicyAccessFunc, bootPolicyGovernFunc, node)
%
% Install services representing the operations performed at each of
% the boot levels.
%
installAEGISServices(node : Node) : Node =
installService(levelFiveBootSvc, bootPolicy,
installService(levelFourBootSvc, bootPolicy,
installService(levelThreeBootSvc, bootPolicy,
installService(levelTwoBootSvc, bootPolicy,
installService(levelOneBootSvc, bootPolicy,
installService(levelZeroBootSvc, bootPolicy,node))))))
initialAEGISServices : AXIOM
serviceLookup(levelFiveBootSvc) = levelFiveBoot AND
serviceLookup(levelFourBootSvc) = levelFourBoot AND
serviceLookup(levelThreeBootSvc) = levelThreeBoot AND
serviceLookup(levelTwoBootSvc) = levelTwoBoot AND
serviceLookup(levelOneBootSvc) = levelOneBoot AND
serviceLookup(levelZeroBootSvc) = levelZeroBoot
saneBoot(addr : Address) : Node =
executeBootSequence(
installAEGISResources(
installAEGISServices(
installAEGISPolicies(newNode(addr)))))
test_secure3 : THEOREM
LET node : Node =
installResource(levelOneCert,
installResource(levelZeroCert,
installService(levelZeroBootSvc, bootPolicy,
installPolicy(bootPolicy, administrator,
bootPolicyAccessFunc, bootPolicyGovernFunc,
newNode(administrator)))))
IN
validCertificate = getResource(levelOneCert, executeBootSequence(node))
aegis_secure : THEOREM
LET node : Node = saneBoot(administrator) IN
validCertificate = getResource(levelOneCert, node) AND
validCertificate = getResource(levelTwoCert, node) AND
validCertificate = getResource(levelThreeCert, node) AND
validCertificate = getResource(levelFourCert, node) AND
validCertificate = getResource(levelFiveCert, node)
END Sane
$$$Sane.prf
(|Sane|
(|test_secure3| "" (SIMPLIFY)
(("" (EXPAND "installService")
(("" (EXPAND "installService")
(("" (EXPAND "installPolicy")
(("" (EXPAND "newNode")
(("" (EXPAND "nullNode")
(("" (EXPAND "governService")
(("" (LIFT-IF)
(("" (SPLIT)
(("1" (FLATTEN)
(("1" (EXPAND "installResource")
(("1" (EXPAND "executeBootSequence")
(("1" (EXPAND "executeService")
(("1" (LIFT-IF)
(("1" (HIDE -1)
(("1"
(EXPAND "pktCanAccess")
(("1"
(SPLIT)
(("1"
(FLATTEN)
(("1"
(HIDE -1)
(("1"
(LEMMA "initialAEGISServices")
(("1"
(FLATTEN)
(("1"
(REPLACE -6 1)
(("1"
(HIDE -1 -2 -3 -4 -5)
(("1"
(HIDE -1)
(("1"
(EXPAND
"levelZeroBoot")
(("1"
(LIFT-IF)
(("1"
(EXPAND
"integrityValid")
(("1"
(EXPAND
"getBootLevelResource")
(("1"
(EXPAND
"getResource")
(("1"
(SIMPLIFY)
(("1"
(EXPAND
"recover")
(("1"
(EXPAND
"getBootLevelResource")
(("1"
(EXPAND
"setResource")
(("1"
(SIMPLIFY)
(("1"
(LIFT-IF)
(("1"
(SPLIT)
(("1"
(FLATTEN)
(("1"
(HIDE
1)
(("1"
(EXPAND
"executeBootSequence")
(("1"
(EXPAND
"executeService")
(("1"
(EXPAND
"pktCanAccess")
(("1"
(SIMPLIFY)
(("1"
(LIFT-IF)
(("1"
(SPLIT)
(("1"
(FLATTEN)
(("1"
(REVEAL
-1)
(("1"
(REPLACE
-1
1)
(("1"
(EXPAND
"levelZeroBoot")
(("1"
(HIDE
-1
-2)
(("1"
(LIFT-IF)
(("1"
(EXPAND
"integrityValid")
(("1"
(EXPAND
"getBootLevelResource")
(("1"
(EXPAND
"getResource")
(("1"
(SIMPLIFY)
(("1"
(EXPAND
"executeService")
(("1"
(EXPAND
"pktCanAccess")
(("1"
(LIFT-IF)
(("1"
(SPLIT)
(("1"
(FLATTEN)
(("1"
(REVEAL
-8)
(("1"
(REPLACE
-1
1)
(("1"
(EXPAND
"levelOneBoot")
(("1"
(SIMPLIFY)
(("1"
(PROPAX)
NIL)))))))))))
("2"
(FLATTEN)
(("2"
(PROPAX)
NIL)))))))))))))))))))))))))))))))
("2"
(FLATTEN)
(("2"
(PROPAX)
NIL)))))))))))))))))))
("2"
(FLATTEN)
(("2"
(EXPAND
"executeBootSequence")
(("2"
(EXPAND
"executeService")
(("2"
(LIFT-IF)
(("2"
(SPLIT)
(("1"
(FLATTEN)
(("1"
(REVEAL
-1)
(("1"
(REPLACE
-1
1)
(("1"
(EXPAND
"levelZeroBoot")
(("1"
(EXPAND
"integrityValid")
(("1"
(EXPAND
"getBootLevelResource")
(("1"
(EXPAND
"getResource")
(("1"
(SIMPLIFY)
(("1"
(PROPAX)
NIL)))))))))))))))))
("2"
(FLATTEN)
(("2"
(HIDE
-1
2)
(("2"
(EXPAND
"pktCanAccess")
(("2"
(GRIND)
NIL)))))))))))))))))))))))))))))))))))))))))))))))))))))))
("2"
(FLATTEN)
(("2"
(HIDE 2)
(("2"
(GRIND)
NIL)))))))))))))))))))))
("2" (FLATTEN)
(("2" (HIDE 2)
(("2" (GRIND) NIL)))))))))))))))))))))))
(|aegis_secure| "" (LEMMA "initialAEGISServices")
(("" (SIMPLIFY)
(("" (FLATTEN)
(("" (SPLIT)
(("1" (POSTPONE) NIL)
("2" (EXPAND "saneBoot")
(("2" (EXPAND "installAEGISPolicies")
(("2" (EXPAND "installPolicy")
(("2" (EXPAND "newNode")
(("2" (EXPAND "nullNode")
(("2" (SIMPLIFY)
(("2" (EXPAND "installAEGISServices")
(("2" (EXPAND "installService" 1 6)
(("2" (EXPAND "installService" 1 6)
(("2" (EXPAND "governService")
(("2" (LIFT-IF)
(("2"
(SPLIT)
(("1"
(FLATTEN)
(("1"
(EXPAND "installService" 1 5)
(("1"
(EXPAND "installService" 1 5)
(("1"
(EXPAND "governService")
(("1"
(LIFT-IF)
(("1"
(SPLIT)
(("1"
(FLATTEN)
(("1"
(EXPAND
"installService"
1
4)
(("1"
(EXPAND
"installService"
1
4)
(("1"
(EXPAND
"governService")
(("1"
(LIFT-IF)
(("1"
(SPLIT)
(("1"
(EXPAND
"installService"
1
3)
(("1"
(EXPAND
"installService"
1
3)
(("1"
(EXPAND
"governService")
(("1"
(LIFT-IF)
(("1"
(SPLIT)
(("1"
(FLATTEN)
(("1"
(EXPAND
"installService"
1
2)
(("1"
(EXPAND
"installService"
1
2)
(("1"
(EXPAND
"governService")
(("1"
(LIFT-IF)
(("1"
(SPLIT)
(("1"
(FLATTEN)
(("1"
(EXPAND
"installService"
1
1)
(("1"
(EXPAND
"installService"
1
1)
(("1"
(POSTPONE)
NIL)))))))
("2"
(POSTPONE)
NIL)))))))))))))
("2"
(POSTPONE)
NIL)))))))))))
("2"
(POSTPONE)
NIL)))))))))))))
("2"
(POSTPONE)
NIL)))))))))))))
("2"
(POSTPONE)
NIL)))))))))))))))))))))))))
("3" (POSTPONE) NIL) ("4" (POSTPONE) NIL)
("5" (POSTPONE) NIL))))))))))
$$$DSA.pvs
DSA : THEORY
BEGIN
SecureHash : TYPE+
Certificate : TYPE+
DSAVerify(hash : SecureHash, cert : Certificate) : bool = true
END DSA
$$$Policies.pvs
Policies % [ parameters ]
: THEORY
BEGIN
IMPORTING Store
END Policies
$$$Access.pvs
Access % [ parameters ]
: THEORY
BEGIN
IMPORTING Nodes
IMPORTING Policies
%===========================================================================
svcCanBeGoverned(node: Node, svc: Service, pol: Policy) : bool =
%---------------------------------------------------------------------------
% Description:
% A service can be goverened by a policy only if all the policies
% currently governing the service will allow the new policy to also
% govern the service.
% Arguments:
% node: Node
% svc: Service to be governed
% pol: Policy to govern the service
%===========================================================================
member(svc, services(node)) AND
(FORALL (p: (svcGovernedBy(node)(svc))) : polGovernFunc(node)(p)(svc,pol))
%===========================================================================
pktCanAccess(node: Node, pkt: Packet, svc: Service) : bool =
%---------------------------------------------------------------------------
% Description:
% A packet can access a service if all of the security policies
% which govern the service will allow the packet to access the
% service.
% Arguments:
% node: Node
% pkt: Packet requesting access
% svc: Service to access
%===========================================================================
member(svc, services(node)) AND
(FORALL (p: (svcGovernedBy(node)(svc))): polAccessFunc(node)(p)(pkt,svc))
%===========================================================================
governService(svc : Service, pol : Policy, node: Node) : Node =
%---------------------------------------------------------------------------
% Description:
% Assign the given policy as a govener of the given service
% Arguments:
% node - Current state of node
% pol - Policy to assign as a governer
% svc - Service to govern
%===========================================================================
IF svcCanBeGoverned(node,svc,pol) THEN
node WITH [
(polGoverns)(pol) := add(svc,polGoverns(node)(pol)),
(svcGovernedBy)(svc) := add(pol,emptyset[Policy])
]
ELSE
node
ENDIF
installService(svc : Service, node: Node): Node =
node WITH [
services := add(svc, services(node))
]
installService(svc : Service, pol : Policy, node: Node): Node =
governService(svc, pol,
installService(svc, node))
installPolicy(pol : Policy, admin : Address,
accessFunc : AccessFuncType, governFunc: GovernFuncType,
node : Node) : Node =
node WITH [
policies := add(pol,policies(node)),
polOwns := polOwns(node) WITH [ pol := emptyset[Service]],
polGoverns := polGoverns(node) WITH [ pol := emptyset[Service]],
polAdmin := polAdmin(node) WITH [ pol := admin ],
polAccessFunc := polAccessFunc(node) WITH [pol := accessFunc],
polGovernFunc := polGovernFunc(node) WITH [pol := governFunc]
]
installResource(res : Resource, node : Node) : Node =
node WITH [
resources := resources(node) WITH [res := unknown]
]
setResource(res : Resource, val: ResourceValue, node: Node) : Node =
IF resources(node)(res) /= notInstalled THEN
node with [
resources := resources(node) WITH [res := val]
]
ELSE
node
ENDIF
getResource(res : Resource, node: Node) : ResourceValue =
resources(node)(res)
%===========================================================================
%---------------------------------------------------------------------------
% Description:
% Arguments:
%===========================================================================
END Access
$$$Store.pvs
Store % [ parameters ]
: THEORY
BEGIN
% ASSUMING
% assuming declarations
% ENDASSUMING
IMPORTING ActiveTypes
IMPORTING Nodes
ServiceSpec : TYPE = [Node, Packet -> Node]
PacketSpec : TYPE = [Node, Packet -> Node]
serviceLookup : [Service->ServiceSpec]
accessFuncLookup : [Policy->AccessFuncType]
governFuncLookup : [Policy->GovernFuncType]
packetSpecLookup : [Packet -> PacketSpec]
packetServiceLookup : [Packet -> Service]
packetPolicyLookup : [Packet -> Policy]
END Store
$$$Packets.pvs
Packets : THEORY
BEGIN
IMPORTING ActiveTypes
IMPORTING Store
IMPORTING Access
extractService(pkt : Packet) : Service =
packetServiceLookup(pkt)
extractPolicy(pkt : Packet) : Policy =
packetPolicyLookup(pkt)
canExecute(node : Node, pkt : Packet) : bool =
(FORALL (s : Service) :
member(s, services(node)) IMPLIES
pktCanAccess(node, pkt, s))
executePacket(pkt: Packet, node : Node) : Node =
IF canExecute(node,pkt) THEN
packetSpecLookup(pkt)(node,pkt)
ELSE
node
ENDIF
newPacket(newPtype : PacketType,
newSrc : Address,
newDest : Address,
newServices : set[Service],
newLimit : ResourceLimit,
newPayload : Payload,
newChecksum : Checksum
) : Packet =
(#
ptype := newPtype,
src := newSrc,
dest := newDest,
services := newServices,
limit := newLimit,
payload := newPayload,
checksum := newChecksum
#)
nullPacket : Packet =
newPacket(nullPacketType,
nullAddress,
nullAddress,
emptyset[Service],
nullResourceLimit,
nullPayload,
nullChecksum
)
newPacket(pkt : Packet) : Packet =
(#
ptype := ptype(pkt),
src := src(pkt),
dest := dest(pkt),
services := services(pkt),
limit := limit(pkt),
payload := payload(pkt),
checksum := checksum(pkt)
#)
END Packets
$$$Comm.pvs
Comm % [ parameters ]
: THEORY
BEGIN
IMPORTING Packets
% This version of send places the packet directly in the receive queue
% of the destination node. Once we have specified network operations,
% we will place the packet in the send queue, and let the network
% handle the delivery of the packet.
% send(pkt: Packet, destNode: Node) : Node =
% IF address(destNode) = dest(pkt) THEN
% destNode WITH [
% recvQ := add(pkt,recvQ(destNode))
% ]
% ELSE
% destNode
% ENDIF
% Network version of send
send(pkt: Packet, node: Node) : Node =
node WITH [
sendQ := add(pkt, sendQ(node))
]
recv(node : Node) : Node =
IF nonempty?(recvQ(node)) THEN
executePacket(first(recvQ(node)),node) WITH [
recvQ := rest(recvQ(node))
]
ELSE
node
ENDIF
END Comm
$$$Services.pvs
Services : THEORY
BEGIN
IMPORTING Nodes
IMPORTING Comm
IMPORTING Store
IMPORTING Policies
%
% Core services
%
% What does a service do?
% What does a service require?
% A packet requires access to all the services that it uses
% before it is able to execute.
% How do we specify what is required?
%
% What does a service ensure?
% A service ensures what is specified in the service spec.
% What is a service spec?
% What is the signature of a service spec?
%
% What does a service modify?
% A service can modify the state of the node
%
% How do you know what packets a service requires?
% How do you know that the packet is not lying?
% How does the service cause the state to change?
%
%
% sendPacketSvc
% Arguments: pkt Packet to send
% spec Packet specification
%
%nullSvc : Service
%installSvcSvc : Service
%installPolSvc : Service
%sendPacketSvc : Service
nullSvcSpec(node : Node, pkt : Packet) : Node = node
sendPacketSpec(node: Node, pkt : Packet) : Node =
send(pkt, node)
installSvcSpec(node : Node, pkt : Packet) : Node =
LET svc : Service = extractService(pkt) IN
installService(svc, node)
installPolSpec(node : Node, pkt : Packet) : Node =
node
% LET pol : Policy = extractPolicy(pkt) IN
% installPolicy(pol, src(pkt), node)
executeService(service : Service, pkt : Packet, node : Node) : Node =
IF pktCanAccess(node, pkt, service) THEN
serviceLookup(service)(node, pkt)
ELSE
node
ENDIF
END Services
$$$Queue.pvs
Queue [T: TYPE+] : THEORY
BEGIN
Queue : TYPE+
q: VAR Queue
empty?, nonempty?: [Queue -> boolean]
queue_disjoint: AXIOM NOT empty?(q) IFF nonempty?(q)
queue_inclusive: AXIOM empty?(q) OR nonempty?(q)
exists_nonempty: AXIOM (EXISTS (x: [[T, Queue] ->(nonempty?)]):TRUE)
exists_empty: AXIOM (EXISTS (x: [[T, Queue] ->(empty?)]):TRUE)
add: [T, Queue -> (nonempty?)]
first: [(nonempty?) -> T]
rest: [(nonempty?) -> Queue]
size: [Queue -> nat]
empty: (empty?)
e: VAR T
e1, e2: VAR T
nq, nq1, nq2: VAR (nonempty?)
empty1, empty2: VAR (empty?)
empty_extensionality: AXIOM empty1 = empty2
add_extensionality: AXIOM
first(nq1) = first(nq2) AND rest(nq1) = rest(nq2) IMPLIES nq1 = nq2
add_eta: AXIOM add(first(nq), rest(nq)) = nq
first_add: AXIOM
first(add(e, q)) =
IF empty?(q) THEN e
ELSE first(q)
ENDIF
rest_add: AXIOM
rest(add(e, q)) =
IF empty?(q) THEN q
ELSE add(e, rest(q))
ENDIF
p: VAR pred[Queue]
queue_induction: AXIOM
((FORALL (q: Queue): empty?(q) IMPLIES p(q))
AND (FORALL (e: T), (q1: Queue): p(q1) IMPLIES p(add(e, q1))))
IMPLIES (FORALL (q2: Queue): p(q2))
size_rest: AXIOM size(rest(nq)) = size(nq) - 1
size_add: AXIOM size(add(e, q)) = size(q) + 1
size_empty: AXIOM empty?(q) IFF size(q) = 0
empty_is_not_nonempty: LEMMA NOT empty?(q) IMPLIES nonempty?(q)
nonempty_is_not_empty: LEMMA NOT nonempty?(q) IMPLIES empty?(q)
nonempty_add: LEMMA NOT empty?(add(e, q))
END Queue
$$$Queue.prf
(|Queue|
(|add_TCC1| "" (EXISTENCE-TCC)
(("" (LEMMA "exists_nonempty") (("" (PROPAX) NIL)))))
(|empty_TCC1| "" (EXISTENCE-TCC)
(("" (LEMMA "exists_empty") (("" (GRIND) NIL)))))
(|empty_extensionality| "" (POSTPONE) NIL)
(|first_add_TCC1| "" (SUBTYPE-TCC)
(("" (LEMMA "queue_disjoint") (("" (GRIND) NIL))))))
$$$ActiveTypes.pvs
ActiveTypes: THEORY
BEGIN
PacketType : TYPE+
ResourceLimit : TYPE+
Checksum : TYPE+
Payload : TYPE+
nullPacketType : PacketType
nullResourceLimit : ResourceLimit
nullChecksum : Checksum
nullPayload : Payload
Address : TYPE = {
nullAddress,
administrator,
client,
gatekeeper,
attacker,
mingus
}
Resource : TYPE = {
nullResource,
levelZeroCert,
levelOneCert,
levelTwoCert,
levelThreeCert,
levelFourCert,
levelFiveCert
}
ResourceValue : TYPE = {
notInstalled,
unknown,
validCertificate,
invalidCertificate
}
Service : TYPE = {
installSvcSvc,
installPolSvc,
sendPacketSvc,
myServiceSvc,
levelZeroBootSvc,
levelOneBootSvc,
levelTwoBootSvc,
levelThreeBootSvc,
levelFourBootSvc,
levelFiveBootSvc,
nullSvc
}
Policy : TYPE = {
initialPolicy,
adminPolicy,
clientPolicy,
myPolicy,
bootPolicy,
nullPolicy
}
Packet : TYPE = [#
ptype : PacketType,
src : Address,
dest : Address,
services : set[Service],
limit : ResourceLimit,
payload : Payload,
checksum : Checksum
#]
%===========================================================================
% SERVICE ACCESS FUNCTION
%---------------------------------------------------------------------------
% The service access function determines if a packet can be granted
% access to the specified service. Each policy installed on the
% active node will provide its own requirements which must be
% satisfied to allow access to the resources which it governs.
%===========================================================================
AccessFuncType : TYPE = [Packet,Service->bool]
nullAccessFunc(pkt : Packet, svc : Service) : bool = false;
%===========================================================================
% SERVICE GOVERN FUNCTION
%---------------------------------------------------------------------------
% The service govern function determines if a service can be governed
% by an additional policy. When a new policy wishes to govern an
% existing service, all policies which currently govern the service
% must permit the service to be governed by the new policy. Each
% policy installed on the active node will provide its own
% requirements which must be satisfied to allow its services to be
% governed by other policies.
%===========================================================================
GovernFuncType : TYPE = [Service,Policy->bool]
nullGovernFunc(svc:Service, pol: Policy) : bool = false;
END ActiveTypes
$$$Nodes.pvs
Nodes : THEORY
BEGIN
IMPORTING ActiveTypes
IMPORTING Queue[Packet]
%===========================================================================
% NODE SERVICE ARCHITECTURE
%---------------------------------------------------------------------------
% Description:
% The node service architecture is composed of services, resources,
% security policies, and some relations between them.
%
% Collections
% -----------
% services Set of services installed on the node
% resources Set of resources present on the node
% policies Set of security policies installed on the node
%
% Relations
% -----------
% polOwns Set of services which a policy owns. Each service
% may only be owned by one policy.
% polGoverns Set of services which a policy governs. A service
% may be governed by more than one policy.
% polAdmin The host that is the administrator of the policy
% polAccessFunc A function which the policy uses to detmine if
% access to services for specific packets should be
% granted.
% polGovernFunc A function which determines if other policies may
% govern services which are owned by this policy.
%===========================================================================
NodeStatus : TYPE = {
UNKNOWN,
BOOT
}
Node : TYPE = [#
address : Address,
sendQ : Queue[Packet], % Currently unused
recvQ : Queue[Packet],
services : set[Service],
resources : [Resource -> ResourceValue],
policies : set[Policy],
polOwns : [Policy ->set[Service]],
polGoverns : [Policy ->set[Service]],
polAdmin : [Policy->Address],
polAccessFunc : [Policy->AccessFuncType],
polGovernFunc : [Policy->GovernFuncType],
svcGovernedBy : [Service->set[Policy]],
status : NodeStatus
#]
END Nodes
$$$InitNodes.pvs
InitNodes : THEORY
BEGIN
IMPORTING Nodes
IMPORTING Services
initGovernFunc(svc : Service, pol : Policy) : bool = true;
initAccessFunc(pkt : Packet, svc : Service) : bool =
IF src(pkt) = administrator THEN
true
ELSE
false
ENDIF
nullNode : Node = (#
address := nullAddress,
sendQ := Queue.empty,
recvQ := Queue.empty,
services := emptyset[Service],
resources := (LAMBDA (r:Resource) : notInstalled),
policies := emptyset[Policy],
polOwns := (LAMBDA (p:Policy) : emptyset[Service]),
polGoverns := (LAMBDA (p:Policy) : emptyset[Service]),
polAdmin := (LAMBDA (p:Policy) : nullAddress),
polAccessFunc := (LAMBDA (p:Policy) : nullAccessFunc),
polGovernFunc := (LAMBDA (p:Policy) : nullGovernFunc),
svcGovernedBy := (LAMBDA (s:Service) : emptyset[Policy]),
status := UNKNOWN
#)
newNode(addr : Address) : Node =
nullNode WITH [
address := addr
]
initNode(addr : Address, node: Node) : Node =
installService(sendPacketSvc, initialPolicy,
installService(installPolSvc, initialPolicy,
installService(installSvcSvc, initialPolicy,
installPolicy(initialPolicy, addr, initAccessFunc, initGovernFunc,
newNode(addr)))))
initial_services : AXIOM
serviceLookup(nullSvc) = nullSvcSpec AND
serviceLookup(installSvcSvc) = installSvcSpec AND
serviceLookup(installPolSvc) = installPolSpec AND
serviceLookup(sendPacketSvc) = sendPacketSpec
END InitNodes
$$$InitNodes.prf
(|InitNodes| (|nullNode_TCC1| "" (SUBTYPE-TCC))
(|initNode_TCC1| "" (SUBTYPE-TCC) NIL))