Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Message-Id: <9307261527.AA14788@dbms1.cs.byu.edu>
To: garrel@msiadmin.cit.cornell.edu (Garrel Pottinger-MSI Visitor)
Cc: info-hol@ted.cs.uidaho.edu
Subject: Re: Design verification
In-Reply-To: Your message of Thu, 22 Jul 93 16:09:42 -0400. <9307222009.AA00471@msiadmin.cit.cornell.edu>
Date: Mon, 26 Jul 93 09:27:03 -0600
From: Phil Windley <windley@dbms1.cs.byu.edu>


On Thu, 22 Jul 93 16:09:42 EDT, garrel@msiadmin.cit.cornell.edu wrote:
+------------
| This leads to two questions:  (1)~Is my impression that, in hardware
| verification, design verification has a definite effect on chip construction
| correct? (2)~Assuming a positive answer to (1), what is the reason for the
| contrast and does it apply generally to design verification in work on
| software, or just to design verification in work on secure software?


I have done what might be considered "design verification" (although I have
been taken to task by reviewers for using this term).  For example, I
verified several important properties about the supervisory mode in AVM-1.
The reason that these efforts had an effect on the underlying
implementation is that I already had a functional correctness theorem.  So,
while I was proving D ==> P (where D is the design and P is a property), I
already had a theorem that said I ==> D (where I is the implementation) and
eventually, I combined these to reach the conclusion I ==> P.

My impression of Orange Book type verifications is that there is never an
effort to show I ==> D and indeed many security folks I have talked to
consider this a waste of time.  Thus, as you point out Garrel, the
verification effort proves D ==> P and then someone goes off and writes
code that has no formal connection to D.  

So, I would conclude that your impression is correct, but only because
I ==> D already exists, OR I ==> P is done directly (since, after all,
hardware is so much simpler than software ;-).  

--phil--


Phillip J. Windley, Asst. Professor   |  windley@cs.byu.edu
Laboratory for Applied Logic	      |  
Dept. of Computer Science, TMCB 3370  |
Brigham Young University              |  Phone: 801.378.3722
Provo UT       84602-6576             |  Fax:   801.378.7775