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

Re: EXPAND and IF-THEN?



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



You're trying to do too much at once.

You have to have define some lemmas here, doing arbitrary expansions
on a state as complicated as yours gets too hard for the theorem
prover to follow.

We run into similar problems whenever we define multiple state
transitions.  Properties of these iterated functions on state (node in
your case) tend to be difficult to prove.  We often prove lemmas for
each individual transition, and use the lemmas to get the final
result.

However, if you're bound and determined to proceed along this path of
proving everything at once, here's the proof file for the "first"
case, that avoids the evil pvs halting expansions.  Note, however,
that in this case, the theorem isn't true, (you end up having to
show....

	validCertificate = unknown

which I'm assuming is false) The trick on proving complicated theorems
about record updates like you have here is to work "outside in."  Then
when you get to a point where the field is updated, the rest of the
expansions can be ignored.

I've appended my first try at the proof to the mail message.  If I
were doing it again, I'd do it differently, but I'm getting too hungry
to run through it again.

Hope this helps, feel free to ask if I'm spewing smoke.

John



==============================++====================
John Hoffman, PhD             ||                    
Secure Computing Corporation  || What do you want to
2675 Long Lake Road           || read for, when you 
Roseville, MN  55124          || can watch TV?      
hoffman@securecomputing.com   ||                    
Fax  :(612)628-2701           ||  - Matilda's Father
Phone:(612)628-2808           ||                    
==============================++====================




--------------------
(""
 (USE "initialAEGISServices")
 (FLATTEN)
 (SIMPLIFY)
 (SPLIT)
 (("1"
   (EXPAND "saneBoot")
   (EXPAND "getResource")
   (EXPAND "executeBootSequence")
   (EXPAND "executeService")
   (LIFT-IF)
   (SPLIT)
   (("1"
     (FLATTEN)
     (HIDE -1)
     (REPLACE -6)
     (HIDE -1 -2 -3 -4 -5 -6)
     (EXPAND "levelZeroBoot")
     (LIFT-IF)
     (SPLIT)
     (("1"
       (FLATTEN)
       (HIDE -1)
       (EXPAND "executeService")
       (LIFT-IF)
       (SPLIT)
       (("1"
         (FLATTEN)
         (HIDE -1)
         (REVEAL -7)
         (REPLACE -1)
         (HIDE -1)
         (EXPAND "levelOneBoot")
         (LIFT-IF)
         (SPLIT)
         (("1"
           (FLATTEN)
           (HIDE -1)
           (EXPAND "executeService")
           (LIFT-IF)
           (SPLIT)
           (("1"
             (FLATTEN)
             (HIDE -1)
             (REVEAL -8)
             (REPLACE -1)
             (HIDE -1)
             (EXPAND "levelTwoBoot")
             (LIFT-IF)
             (SPLIT)
             (("1"
               (FLATTEN)
               (HIDE -1)
               (EXPAND "executeService")
               (LIFT-IF)
               (SPLIT)
               (("1"
                 (FLATTEN)
                 (HIDE -1)
                 (REVEAL -9)
                 (REPLACE -1)
                 (HIDE -1)
                 (EXPAND "levelThreeBoot")
                 (LIFT-IF)
                 (SPLIT)
                 (("1"
                   (FLATTEN)
                   (HIDE -1)
                   (EXPAND "executeService")
                   (LIFT-IF)
                   (SPLIT)
                   (("1"
                     (FLATTEN)
                     (HIDE -1)
                     (REVEAL -10)
                     (REPLACE -1)
                     (HIDE -1)
                     (EXPAND "levelFourBoot")
                     (LIFT-IF)
                     (SPLIT)
                     (("1"
                       (FLATTEN)
                       (HIDE -1)
                       (EXPAND "executeService")
                       (LIFT-IF)
                       (SPLIT)
                       (("1"
                         (FLATTEN)
                         (HIDE -1)
                         (REVEAL -11)
                         (REPLACE -1)
                         (HIDE -1)
                         (EXPAND "levelFiveBoot")
                         (EXPAND "installAEGISResources")
                         (EXPAND "installResource")
                         (ASSERT)
                         (POSTPONE))
                        ("2" (POSTPONE))))
                      ("2" (POSTPONE))))
                    ("2" (POSTPONE))))
                  ("2" (POSTPONE))))
                ("2" (POSTPONE))))
              ("2" (POSTPONE))))
            ("2" (POSTPONE))))
          ("2" (POSTPONE))))
        ("2" (POSTPONE))))
      ("2" (POSTPONE))))
    ("2" (POSTPONE))))
  ("2" (POSTPONE)) ("3" (POSTPONE)) ("4" (POSTPONE)) ("5" (POSTPONE))))