Computer systems that earn a high degree of trust must be backed by rigorous verification methods. A verification system is an interactive environment for writing formal specifications and checking formal proofs. Verification systems allow large complicated proofs to be managed and checked interactively. We desire evaluation criteria that provide a means of finding which verification system is suitable for a specific research environment and what needs of a particular project the tool satisfies. Therefore, the purpose of this thesis is to develop a methodology and set of evaluation criteria to evaluate verification systems for their suitability to improve the assurance that systems meet security objectives. A specific verification system is evaluated with respect to the defined methodology. The main goals are to evaluate whether the verification system has the capability to express the properties of software systems and to evaluate whether the verification system can provide inter-level mapping, a feature required for understanding how a system meets security objectives. / Naval Postgraduate School author (civilian).
| Identifer | oai:union.ndltd.org:nps.edu/oai:calhoun.nps.edu:10945/893 |
| Date | 06 1900 |
| Creators | Ubhayakar, Sonali S. |
| Contributors | Dinolt, George, Levin, Timothy, Computer Science |
| Publisher | Monterey, California. Naval Postgraduate School |
| Source Sets | Naval Postgraduate School |
| Detected Language | English |
| Type | Thesis |
| Format | xviii, 139 p. : ill. (some col.) ;, application/pdf |
| Rights | This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. As such, it is in the public domain, and under the provisions of Title 17, United States Code, Section 105, may not be copyrighted. |
Page generated in 0.0019 seconds