home *** CD-ROM | disk | FTP | other *** search
/ Hackers Toolkit v2.0 / Hackers_Toolkit_v2.0.iso / HTML / archive / Rainbow / ncsc / purplencsc.txt < prev    next >
Text File  |  1999-11-04  |  61KB  |  1,460 lines
  1. Guidelines for Formal Verification Systems
  2.  
  3.  
  4.  
  5. NCSC-TG-014-89
  6. Library No.  S-231,308
  7.  
  8.  
  9.  
  10.  FOREWORD 
  11.  
  12.  
  13.  
  14.  
  15.  
  16. This publication, Guidelines for Formal Verification Systems, is issued by 
  17. the National Computer Security Center (NCSC) under the authority and in 
  18. accordance with Department of Defense (DoD) Directive 5215.1, "Computer 
  19. Security Evaluation Center."  The guidelines defined in this document are 
  20. intended for vendors building formal specification and verification 
  21. systems that trusted system developers may use in satisfying the 
  22. requirements of the Department of Defense Trusted Computer System 
  23. Evaluation Criteria (TCSEC), DoD 5200.28-STD, and the Trusted Network 
  24. Interpretation of the TCSEC.
  25.  
  26. As the Director, National Computer Security Center, I invite your
  27. recommendations for revision to this technical guideline.  Address all
  28. proposals for revision through appropriate channels to the National Computer
  29. Security Center, 9800 Savage Road, Fort George G.  Meade, MD, 20755-6000,
  30. Attention: Chief, Technical Guidelines Division.
  31.  
  32.  
  33.  
  34.  
  35.  
  36.  
  37.  
  38.  
  39. Patrick R.  Gallagher, Jr.
  40.                                                                                 
  41.                                 1 April 1989 
  42. Director 
  43. National Computer Security Center
  44.  
  45.  
  46.  
  47.  
  48.                         ACKNOWLEDGMENTS 
  49.  
  50.  
  51.  
  52.  
  53. The National Computer Security Center expresses appreciation to Barbara 
  54. Mayer and Monica McGill Lu as principal authors and project managers of 
  55. this document.  We recognize their contribution to the technical content 
  56. and presentation of this publication.
  57.  
  58. We thank the many individuals who contributed to the concept, development, 
  59. and review of this document.  In particular, we acknowledge:  Karen 
  60. Ambrosi, Tom Ambrosi, Terry Benzel, David Gibson, Sandra Goldston, Dale 
  61. Johnson, Richard Kemmerer, Carl Landwehr, Carol Lane, John McLean, 
  62. Jonathan Millen, Andrew Moore, Michele Pittelli, Marvin Schaefer, Michael 
  63. Sebring, Jeffrey Thomas, Tom Vander-Vlis, Alan Whitehurst, James Williams, 
  64. Kimberly Wilson, and Mark Woodcock.  Additionally, we thank the 
  65. verification system developers and the rest of the verification community 
  66. who helped develop this document.
  67.  
  68.  
  69.  
  70. TABLE OF CONTENTS
  71.  
  72.  
  73. FOREWORD        i
  74. ACKNOWLEDGMENTS ii
  75. PREFACE iv
  76. 1. INTRODUCTION 1
  77.         1.1 PURPOSE     1
  78.         1.2 BACKGROUND  1
  79.         1.3 SCOPE       2
  80. 2. EVALUATION APPROACH  3
  81.         2.1 EVALUATION OF NEW SYSTEMS   3
  82.         2.2 REEVALUATION FOR ENDORSEMENT        5
  83.         2.3 REEVALUATION FOR REMOVAL    6
  84.         2.4 BETA VERSIONS       7
  85. 3. METHODOLOGY AND SYSTEM SPECIFICATION 8
  86.         3.1 METHODOLOGY 8
  87.         3.2 FEATURES    9
  88.         3.2.1 Specification Language    9
  89.         3.2.2 Specification Processing  10
  90.         3.2.3 Reasoning Mechanism       11
  91.         3.3 ASSURANCE, SOUNDNESS, AND ROBUSTNESS        12
  92.         3.4 DOCUMENTATION       14
  93. 4. IMPLEMENTATION AND OTHER SUPPORT FACTORS     15
  94.         4.1 FEATURES    15
  95.         4.1.1 User Interface    15
  96.         4.1.2 Hardware Support  16
  97.         4.2 ASSURANCE   17
  98.         4.2.1 Configuration Management  17
  99.         4.2.2 Support and Maintenance   19
  100.         4.2.3 Testing   19
  101.         4.3 DOCUMENTATION       19
  102. 5. FUTURE DIRECTIONS    23
  103. APPENDIX A: CONFIGURATION MANAGEMENT    25
  104. GLOSSARY        28
  105. BIBLIOGRAPHY    35
  106.  
  107.  
  108.                  PREFACE 
  109.  
  110.  
  111.  
  112.  
  113. One of the goals of the NCSC is to encourage the development of 
  114. production-quality verification systems.  This guideline was developed as 
  115. part of the Technical Guideline Program specifically to support this goal.
  116.  
  117. Although there are manual methodologies for performing formal 
  118. specification and verification, this guideline addresses verification 
  119. systems that provide automated support. 
  120.  
  121. Throughout the document, the term developer is used to describe the 
  122. developer of the verification system.  The term vendor is used to describe 
  123. the individual(s) who are providing support for the tool.  These 
  124. individuals may or may not be the same for a particular tool.
  125.  
  126.  
  127.  
  128.  
  129.  1.             INTRODUCTION 
  130.  
  131.  
  132. The principal goal of the National Computer Security Center (NCSC) is to 
  133. encourage the widespread availability of trusted computer systems.  In 
  134. support of this goal the DoD Trusted Computer System Evaluation Criteria 
  135. (TCSEC) was created, against which computer systems could be evaluated.  
  136. The TCSEC was originally published on 15 August 1983 as CSC-STD-001-83.  
  137. In December 1985 the DoD modified and adopted the TCSEC as a DoD Standard, 
  138. DoD 5200.28-STD. [1]
  139.  
  140.  
  141.           1.1           PURPOSE  
  142.  
  143. This document explains the requirements for formal verification systems 
  144. that are candidates for the NCSC's Endorsed Tools List (ETL). [5]  This 
  145. document is primarily intended for developers of verification systems to 
  146. use in the development of production-quality formal verification systems.  
  147. It explains the requirements and the process used to evaluate formal 
  148. verification systems submitted to the NCSC for endorsement.
  149.  
  150.  
  151.           1.2           BACKGROUND  
  152.  
  153. The requirement for NCSC endorsement of verification systems is stated in 
  154. the TCSEC and the Trusted Network Interpretation of the TCSEC (TNI). [4]  
  155. The TCSEC and TNI are the standards used for evaluating security controls 
  156. built into automated information and network systems, respectively.  The 
  157. TCSEC and TNI classify levels of trust for computer and network systems by 
  158. defining divisions and classes within divisions.  Currently, the most 
  159. trusted class defined is A1, Verified Design, which requires formal design 
  160. specification and formal verification.  As stated in the TCSEC and TNI, ". 
  161. . . verification evidence shall be consistent with that provided within 
  162. the state of the art of the particular Computer Security Center-endorsed 
  163. formal specification and verification system used." [1]
  164.  
  165. Guidelines were not available when the NCSC first considered endorsing 
  166. verification systems.  The NCSC based its initial endorsement of 
  167. verification systems on support and maintenance of the system, acceptance 
  168. within the verification community, and stability of the system.
  169.  
  170.           1.3           SCOPE  
  171.  
  172. Any verification system that has the capability for formally specifying 
  173. and verifying the design of a trusted system to meet the TCSEC and TNI A1 
  174. Design Specification and Verification requirement can be considered for 
  175. placement on the ETL.  Although verification systems that have 
  176. capabilities beyond design verification are highly encouraged by the NCSC, 
  177. this guideline focuses mainly on those aspects of verification systems 
  178. that are sufficient for the design of candidate A1 systems.
  179.  
  180. The requirements described in this document are the primary consideration 
  181. in the endorsement process.  They are categorized as either methodology 
  182. and system specification or implementation and other support factors.  
  183. Within each category are requirements for features, assurances, and 
  184. documentation.  
  185.  
  186. The requirements cover those characteristics that can and should exist in 
  187. current verification technology for production-quality systems.  A 
  188. production-quality verification system is one that is sound, 
  189. user-friendly, efficient, robust, well documented, maintainable, developed 
  190. with good software engineering techniques, and available on a variety of 
  191. hardware. [2]  The NCSC's goal is to elevate the current state of  
  192. verification technology to production quality, while still encouraging the 
  193. advancement of research in the verification field.
  194.  
  195. Since the NCSC is limited in resources for both evaluation and support of 
  196. verification systems, the ETL may reflect this limitation.  Verification 
  197. systems placed on the ETL will either be significant improvements to 
  198. systems already on the list or will provide a useful approach or 
  199. capability that the currently endorsed systems lack.
  200.  
  201. This guideline was written to help in identifying the current needs in 
  202. verification systems and to encourage future growth of verification 
  203. technology.  The evaluation process is described in the following section. 
  204.  Verification systems will be evaluated against the requirements listed in 
  205. sections 3 and 4.  Section 5 contains a short list of possibilities for 
  206. next-generation verification systems.  It is not an all-encompassing list 
  207. of features as this would be counterproductive to the goals of research.
  208.  
  209. 2.              EVALUATION APPROACH 
  210.  
  211.  
  212. A formal request for evaluation of a verification system for placement on 
  213. the ETL shall be submitted in writing directly to:
  214.                                 National Computer Security Center
  215.                                 ATTN:           Deputy 
  216. C       (Verification Committee Chairperson)
  217.                                 9800 Savage Road
  218.                                 Fort George G. Meade, MD 20755-6000
  219. Submitting a verification system does not guarantee NCSC evaluation or 
  220. placement on the ETL.
  221.  
  222. The developers shall submit a copy of the verification system to the NCSC 
  223. along with supporting documentation and tools, test suites, configuration 
  224. management evidence, and source code.  In addition, the system developers 
  225. shall support the NCSC evaluators.  For example, the developers shall be 
  226. available to answer questions, provide training, and meet with the 
  227. evaluation team.
  228.  
  229. There are three cases in which an evaluation can occur:  1) the evaluation 
  230. of a new verification system being considered for placement on the ETL, 2) 
  231. the reevaluation of a new version of a system already on the ETL for 
  232. placement on the ETL (reevaluation for endorsement), and 3) the 
  233. reevaluation of a system on the ETL being considered for removal from the 
  234. ETL (reevaluation for removal).
  235.  
  236.  
  237.           2.1           EVALUATION OF NEW SYSTEMS  
  238.  
  239. To be considered for initial placement on the ETL, the candidate endorsed 
  240. tool must provide some significant feature or improvement that is not 
  241. available in any of the currently endorsed tools.  If the verification 
  242. system meets this requirement, the evaluators shall analyze the entire 
  243. verification system, concentrating on the requirements described in 
  244. Chapters 3 and 4 of this document.  If a requirement is not completely 
  245. satisfied, but the developer is working toward completion, the relative 
  246. significance of the requirement shall be measured by the evaluation team.  
  247. The team shall determine if the deficiency is substantial or detrimental.  
  248. For example, a poor user interface would not be as significant as the lack 
  249. of a justification of the methodology.  Requirements not completely 
  250. satisfied shall be identified and documented in the final evaluation 
  251. report.
  252.  
  253. Studies or prior evaluations (e.g., the Verification Assessment Study 
  254. Final Report) [2] performed on the verification system shall be reviewed.  
  255. Strengths and weaknesses identified in other reports shall be considered 
  256. when evaluating the verification system.
  257.  
  258. The following are the major steps leading to an endorsement and ETL 
  259. listing for a new verification system.
  260.  
  261.                 1)      The developer submits a request for evaluation to 
  262. the NCSC Verification Committee Chairperson.
  263.  
  264.                 2)      The Committee meets to determine whether the 
  265. verification system provides a significant improvement to systems already 
  266. on the ETL or provides a useful approach or capability that the existing 
  267. systems lack.
  268.  
  269.                 3)      If the result is favorable, an evaluation team is 
  270. formed and the verification system evaluation begins.
  271.  
  272.                 4)      Upon completion of the evaluation, a Technical 
  273. Assessment Report (TAR) is written by the evaluation team.
  274.  
  275.                 5)      The Committee reviews the TAR and makes 
  276. recommendations on endorsement.
  277.  
  278.                 6)      The Committee Chairperson approves or disapproves 
  279. endorsement.
  280.  
  281.                 7)      If approved, an ETL entry is issued for the 
  282. verification system.
  283.  
  284.                 8)      A TAR is issued for the verification system.
  285.  
  286.  
  287.          2.2           REEVALUATION FOR ENDORSEMENT  
  288.  
  289. The term reevaluation for endorsement denotes the evaluation of a new 
  290. version of an endorsed system for placement on the ETL.  A significant 
  291. number of changes or enhancements, as determined by the developer, may 
  292. warrant a reevaluation for endorsement.  The intent of this type of 
  293. reevaluation is to permit improvements to endorsed versions and advocate 
  294. state-of-the-art technology on the ETL while maintaining the assurance of 
  295. the original endorsed version.  
  296.  
  297. A verification system that is already on the ETL maintains assurance of 
  298. soundness and integrity through configuration management (see Appendix).  
  299. The documentation of this process is evidence for the reevaluation of the 
  300. verification system.  Reevaluations are based upon an assessment of all 
  301. evidence and a presentation of this material by the vendor to the NCSC.  
  302. The NCSC reserves the right to request additional evidence as necessary.
  303.  
  304. The vendor shall prepare the summary of evidence in the form of a Vendor 
  305. Report (VR).  The vendor may submit the VR to the NCSC at any time after 
  306. all changes have ended for the version in question.  The VR shall relate 
  307. the reevaluation evidence at a level of detail equivalent to the TAR.  The 
  308. VR shall assert that assurance has been upheld and shall include 
  309. sufficient commentary to allow an understanding of every change made to 
  310. the verification system since the endorsed version.  
  311.  
  312. The Committee shall expect the vendor to present a thorough technical 
  313. overview of changes to the verification system and an analysis of the 
  314. changes, demonstrating continuity and retention of assurance.  The 
  315. Committee subsequently issues a rec*ommendation to the Committee 
  316. Chairperson stating that assurance has or has not been maintained by the 
  317. current verification system since it was endorsed.  If the verification 
  318. system does not sustain its endorsement, the vendor may be given the 
  319. option for another review by the Committee.  The reevaluation cycle ends 
  320. with an endorsement determination by the Committee Chairperson, and if the 
  321. determination is favorable, a listing of the new release is added to the 
  322. ETL, replacing the previously endorsed version; the old version is then 
  323. archived.
  324.  
  325. The following are the major steps leading to an endorsement and ETL 
  326. listing for a revised verification system.
  327.  
  328.                 1)      The vendor submits the VR and other materials to 
  329. the NCSC Verification Committee Chairperson.
  330.  
  331.                 2)      An evaluation team is formed to review the VR.
  332.  
  333.                 3)      The team adds any additional comments and submits 
  334. them to the Verification Committee.
  335.  
  336.                 4)      The vendor defends the VR before the Committee.
  337.  
  338.                 5)      The Committee makes recommendations on endorsement.
  339.  
  340.                 6)      The Committee Chairperson approves or disapproves 
  341. endorsement.
  342.  
  343.                 7)      If approved, a new ETL entry is issued for the 
  344. revised verification system.
  345.  
  346.                 8)      The VR is issued for the revised verification 
  347. system.
  348.  
  349.  
  350.           2.3           REEVALUATION FOR REMOVAL  
  351.  
  352. Once a verification system is endorsed, it shall normally remain on the 
  353. ETL as long as it is supported and is not replaced by another system.  The 
  354. Committee makes the final decision on removal of a verification system 
  355. from the ETL.  For example, too many bugs, lack of users, elimination of 
  356. support and maintenance, and unsoundness are all reasons which may warrant 
  357. removal of a verification system from the ETL.  Upon removal, the 
  358. Committee makes a formal announcement and provides a written justification 
  359. of their decision.  
  360.  
  361. Systems on the ETL that are removed or replaced shall be archived.  
  362. Systems developers that have a Memorandum of Agreement (MOA) with the NCSC 
  363. to use a verification system that is later archived may continue using the 
  364. system agreed upon in the MOA.  Verification evidence from a removed or 
  365. replaced verification system shall not be accepted in new system 
  366. evaluations for use in satisfying the A1 Design Specification and 
  367. Verification requirement.
  368.  
  369. The following are the major steps leading to the removal of a verification 
  370. system from the ETL.
  371.  
  372.                 1)      The Verification Committee questions the 
  373. endorsement of a verification system on the ETL.
  374.  
  375.                 2)      An evaluation team is formed and the verification 
  376. system evaluation begins, focusing on the area in question.
  377.  
  378.                 3)      Upon completion of the evaluation, a TAR is 
  379. written by the evaluation team.
  380.  
  381.                 4)      The Committee reviews the TAR and makes 
  382. recommendations on removal.
  383.  
  384.                 5)      The Committee Chairperson approves or disapproves 
  385. removal.
  386.  
  387.                 6)      If removed, a new ETL is issued eliminating the 
  388. verification system in question.
  389.  
  390.                 7)      A TAR is issued for the verification system under 
  391. evaluation.
  392.  
  393.  
  394.           2.4           BETA VERSIONS  
  395.  
  396. Currently, verification systems are not production quality tools and are 
  397. frequently being enhanced and corrected.  The version of a verification 
  398. system that has been endorsed may not be the newest and most capable 
  399. version.  Modified versions are known as beta tool versions.  Beta 
  400. versions are useful in helping system developers uncover bugs before 
  401. submitting the verification system for evaluation.
  402.  
  403. The goal of beta versions is to stabilize the verification system.  Users 
  404. should not assume that any particular beta version will be evaluated or 
  405. endorsed by the NCSC.  If the developer of a trusted system is using a 
  406. beta version of a formal verification system, specifications and proof 
  407. evidence shall be submitted to the NCSC which can be completely checked 
  408. without significant modification using an endorsed tool as stated in the 
  409. A1 requirement.  This can be accomplished by using either the currently 
  410. endorsed version of a verification system or a previously endorsed version 
  411. that was agreed upon by the trusted system developer and the developer's 
  412. evaluation team.  Submitted specifications and proof evidence that are not 
  413. compatible with the endorsed or agreed-upon version of the tool may 
  414. require substantial modification by the trusted system developer.
  415.  
  416.  3.             METHODOLOGY AND SYSTEM SPECIFICATION 
  417.  
  418.  
  419. The technical factors listed in this Chapter are useful measures of the 
  420. quality and completeness of a verification system.  The factors are 
  421. divided into four categories: 1) methodology, 2) features, 3) assurance, 
  422. and 4) documentation.  Methodology is the underlying principles and rules 
  423. of organization of the verification system.  Features include the 
  424. functionality of the verification system.  Assurance is the confidence and 
  425. level of trust that can be placed in the verification system.  
  426. Documentation consists of a set of manuals and technical papers that fully 
  427. describe the verification system, its components, application, operation, 
  428. and maintenance.
  429.  
  430. These categories extend across each of the components of the verification 
  431. system.  These components minimally consist of the following:
  432.  
  433.         a)      a mathematical specification language that allows the user 
  434. to express correctness conditions,
  435.  
  436.         b)      a specification processor that interprets the 
  437. specification and generates conjectures interpretable by the reasoning 
  438. mechanism, and 
  439.  
  440.         c)      a reasoning mechanism that interprets the conjectures 
  441. generated by the processor and checks the proof or proves that the 
  442. correctness conditions are satisfied.
  443.  
  444.  
  445.           3.1           METHODOLOGY  
  446.  
  447. The methodology of the verification system shall consist of a set of 
  448. propositions used as rules for performing formal verification in that 
  449. system.  This methodology shall have a sound, logical basis.  This 
  450. requirement is a necessary but not sufficient condition for the 
  451. endorsement of the system.
  452.  
  453.  
  454.           3.2           FEATURES  
  455.  
  456.  
  457.                    3.2.1        Specification Language   
  458.  
  459.                 a.      Language expressiveness.
  460.  
  461.                 The specification language shall be sufficiently 
  462. expressive to support the methodology of the verification system.  This 
  463. ensures that the specification language is powerful and rich enough to 
  464. support the underlying methodology.  For example, if the methodology 
  465. requires that a specification language be used to model systems as state 
  466. machines, then the specification language must semantically and 
  467. syntactically support all of the necessary elements for modeling systems 
  468. as state machines.  
  469.  
  470.                 b.      Defined constructs.
  471.  
  472.                 The specification language shall consist of a set of 
  473. constructs that are rigorously defined (e.g., in Backus-Naur Form with 
  474. appropriate semantic definitions).  This implies that the language is 
  475. formally described by a set of rules for correct use.
  476.  
  477.                 c.      Mnemonics.
  478.  
  479.                 The syntax of the specification language shall be clear 
  480. and concise without obscuring the interpretation of the language 
  481. constructs.  Traditional symbols from mathematics should be employed 
  482. wherever possible; reasonably mnemonic symbols should be used in other 
  483. cases.  This aids the users in interpreting constructs more readily.
  484.  
  485.                 d.      Internal uniformity.
  486.  
  487.                 The syntax of the specification language shall be 
  488. internally uniform.  This ensures that the rules of the specification 
  489. language are not contradictory.
  490.  
  491.                 e.      Overloading.
  492.  
  493.                 Each terminal symbol of the specification language's 
  494. grammar should support one and only one semantic definition insofar as it 
  495. increases comprehensibility.  When it is beneficial to incorporate more 
  496. than one definition for a symbol or construct, the semantics of the 
  497. construct shall be clearly defined from the context used.  This is 
  498. necessary to avoid confusion by having one construct with more than one 
  499. interpretation or more than one construct with the same interpretation.  
  500. For example, the symbol "+" may be used for both integer and real 
  501. addition, but it should not be used to denote both integer addition and 
  502. conjunction.
  503.  
  504.                 f.      Correctness conditions.
  505.  
  506.                 The specification language shall provide the capability to 
  507. express correctness conditions.
  508.  
  509.                 g.      Incremental verification.
  510.  
  511.                 The methodology shall allow incremental verification.  
  512. This would allow, for example, a verification of portions of a system 
  513. specification at a single time.  Incremental verification may also include 
  514. the capability for performing verification of different levels of 
  515. abstraction.  This allows essential elements to be presented in the most 
  516. abstract level and important details to be presented at successive levels 
  517. of refinement.
  518.  
  519.  
  520.                    3.2.2        Specification Processing   
  521.  
  522.                 a.      Input.
  523.  
  524.                 All of the constructs of the specification language shall 
  525. be processible by the specification processor(s).  This is necessary to 
  526. convert the specifications to a language or form that is interpretable by 
  527. the reasoning mechanism.
  528.  
  529.                 b.      Output.
  530.  
  531.                 The output from the processor(s) shall be interpretable by 
  532. the reasoning mechanism.  Conjectures derived from the correctness 
  533. conditions shall be generated.  The output shall also report errors in 
  534. specification processing to the user in an easily interpretable manner.
  535.  
  536.  
  537.                    3.2.3        Reasoning Mechanism   
  538.  
  539.                 a.      Compatibility of components.
  540.  
  541.                 The reasoning mechanism shall be compatible with the other 
  542. components of the verification system to ensure that the mechanism is 
  543. capable of determining the validity of conjectures produced by other 
  544. components of the verification system.  For example, if conjectures are 
  545. generated by the specification processor that must be proven, then the 
  546. reasoning mechanism must be able to interpret these conjectures correctly.
  547.  
  548.                 b.      Compatibility of constructs.
  549.  
  550.                 The well-formed formulas in the specification language 
  551. that may also be input either directly or indirectly into the reasoning 
  552. mechanism using the language(s) of the reasoning mechanism shall be 
  553. mappable to ensure compatibility of components.  For example, if a lemma 
  554. can be defined in the specification language as "LEMMA " and can also be defined in the reasoning mechanism, then the 
  555. construct for the lemma in the reasoning mechanism shall be in the same 
  556. form.
  557.  
  558.                 c.      Documentation.
  559.  
  560.                 The reasoning mechanism shall document the steps it takes 
  561. to develop the proof.  Documentation provides users with a stable, 
  562. standard reasoning mechanism that facilitates debugging and demonstrates 
  563. completed proofs.  If the reasoning mechanism is defined to use more than 
  564. one method of reasoning, then it should clearly state which method is used 
  565. and remain consistent within each method of reasoning.
  566.  
  567.                 d.      Reprocessing.
  568.  
  569.                 The reasoning mechanism shall provide a means for 
  570. reprocessing completed proof sessions.  This is to ensure that users have 
  571. a means of reprocessing theorems without reconstructing the proof process. 
  572.  This mechanism shall also save the users from reentering voluminous input 
  573. to the reasoning mechanism.  For example, reprocessing may be accomplished 
  574. by the generation of command files that can be invoked to recreate the 
  575. proof session.
  576.  
  577.                 e.      Validation.
  578.  
  579.                 The methodology shall provide a means for validating proof 
  580. sessions independently of the reasoning mechanism.  Proof strategies 
  581. checked by an independent, trustworthy proof checker shall ensure that 
  582. only sound proof steps were employed in the proof process.  Trustworthy 
  583. implies that there is assurance that the proof checker accepts only valid 
  584. proofs.  The validation process shall not be circumventable and shall 
  585. always be invoked for each completed proof session.
  586.  
  587.                 f.      Reusability.
  588.  
  589.                 The reasoning mechanism shall facilitate the use of 
  590. system- and user-supplied databases of reusable definitions and theorems.  
  591. This provides a foundation for proof sessions that will save the user time 
  592. and resources in reproving similar theorems and lemmas.
  593.  
  594.                 g.      Proof dependencies.
  595.  
  596.                 The reasoning mechanism shall track the status of the use 
  597. and reuse of theorems throughout all phases of development.  Proof 
  598. dependencies shall be identified and maintained so that if modifications 
  599. are made to a specification (and indirectly to any related 
  600. conjectures/theorems), the minimal set of theorems and lemmas that are 
  601. dependent on the modified proofs will need to be reproved.
  602.  
  603.  
  604.           3.3           ASSURANCE, SOUNDNESS, AND ROBUSTNESS   
  605.  
  606.         a.      Sound basis.
  607.  
  608.         Each of the verification system's tools and services shall support 
  609. the method*ology.  This ensures that users can understand the 
  610. functionality of the verification system with respect to the methodology 
  611. and that the methodology is supported by the components of the 
  612. verification system.
  613.  
  614.         b.      Correctness.
  615.  
  616.         The verification system shall be rigorously tested to provide 
  617. assurance that the majority of the system is free of error.
  618.  
  619.         c.      Predictability.
  620.  
  621.         The verification system shall behave predictably.  Consistent 
  622. results are  needed for the users to interpret the results homogeneously.  
  623. This will ensure faster and easier interpretation and fewer errors in 
  624. interpretation.  
  625.  
  626.         d.      Previous use.
  627.  
  628.         The verification system shall have a history of use to establish 
  629. stability, usefulness, and credibility.  This history shall contain 
  630. documentation of applications (for example, applications from academia or 
  631. the developers).  These applications shall test the verification system, 
  632. so that strengths and weaknesses may be uncovered.
  633.  
  634.         e.      Error recovery.
  635.  
  636.         The verification system shall gracefully recover from internal 
  637. software errors.  This error handling is necessary to ensure that errors 
  638. in the verification system do not cause damage to a user session.
  639.  
  640.         f.      Software engineering.
  641.  
  642.         The verification system shall be implemented using documented 
  643. software engineering practices.  The software shall be internally 
  644. structured into well-defined, independent modules for ease of 
  645. maintainability and configuration management.  
  646.  
  647.         g.      Logical theory.
  648.  
  649.         All logical theories used in the verification system shall be 
  650. sound.  If more than one logical theory is used in the verification 
  651. system, then there shall be evidence that the theories work together via a 
  652. metalogic.  This provides the users with a sound method of interaction 
  653. among the theories.
  654.  
  655.         h.      Machine independence.
  656.  
  657.         The functioning of the methodology and the language of the 
  658. verification system shall be machine independent.  This is to ensure that 
  659. the functioning of the theory, specification language, reasoning mechanism 
  660. and other essential features does not change from one machine to another.  
  661. Additionally, the responses that the user receives from each of the 
  662. components of the verification system should be consistent across the 
  663. different hardware environments that support the verification system.
  664.  
  665.  
  666.           3.4           DOCUMENTATION  
  667.  
  668.         a.      Informal justification.
  669.  
  670.         An informal justification of the methodology behind the 
  671. verification system shall be provided.  All parts of the methodology must 
  672. be fully documented to serve as a medium for validating the accuracy of 
  673. the stated implementation of the verification system.  The logical theory 
  674. used in the verification system shall be documented.  If more than one 
  675. logical theory exists in the system, the metalogic employed in the system 
  676. shall be explained and fully documented.  This documentation is essential 
  677. for the evaluators and will aid the users in understanding the methodology.
  678.  
  679.         b.      Formal definition.
  680.  
  681.         A formal definition (e.g., denotational semantics) of the 
  682. specification language(s) shall be provided.  A formal definition shall 
  683. include a clear semantic definition of the expressions supported by the 
  684. specification language and a concise description of the syntax of all 
  685. specification language constructs.  This is essential for the evaluators 
  686. and will aid the users in understanding the specification language.
  687.  
  688.         c.      Explanation of methodology.
  689.  
  690.         A description of how to use the methodology, its tools, its 
  691. limitations, and the kinds of properties that it can verify shall be 
  692. provided.  This is essential for users to be able to understand the 
  693. methodology and to use the verification system effectively.
  694.  
  695.  4.             IMPLEMENTATION AND OTHER SUPPORT FACTORS 
  696.  
  697.  
  698. The NCSC considers the support factors listed in this section to be 
  699. measures of the usefulness, understandability, and maintainability of the 
  700. verification system.  The support factors are divided into the following 
  701. three categories:  1) features, 2) assurances, and 3) documentation.
  702.  
  703. Two features that provide support for the user are the interface and the 
  704. base hardware of the verification system.  Configuration management, 
  705. testing, and mainte*nance are three means of providing assurance.  (The 
  706. Appendix contains additional information on configuration management.)  
  707. Documentation consists of a set of manuals and technical papers that fully 
  708. describe the verification system, its components, application, operation, 
  709. and maintenance.
  710.  
  711.  
  712.           4.1           FEATURES  
  713.  
  714.  
  715.                    4.1.1        User Interface   
  716.  
  717.                 a.      Ease of use.
  718.  
  719.                 The interface for the verification system shall be 
  720. user-friendly.  Input must be understandable, output must be informative, 
  721. and the entire interface must support the users' goals.
  722.  
  723.                 b.      Understandable input.
  724.  
  725.                 Input shall be distinct and concise for each language 
  726. construct and ade*quately represent what the system requires for the 
  727. construct.  
  728.  
  729.                 c.      Understandable output.
  730.  
  731.                 Output from the components of the verification system 
  732. shall be easily interpretable, precise, and consistent.  This is to ensure 
  733. that users are provided with understandable and helpful information.  
  734.  
  735.                 d.      Compatibility.
  736.  
  737.                 Output from the screen, the processor, and the reasoning 
  738. mechanism shall be compatible with their respective input, where 
  739. appropriate.  It is reasonable for a specification processor (reasoning 
  740. mechanism) to put assertions into a canonical form, but canonical forms 
  741. should be compatible in the specification language (reasoning mechanism).
  742.  
  743.                 e.      Functionality.
  744.  
  745.                 The interface shall support the tasks required by the user 
  746. to exercise the verification system effectively.  This is to ensure that 
  747. all commands necessary to utilize the components of the methodology are 
  748. available and functioning according to accompanying documentation.
  749.  
  750.                 f.      Error reporting.
  751.  
  752.                 The verification system shall detect, report, and recover 
  753. from errors in a specification.  Error reporting shall remain consistent 
  754. by having the same error message generated each time the error identified 
  755. in the message is encountered.  The output must be informative and 
  756. interpretable by the users.
  757.  
  758.  
  759.                    4.1.2        Hardware Support   
  760.  
  761.                 a.      Availability.
  762.  
  763.                 The verification system shall be available on commonly 
  764. used computer systems.  This will help ensure that users need not purchase 
  765. expensive or outdated machines, or software packages to run the 
  766. verification system.
  767.  
  768.                 b.      Efficiency.
  769.  
  770.                 Processing efficiency and memory usage shall be reasonable 
  771. for specifications of substantial size.  This ensures that users are able 
  772. to process simple (no complex constructs), short (no more than two or 
  773. three pages) specifications in a reasonable amount of time (a few 
  774. minutes).  The processing time of larger, more complex specifications 
  775. shall be proportional to the processing time of smaller, less complex 
  776. specifications.  Users should not need to wait an unacceptable amount of 
  777. time for feedback.
  778.  
  779.  
  780.           4.2           ASSURANCE  
  781.  
  782.  
  783.                    4.2.1        Configuration Management   
  784.  
  785.                 a.      Life-cycle maintenance.
  786.  
  787.                 Configuration management tools and procedures shall be 
  788. used to track changes (both bug fixes and new features) to the 
  789. verification system from initial concept to final implementation.  This 
  790. provides both the system maintainers and the evaluators with a method of 
  791. tracking the numerous changes made to the verification system to ensure 
  792. that only sound changes are implemented.
  793.  
  794.                 b.      Configuration items.
  795.  
  796.                 Identification of Configuration Items (CIs) shall begin 
  797. early in the design stage.  CIs are readily established on a logical basis 
  798. at this time.  The configuration management process shall allow for the 
  799. possibility that system changes will convert non-CI components into CIs.
  800.  
  801.                 c.      Configuration management tools.
  802.  
  803.                 Tools shall exist for comparing a newly generated version 
  804. with the pre*vious version.  These tools shall confirm that a) only the 
  805. intended changes have been made in the code that will actually be used as 
  806. the new version of the verification system, and b) no additional changes 
  807. have been inserted into the verification system that were not intended by 
  808. the system developer.  The tools used to perform these functions shall 
  809. also be under strict configuration control.  
  810.  
  811.                 d.      Configuration control.
  812.  
  813.                 Configuration control shall cover a broad range of items 
  814. including software, documentation, design data, source code, the running 
  815. version of the object code, and tests.  Configuration control shall begin 
  816. in the earliest stages of design and development and extend over the full 
  817. life of the CIs.  It involves not only the approval of changes and their 
  818. implementation but also the updat*ing of all related material to reflect 
  819. each change.  For example, often a change to one area of a verification 
  820. system may necessitate a change to an*other area.  It is not acceptable to 
  821. write or update documentation only for new code or newly modified code, 
  822. rather than for all parts of the verification sys*tem affected by the 
  823. addition or change.  Changes to all CIs shall be subject to review and 
  824. approval.
  825.  
  826.                 The configuration control process begins with the 
  827. documentation of a change request.  This change request should include 
  828. justification for the proposed change, all of the affected items and 
  829. documents, and the proposed solution.  The change request shall be 
  830. recorded in order to provide a way of tracking all proposed system changes 
  831. and to ensure against duplicate change requests being processed.
  832.  
  833.                 e.      Configuration accounting.
  834.  
  835.                 Configuration accounting shall yield information that can 
  836. be used to answer the following questions:  What source code changes were 
  837. made on a given date?  Was a given change absolutely necessary?  Why or 
  838. why not?  What were all the changes in a given CI between releases N and 
  839. N+1?  By whom were they made, and why?  What other modifications were 
  840. required by the changes to this CI?  Were modifications required in the 
  841. test set or documentation to accommodate any of these changes?  What were 
  842. all the changes made to support a given change request?
  843.  
  844.                 f.      Configuration auditing.
  845.  
  846.                 A configuration auditor shall be able to trace a system 
  847. change from start to finish.  The auditor shall check that only approved 
  848. changes have been implemented, and that all tests and documentation have 
  849. been updated concurrently with each implementation to reflect the current 
  850. status of the system.
  851.  
  852.                 g.      Configuration control board.
  853.  
  854.                 The vendor's Configuration Control Board (CCB) shall be 
  855. responsible for approving and disapproving change requests, prioritizing 
  856. approved modifications, and verifying that changes are properly 
  857. incorporated.  The members of the CCB shall interact periodically to 
  858. discuss configuration man*agement topics such as proposed changes, 
  859. configuration status accounting reports, and other topics that may be of 
  860. interest to the different areas of the system development.
  861.  
  862.  
  863.                    4.2.2        Support and Maintenance
  864.  
  865. The verification system shall have ongoing support and maintenance from 
  866. the developers or another qualified vendor.  Skilled maintainers are 
  867. necessary to make changes to the verification system.  
  868.  
  869.  
  870.                    4.2.3        Testing   
  871.  
  872.                 a.      Functional tests.
  873.  
  874.                 Functional tests shall be conducted to demonstrate that 
  875. the verification system operates as advertised.  These tests shall be 
  876. maintained over the life cycle of the verification system.  This ensures 
  877. that a test suite is available for use on all versions of the verification 
  878. system.  The test suite shall be enhanced as software errors are 
  879. identified to demonstrate the elimination of the errors in subsequent 
  880. versions.  Tests shall be done at the module level to demonstrate 
  881. compliance with design documentation and at the system level to 
  882. demonstrate that software accurately generates assertions, correctly 
  883. implements the logic, and correctly responds to user commands.  
  884.  
  885.                 b.      Stress testing.
  886.  
  887.                 The system shall undergo stress testing by the evaluation 
  888. team to test the limits of and to attempt to generate contradictions in 
  889. the specification language, the reasoning mechanism, and large 
  890. specifications.
  891.  
  892.  
  893.           4.3           DOCUMENTATION  
  894.  
  895.         a.      Configuration management plan.
  896.  
  897.         A configuration management plan and supporting evidence assuring a 
  898. consistent mapping of documentation and tools shall be provided for the 
  899. evaluation.  This provides the evaluators with evidence that compatibility 
  900. exists between the components of the verification system and its 
  901. documentation.  The plan shall include the following:
  902.  
  903.                 1.      The configuration management plan shall describe 
  904. what is to be done to implement configuration management in the 
  905. verification system.  It shall define the roles and responsibilities of 
  906. designers, developers, management, the Configuration Control Board, and 
  907. all of the personnel involved with any part of the life cycle of the 
  908. verification system.  
  909.  
  910.                 2.      Tools used for configuration management shall be 
  911. documented in the configuration management plan.  The forms used for 
  912. change control, conventions for labeling configuration items, etc., shall 
  913. be contained in the configuration management plan along with a description 
  914. of each.
  915.  
  916.                 3.      The plan shall describe procedures for how the 
  917. design and implementation of changes are proposed, evaluated, coordinated, 
  918. and approved or disapproved.  The configuration management plan shall also 
  919. include the steps to ensure that only those approved changes are actually 
  920. included and that the changes are included in all of the necessary areas.
  921.  
  922.                 4.      The configuration management plan shall describe 
  923. how changes are made to the plan itself and how emergency procedures are 
  924. handled.  It should describe the procedures for performing time-sensitive 
  925. changes without going through a full review process.  These procedures 
  926. shall define the steps for retroactively implementing configuration 
  927. management after the emergency change has been completed.
  928.  
  929.         b.      Configuration management evidence.
  930.  
  931.         Documentation of the configuration management activities shall be 
  932. provided to the evaluators.  This ensures that the policies of the 
  933. configuration management plan have been followed.
  934.  
  935.         c.      Source code.
  936.  
  937.         Well-documented source code for the verification system, as well 
  938. as documentation to aid in analysis of the code during the evaluation, 
  939. shall be provided.  This provides the evaluators with evidence that good 
  940. software engineering practices and configuration management procedures 
  941. were used in the implementation of the verification system.
  942.  
  943.         d.      Test documentation.
  944.  
  945.         Documentation of test suites and test procedures used to check 
  946. functionality of the system shall be provided.  This provides an 
  947. explanation to the evaluators of each test case, the testing methodology, 
  948. test results, and procedures for using the tests.
  949.  
  950.         e.      User's guide.
  951.  
  952.         An accurate and complete user's guide containing all available 
  953. commands and their usage shall be provided in a tutorial format.  The 
  954. user's guide shall contain worked examples.  This is necessary to guide 
  955. the users in the use of the verification system.
  956.  
  957.         f.      Reference manuals.
  958.  
  959.         A reference manual that contains instructions, error messages, and 
  960. examples of how to use the system shall be provided.  This provides the 
  961. users with a guide for problem-solving techniques as well as answers to 
  962. questions that may arise while using the verification system.
  963.  
  964.         g.      Facilities manual.
  965.  
  966.         A description of the major components of the software and their 
  967. interfacing shall be provided.  This will provide users with a limited 
  968. knowledge of the hardware base required to configure and use the 
  969. verification system.
  970.  
  971.         h.      Vendor report.
  972.  
  973.         A report written by the vendor during a reevaluation that provides 
  974. a complete description of the verification system and changes made since 
  975. the initial evaluation shall be provided.  This report, along with 
  976. configuration management documentation, provides the evaluators with 
  977. evidence that soundness of the system has not been jeopardized.
  978.  
  979.         i.      Significant worked examples.
  980.  
  981.         Significant worked examples shall be provided which demonstrate 
  982. the strengths, weaknesses, and limitations of the verification system.  
  983. These examples shall reflect portions of computing systems.  They may 
  984. reside in the user's guide, the reference manual, or a separate document.
  985.  
  986.  5.             FUTURE DIRECTIONS 
  987.  
  988.  
  989. The purpose of this section is to list possible features for future or 
  990. beyond-A1 verification systems.  Additionally, it contains possibilities 
  991. for future research -- areas that researchers may choose to investigate.  
  992. Research and development of new verification systems or investigating 
  993. areas not included in this list is also encouraged.  Note that the order 
  994. in which these items appear has no bearing on their relative importance.
  995.  
  996.         a.      The specification language should permit flexibility in 
  997. approaches to specification.
  998.  
  999.         b.      The specification language should allow the expression of 
  1000. properties involving liveness, concurrency, and eventuality.
  1001.  
  1002.         c.      The reasoning mechanism should include a method for 
  1003. reasoning about information flows.
  1004.  
  1005.         d.      The design and code of the verification system should be 
  1006. formally verified.
  1007.  
  1008.         e.      The theory should support rapid prototyping.  Rapid 
  1009. prototyping supports a way of developing a first, quick version of a 
  1010. specification.  The prototype provides immediate feedback to the user.
  1011.  
  1012.         f.      The verification system should make use of standard (or 
  1013. reusable) components where possible (for example, use of a standard 
  1014. windowing system, use of a standard language-independent parser, editor, 
  1015. or printer, use of a standard database support system, etc.).
  1016.  
  1017.         g.      The verification system should provide a language-specific 
  1018. verifier for a commonly used systems programming language.
  1019.  
  1020.         h.      The verification system should provide a method for 
  1021. mapping a top-level specification to verified source code.
  1022.  
  1023.         i.      The verification system should provide a tool for 
  1024. automatic test data generation of the design specification.
  1025.  
  1026.         j.      The verification system should provide a means of 
  1027. identifying which paths in the source code of the verification system are 
  1028. tested by a test suite.
  1029.  
  1030.         k.      The verification system should provide a facility for 
  1031. high-level debugging/tracing of unsuccessful proofs.
  1032.  
  1033.         l.      A formal justification of the methodology behind the 
  1034. verification system should be provided.
  1035.  
  1036.  APPENDIX
  1037.  
  1038. CONFIGURATION MANAGEMENT 
  1039.  
  1040.  
  1041. The purpose of configuration management is to ensure that changes made to 
  1042. verification systems take place in an identifiable and controlled 
  1043. environment.  Configuration managers take responsibility that additions, 
  1044. deletions, or changes made to the verification system do not jeopardize 
  1045. its ability to satisfy the requirements in Chapters 3 and 4.  Therefore, 
  1046. configuration management is vital to maintaining the endorsement of a 
  1047. verification system.
  1048.  
  1049. Additional information on configuration management can be found in A Guide 
  1050. to Understanding Configuration Management in Trusted Systems. [3]
  1051.  
  1052.  
  1053.  
  1054. OVERVIEW OF CONFIGURATION MANAGEMENT
  1055.  
  1056. Configuration management is a discipline applying technical and 
  1057. administrative direction to:  1) identify and document the functional and 
  1058. physical characteristics of each configuration item for the system; 2) 
  1059. manage all changes to these characteristics; and 3) record and report the 
  1060. status of change processing and implementation.  Configuration management 
  1061. involves process monitoring, version control, information capture, quality 
  1062. control, bookkeeping, and an organizational framework to support these 
  1063. activities.  The configuration being managed is the verification system 
  1064. plus all tools and documentation related to the configuration process.
  1065.  
  1066. Four major aspects of configuration management are configuration 
  1067. identification, configuration control, configuration status accounting, 
  1068. and configuration auditing.  
  1069.  
  1070.  
  1071.  
  1072. CONFIGURATION IDENTIFICATION
  1073.  
  1074. Configuration management entails decomposing the verification system into 
  1075. identifi*able, understandable, manageable, trackable units known as 
  1076. Configuration Items (CIs).  A CI is a uniquely identifiable subset of the 
  1077. system that represents the small*est portion to be subject to independent 
  1078. configuration control procedures.  The decomposition process of a 
  1079. verification system into CIs is called configuration identification.  
  1080.  
  1081. CIs can vary widely in size, type, and complexity.  Although there are no 
  1082. hard-and-fast rules for decomposition, the granularity of CIs can have 
  1083. great practical importance.  A favorable strategy is to designate 
  1084. relatively large CIs for elements that are not expected to change over the 
  1085. life of the system, and small CIs for elements likely to change more 
  1086. frequently.  
  1087.  
  1088.  
  1089.  
  1090. CONFIGURATION CONTROL
  1091.  
  1092. Configuration control is a means of assuring that system changes are 
  1093. approved before being implemented, only the proposed and approved changes 
  1094. are implemented, and the implementation is complete and accurate.  This 
  1095. involves strict procedures for proposing, monitoring, and approving system 
  1096. changes and their implementation.  Configuration control entails central 
  1097. direction of the change process by personnel who coordinate analytical 
  1098. tasks, approve system changes, review the implementation of changes, and 
  1099. supervise other tasks such as documentation.
  1100.  
  1101.  
  1102.  
  1103. CONFIGURATION ACCOUNTING
  1104.  
  1105. Configuration accounting documents the status of configuration control 
  1106. activities and in general provides the information needed to manage a 
  1107. configuration effectively.  It allows managers to trace system changes and 
  1108. establish the history of any developmental problems and associated fixes.  
  1109. Configuration accounting also tracks the status of current changes as they 
  1110. move through the configuration control process.  Configuration accounting 
  1111. establishes the granularity of recorded information and thus shapes the 
  1112. accuracy and usefulness of the audit function.
  1113.  
  1114. The accounting function must be able to locate all possible versions of a 
  1115. CI and all of the incremental changes involved, thereby deriving the 
  1116. status of that CI at any specific time.  The associated records must 
  1117. include commentary about the reason for each change and its major 
  1118. implications for the verification system.
  1119.  
  1120.  
  1121.  
  1122. CONFIGURATION AUDIT
  1123.  
  1124. Configuration audit is the quality assurance component of configuration 
  1125. management.  It involves periodic checks to determine the consistency and 
  1126. completeness of accounting information and to verify that all 
  1127. configuration management policies are being followed.  A vendor's 
  1128. configuration management program must be able to sustain a complete 
  1129. configuration audit by an NCSC review team.
  1130.  
  1131.  
  1132.  
  1133. CONFIGURATION MANAGEMENT PLAN
  1134.  
  1135. Strict adherence to a comprehensive configuration management plan is one 
  1136. of the most important requirements for successful configuration 
  1137. management.  The configuration management plan is the vendor's document 
  1138. tailored to the company's practices and personnel.  The plan accurately 
  1139. describes what the vendor is doing to the system at each moment and what 
  1140. evidence is being recorded.  
  1141.  
  1142.  
  1143.  
  1144. CONFIGURATION CONTROL BOARD
  1145.  
  1146. All analytical and design tasks are conducted under the direction of the 
  1147. vendor's corporate entity called the Configuration Control Board (CCB).  
  1148. The CCB is headed by a chairperson who is responsible for assuring that 
  1149. changes made do not jeopardize the soundness of the verification system.  
  1150. The Chairperson assures that the changes made are approved, tested, 
  1151. documented, and implemented correctly.  
  1152.  
  1153. The members of the CCB should interact periodically, either through formal 
  1154. meetings or other available means, to discuss configuration management 
  1155. topics such as proposed changes, configuration status accounting reports, 
  1156. and other topics that may be of interest to the different areas of the 
  1157. system development.  These interactions should be held to keep the entire 
  1158. system team updated on all advancements or alterations in the verification 
  1159. system.
  1160.  
  1161.  GLOSSARY 
  1162.  
  1163.  
  1164.  
  1165. Beta Version 
  1166.  
  1167.                 Beta versions are intermediate releases of a product to be 
  1168. tested at one or more customer sites by the software end-user.  The 
  1169. customer describes in detail any problems encountered during testing to 
  1170. the developer, who makes the appropriate modifications.  Beta versions are 
  1171. not endorsed by the NCSC, but are primarily used for debugging and testing 
  1172. prior to submission for endorsement.
  1173.  
  1174. Complete
  1175.  
  1176.                 A theory is complete if and only if every sentence of its 
  1177. language is either provable or refutable.
  1178.  
  1179. Concurrency 
  1180.  
  1181.                 Simultaneous or parallel processing of events.
  1182.  
  1183. Configuration Accounting 
  1184.  
  1185.                 The recording and reporting of configuration item 
  1186. descriptions and all departures from the baseline during design and 
  1187. production.
  1188.  
  1189. Configuration Audit 
  1190.  
  1191.                 An independent review of computer software for the purpose 
  1192. of assessing compliance with established requirements, standards, and 
  1193. baselines. [3]
  1194.  
  1195. Configuration Control 
  1196.  
  1197.                 The process of controlling modifications to the system's 
  1198. design, hardware, firmware, software, and documentation which provides 
  1199. sufficient assurance that the system is protected against the introduction 
  1200. of improper modification prior to, during, and after system 
  1201. implementation. [3]
  1202.  
  1203. Configuration Control Board (CCB) 
  1204.  
  1205.                 An established vendor committee that is the final 
  1206. authority on all proposed changes to the verification system.
  1207.  
  1208. Configuration Identification 
  1209.  
  1210.                 The identifying of the system configuration throughout the 
  1211. design, development, test, and production tasks. [3]
  1212.  
  1213. Configuration Item (CI) 
  1214.  
  1215.                 The smallest component tracked by the configuration 
  1216. management system. [3]
  1217.  
  1218. Configuration Management 
  1219.  
  1220.                 The process of controlling modifications to a verification 
  1221. system, including documentation, that provides sufficient assurance that 
  1222. the system is protected against the introduction of improper modification 
  1223. before, during, and after system implementation.  
  1224.  
  1225. Conjecture 
  1226.  
  1227.                 A general conclusion proposed to be proved upon the basis 
  1228. of certain given premises or assumptions.
  1229.  
  1230. Consistency (Mathematical) 
  1231.  
  1232.                 A logical theory is consistent if it contains no formula 
  1233. such that the formula and its negation are provable theorems.
  1234.  
  1235. Consistency (Methodological)
  1236.  
  1237.                 Steadfast adherence to the same principles, course, form, 
  1238. etc.
  1239.  
  1240. Correctness 
  1241.  
  1242.                 Free from errors; conforming to fact or truth.
  1243.  
  1244. Correctness Conditions 
  1245.  
  1246.                 Conjectures that formalize the rules, security policies, 
  1247. models, or other critical requirements on a system.
  1248.  
  1249. Design Verification 
  1250.  
  1251.                 A demonstration that a formal specification of a software 
  1252. system satisfies the correctness conditions (critical requirements 
  1253. specification).
  1254.  
  1255. Documentation 
  1256.  
  1257.                 A set of manuals and technical papers that fully describe 
  1258. the verification system, its components, application, and operation.
  1259.  
  1260. Endorsed Tools List (ETL) 
  1261.  
  1262.                 A list composed of those verification systems currently 
  1263. recommended by the NCSC for use in developing highly trusted systems.
  1264.  
  1265. Eventuality 
  1266.  
  1267.                 The ability to prove that at some time in the future, a 
  1268. particular event will occur.
  1269.  
  1270. Formal Justification 
  1271.  
  1272.                 Mathematically precise evidence that the methodology of 
  1273. the verification system is sound.
  1274.  
  1275. Formal Verification 
  1276.  
  1277.                 The process of using formal proofs to demonstrate the 
  1278. consistency (design verification) between a formal specification of a 
  1279. system and a formal security policy model or (implementation verification) 
  1280. between the formal specification and its program implementation. [1]
  1281.  
  1282. Implementation Verification 
  1283.  
  1284.                 A demonstration that a program implementation satisfies a 
  1285. formal specification of a system.
  1286.  
  1287. Informal Justification 
  1288.  
  1289.                 An English description of the tools of a verification 
  1290. system and how they interact.  This includes a justification of the 
  1291. soundness of the theory.
  1292.  
  1293. Language 
  1294.  
  1295.                 A set of symbols and rules of syntax regulating the 
  1296. relationship between the symbols, used to convey information.
  1297.  
  1298. Liveness 
  1299.  
  1300.                 Formalizations that ensure that a system does something 
  1301. that it should do.
  1302.  
  1303. Metalogic 
  1304.  
  1305.                 A type of logic used to describe another type of logic or 
  1306. a combination of different types of logic.
  1307.  
  1308. Methodology 
  1309.  
  1310.                 The underlying principles and rules of organization of a 
  1311. verification system.
  1312.  
  1313. Production Quality Verification System 
  1314.  
  1315.                 A verification system that is sound, user-friendly, 
  1316. efficient, robust, well-documented, maintainable, well-engineered 
  1317. (developed with software engineering techniques), available on a variety 
  1318. of hardware, and promoted (has education available for users). [2]
  1319.  
  1320. Proof 
  1321.  
  1322.                 A syntactic analysis performed to validate the truth of an 
  1323. assertion relative to an (assumed) base of assertions.
  1324.  
  1325. Proof Checker 
  1326.  
  1327.                 A tool that 1) accepts as input an assertion (called a 
  1328. conjecture), a set of assertions (called assumptions), and a proof; 2) 
  1329. terminates and outputs either success or failure; and 3) if it succeeds, 
  1330. then the conjecture is a valid consequence of the assumptions.
  1331.  
  1332. Reasoning Mechanism 
  1333.  
  1334.                 A tool (interactive or fully automated) capable of 
  1335. checking or constructing proofs.
  1336.  
  1337. Safety Properties 
  1338.  
  1339.                 Formalizations that ensure that a system does not do 
  1340. something that it should not do.
  1341.  
  1342. Semantics 
  1343.  
  1344.                 A set of rules for interpreting the symbols and 
  1345. well-formed formulae of a language.
  1346.  
  1347. Sound 
  1348.  
  1349.                 An argument is sound if all of its propositions are true 
  1350. and its argument form is valid.  A proof system is sound relative to a 
  1351. given semantics if every conjecture that can be proved is a valid 
  1352. consequence of the assumptions used in the proof.
  1353.  
  1354. Specification Language 
  1355.  
  1356.                 A logically precise language used to describe the 
  1357. structure or behavior of a system to be verified.
  1358.  
  1359. Specification Processor 
  1360.  
  1361.                 A software tool capable of receiving input, parsing it, 
  1362. generating conjectures (candidate theorems), and supplying results for 
  1363. further analysis (e.g., reasoning mechanism).
  1364.  
  1365. Syntax 
  1366.  
  1367.                 A set of rules for constructing sequences of symbols from 
  1368. the primitive symbols of a language.
  1369.  
  1370. Technical Assessment Report (TAR) 
  1371.  
  1372.                 A report that is written by an evaluation team during an 
  1373. evaluation of a verification system and available upon completion.
  1374.  
  1375. Theorem 
  1376.  
  1377.                 In a given logical system, a well-formed formula that is 
  1378. proven in that system.
  1379.  
  1380. Theory 
  1381.  
  1382.                 A formal theory is a coherent group of general 
  1383. propositions used as principles of explanation for a particular class of 
  1384. phenomena.
  1385.  
  1386. User-Friendly 
  1387.  
  1388.                 A system is user-friendly if it facilitates learning and 
  1389. usage in an efficient manner.
  1390.  
  1391. Valid 
  1392.  
  1393.                 An argument is valid when the conclusion is a valid 
  1394. consequence of the assumptions used in the argument.
  1395.  
  1396. Vendor Report (VR) 
  1397.  
  1398.                 A report that is written by a vendor during and available 
  1399. upon completion of a reevaluation of a verification system.
  1400.  
  1401. Verification 
  1402.  
  1403.                 The process of comparing two levels of system 
  1404. specification for proper correspondence (e.g., security policy model with 
  1405. top-level specification, top-level specification with source code, or 
  1406. source code with object code).  This process may or may not be automated. 
  1407. [1]
  1408.  
  1409. Verification Committee 
  1410.  
  1411.                 A standing committee responsible for the management of the 
  1412. verification efforts at the NCSC.  The committee is chaired by the NCSC 
  1413. Deputy Director and includes the NCSC Chief Scientist, as well as 
  1414. representatives from both the NCSC's Office of Research and Development 
  1415. and Office of Computer Security Evaluations, Publications, and Support.
  1416.  
  1417. Verification System 
  1418.  
  1419.                 An integrated set of tools and techniques for performing 
  1420. verification.
  1421.  
  1422. Well-Formed Formula 
  1423.  
  1424.                 A sequence of symbols from a language that is constructed 
  1425. in accordance with the syntax for that language.
  1426.  
  1427.  
  1428.  
  1429.  BIBLIOGRAPHY 
  1430.  
  1431.  
  1432. [1]             Department of Defense, Department of Defense Trusted 
  1433. Computer System Evaluation Criteria, DOD 5200.28-STD, December 1985.  
  1434.  
  1435. [2]             Kemmerer, Richard A., Verification Assessment Study Final 
  1436. Report, University of California, March 1986.
  1437.  
  1438. [3]             National Computer Security Center, A Guide to 
  1439. Understanding Configuration Management in Trusted Systems, NCSC-TG-006, 
  1440. March 1988.
  1441.  
  1442. [4]             National Computer Security Center, Trusted Network 
  1443. Interpretation of the Trusted Computer System Evaluation Criteria, 
  1444. NCSC-TG-005, July 1987.
  1445.  
  1446. [5]             National Security Agency, Information Systems Security 
  1447. Products and Services Catalogue, Issued Quarterly, January 1989 and 
  1448. successors.
  1449.  
  1450.  
  1451.  
  1452.  
  1453.  
  1454.  
  1455.  
  1456.  
  1457.  
  1458.  
  1459.  
  1460.