AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
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

(2013)

Cited: 0|Views8
Full Text
Bibtex
Weibo

Abstract

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

Code:

Data:

Introduction
  • 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.
Highlights
  • 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
Results
  • 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.
Conclusion
  • 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 [8] 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.
Funding
  • THETA (a Trusted HETerogeneousArchitecture, formerly called SDOS) is a multilevel secure distributed operating system under development a t ORA [9] The THETA project is being sponsored by RADC
Reference
  • J.S. Crow et al. EHDM verification environment: An overview. In Proceedings of the 11th National Computer Security Conference, 1988.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • J. V. Guttag, J. J. Horning, and J. M. Wing. Larch in five easy pieces. Technical Report TR 5, DEC/SRC, July 1985.
    Google ScholarFindings
  • R. Locasso et al. The Ina Jo specification language reference manual. Technical Report TM-(L)6021/001/00, System Development Corporation, June 1980.
    Google ScholarFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarFindings
  • 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.
    Google ScholarLocate open access versionFindings
  • 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.
    Google ScholarLocate open access versionFindings
0
Your rating :

No Ratings

Tags
Comments
数据免责声明
页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果,我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问,可以通过电子邮件方式联系我们:report@aminer.cn