[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: EXPAND and IF-THEN?



> 
> > 
> > 
> > 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))