AI helps you reading Science
AI generates interpretation videos
AI extracts and analyses the key points of the paper to generate videos automatically
AI parses the academic lineage of this thesis
AI extracts a summary of this paper
We have developed a denotational definition of a programming language semantics more regular than Ada’s, and argue informally that - subject to certain hypotheses - observable properties provable of this regular semantics are true of Ada
Formal Methods and Software Engineering
The use of software engineering tools based on formal methods requires an investment not required by traditional methods, but results in more reliable software systems. Assumptions about system behavior are made explicit, and high-level specifications provide unambiguous descriptions of component properties. A formal basis enables automat...More
PPT (Upload PPT)
- The production of software is evolving into a more systematic and scientific discipline.
- The Romulus tool allows the user to specify and verify security properties at the system design level.
- The Penelope specification system is sufficientlyflexible that the authors can use it for design level specificationwith target languages other than Ada. The authors are currently performing a task on behalf of NASA in which the authors specify flight software implementing the Control Mode Panel Logic of the research aircraft (TSRV) of the Advanced Transport Operating System (ATOPS) Program at Langley Research Center.
- The production of software is evolving into a more systematic and scientific discipline
- There are a number of different ways in which formal methods are applied to software engineering
- We are able to prove in a formal proof system that the program satisfies its specification
- We have developed a denotational definition of a programming language semantics more regular than Ada’s, and argue informally that - subject to certain hypotheses - observable properties provable of this regular semantics are true of Ada
- The Romulus environment supports the modeling of secure systems by providing a graphical user interface which allows the user to input a graphical description of system structure which breaks the system into a set of components
- Once a system design has been expressed in Romulus, the user invokes both automatic and interactive theorem proving tools to verify that the design is secure
- Ariel is an RADC sponsored system designed to prove correctness of programs written in a subset of C which includes real arithmetic and some UNIX systems c d s for 1/0 and exception handling.
- It is designed to verify mathematical software, that is, programs which use machine real arithmetic.
- Ariel’s semantic verification works by generating a mathematical description of the possible sequences of states that a program can pass through during execution.
- ORA’S Romulus computer security properties modeling environment is a collectionof tools to assist the user in the development of models of secure computer systems and in formally verifying that these systems are secure.
- The Romulus environment supports the modeling of secure systems by providing a graphical user interface which allows the user to input a graphical description of system structure which breaks the system into a set of components.
- Once a system design has been expressed in Romulus, the user invokes both automatic and interactive theorem proving tools to verify that the design is secure.
- The authors will code the SEM in Ada and will use Penelope, the Ada-based formal specification and verification system described in Section 3, to show that this code implements its design.
- The mandatory policy is based on the formal theory of security developed at ORA, and uses a composable multilevel security property defined within that theory.
- The key problem overcome in this verification is that a formal property such as restriction, which involves quantification over alternate possible execution histories of a component, cannot be expressed as embedded assertions in a language such as Gypsy, that expresses predicates on states in an actual execution history.
- A technique was developed  to formally verify restriction in two steps: e security-relevant embedded assertions were generated for the Gypsy design, and mechanical proofs of these were carried out in Gypsy; e metatheorems were proved to show that the generated assertions imply that the design is restrictive.
- THETA (a Trusted HETerogeneousArchitecture, formerly called SDOS) is a multilevel secure distributed operating system under development a t ORA  The THETA project is being sponsored by RADC
- J.S. Crow et al. EHDM verification environment: An overview. In Proceedings of the 11th National Computer Security Conference, 1988.
- David Guaspari. Penelope, an Ada verification system. In Proceedings of Di-Ada '89, pages 216-224, Pittsburgh, PA, October 1989. original number was 17-16.
- J. V. Guttag, J. J. Horning, and J. M. Wing. Larch in five easy pieces. Technical Report TR 5, DEC/SRC, July 1985.
- R. Locasso et al. The Ina Jo specification language reference manual. Technical Report TM-(L)6021/001/00, System Development Corporation, June 1980.
- L.G. Marcus and J.V. Cook. SDVS user's manual. Technical Report ATR-84(8478)-1, Aerospace Corporation, El Segundo, Calif. 90245, November 1984.
- Daryl McCullough. Foundations of Ulysses: The theory of security. Technical Report RADC-TR-87-222, Rome Air Development Center, May 1988. original number was 11-12.
- D. G. Weber and Roger L. Costello. Beyond A1 using Ada code verification. Technical Report 89-9, Odyssey Research Associates, April 1989. original number was 17-7.
- D. G. Weber and Robert S. Lubarsky. The SDOS project - Verifying hook-up security. In Pmceedings of Third Aerospace Computer Security Conference, pages 7-15, Orlando, FL, December 1987. AIAA/ASIS/IEEE. original number was 12-1.
- Raymond M. Wong et al. The SDOS system: A secure distributed operating system prototype. In Proceedings of the f 2 t h National Computer Security Conference, pages 172-183, Baltimore, MD, October 1989.