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