Delivery-Date: 
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Date: Thu, 22 Jul 93 16:09:42 EDT
From: garrel@msiadmin.cit.cornell.edu (Garrel Pottinger-MSI Visitor)
Message-Id: <9307222009.AA00471@msiadmin.cit.cornell.edu>
To: info-hol@ted.cs.uidaho.edu
Subject: Design verification
Cc: D.MacKenzie@ed.ac.uk, garrel@msiadmin.cit.cornell.edu

I'm working on a research report titled Proof Requirements in the Orange Book:
Origins, Implementation, and Implications (a brief research description is
appended), and the evidence I've accumulated indicates that the design
verification activities madated by the Orange Book for highly secure opearting
systems tend to be epiphenomenal --- that is, the design verification
is carried out, but it has very little effect on system construction.  On the
other hand, my impression is that this isn't the case for design verification
done in work on hardware.

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 would be grateful for suggestions about answers to these questions and
references to the relevant literature.

Regards,

Garrel

**********************************************************************

RESEARCH DESCRIPTION --- The Orange Book (officially, Department of Defense
Trusted Computer System Evaluation Criteria, DOD 5200.28-STD) defines a
hierarchy of security classes for computer systems.  The hierarchy has seven
levels --- D, C1, C2, B1, B2, B3, A1, listed in order of increasing security.
Beginning with class B2, some of the requirements used in defining assurance
for the hierarchy of security classes mandate that the system and/or its
design be proved to have certain specified properties, and these proof
requirements become increasingly stringent in passing from level B2 through
level B3 to level A1.

The research addresses three main questions, focusing in each case on issues
related to proof requirements.  The questions are:  (1) Origins -- Why and
how was the Orange Book written?  (2) Implementation -- What kinds of
ambiguities and vagueness associated with the requirements defining assurance
for the hierarchy of security classes came to light when producers of computer
systems tried to build systems meeting these requirements, and how were
ambiguities and vagueness resolved?  (3) Implications -- What implications do
the answers to questions (1) and (2) have for future attempts to specify
assurance for computer systems?

The project report is based on a combination of documentary evidence and
interviews with persons involved in the processes mentioned in (1) and (2).