MOBILITY ENGINEERING Produced by SAE Media Group
MOBILITY ENGINEERING
Magazines
Magazine cover

Current Issue

Archives

Magazine cover

Current Issue

Archives

Magazine cover

Current Issue

Archives

Magazine cover

Current Issue

Archives

Infrastructure for Development of Secure, Reliable Software

Complex software systems are made secure and correct by construction.

The Verification and Automated Reasoning research group at Cornell University has been building an infrastructure, comprising human expertise and computational resources, for the development of secure, reliable software for critical military applications. Such software includes distributed real-time embedded software systems, which are inherently complex and difficult to understand and specify. The infrastructure includes both efficient means of constructing the software and mathematically rigorous means of ensuring that the software will be secure and correct by construction.

The continuing work of the Verification and Automated Reasoning research group includes the development of formal methods and software tools for design, implementation, verification, and optimization of software systems. To provide a basis for efficient and practical correct-by-construction and secure-by-construction distributed programming, the group has developed a prototype logical programming environment (LPE) that includes an extensive collection of automated reasoning software tools.

A key component of the LPE is a digital library of formal algorithmic knowledge. The library contains vast amounts of highly structured mathematical knowledge and enables researchers and programmers to search for knowledge that is relevant to the development of specific software systems. The information in the library is organized logically in such a way as to make it useable and to enable sharing of the information among researchers and programmers involved in creating hardware and software that are more reliable than they otherwise would be. The library also includes logical accounting mechanisms to enforce the highest standards of correctness and accuracy while enabling researchers to contribute new formal algorithmic knowledge to the library.

The infrastructure also includes computing hardware. Because of the huge search spaces and high processing demands of the formal reasoning software tools of the LPE, many processors and large amounts of memory are necessary for using these tools efficiently in state-of-the-art applications. Processors are also needed to make the LPE accessible to remote users via the Internet. The hardware portion of the infrastructure includes the following:

  • An internal cluster of 32 processors having a total of 68GB of random-access memory (RAM) and a file-system capacity of 1,200GB;
  • A Web cluster of 12 dual-core processors having a total of 44GB of RAM and a file-system capacity of 900GB;
  • More than a dozen assorted computer workstations and associated equipment that includes a projector and several printers.

This assortment of hardware enables several researchers to perform heavy-duty theorem-proving tasks simultaneously while enabling remote users to browse, search, combine, and add formal material to the knowledge base.

This work was done by Robert Constable, Christoph Kreitz, Bart Selman, Stuart Allen, Richard Eaton, Lori Lorigo, Wojciech Moczydlowski, Evan Moran, and Radhika Lakshmanan of Cornell University for the Air Force Research Laboratory.

AFRL-0096

Topics:
Computer software and hardware Cybersecurity Data acquisition and handling Defense industry Embedded software Information Technology Internet Real-time data Research and development Telecommunications
This Brief includes a Technical Support Package (TSP).
Document cover
Infrastructure for Development of Secure, Reliable Software

(reference AFRL-0096) is currently available for download from the TSP library.

Don't have an account?

More From SAE Media Group

    Magazine cover
    Defense Tech Briefs Magazine

    This article first appeared in the February, 2009 issue of Defense Tech Briefs Magazine (Vol. 3 No. 1).

    Read more articles from this issue here.

    Read more articles from the archives here.

    Overview

    The document titled "A Computation Infrastructure for Knowledge-based Development of Reliable Software Systems" presents a final report by Robert Constable and Christoph Kreitz from Cornell University, detailing their research efforts in enhancing the reliability of software systems, particularly for Department of Defense (DoD) applications. The report emphasizes the challenges associated with developing reliable and secure distributed real-time embedded software systems, which are crucial for military capabilities. These systems are inherently complex, making them difficult to specify and understand, often leading to costly design flaws that are discovered late in the development process.

    To address these challenges, the research group employs formal methods, theorem proving, and knowledge management techniques. Their goal is to create formal logical tools that can effectively tackle complex DoD tasks and support the development of safety-critical software. The report outlines the development of a prototype Logical Programming Environment and a Formal Digital Library, which are designed to facilitate formal reasoning and verification of software systems.

    The infrastructure funded by the Air Force Office of Scientific Research (AFOSR) grant has enabled the team to conduct heavy-duty theorem proving tasks with multiple proof engines, model checkers, and SAT solvers operating simultaneously. This capability requires substantial computational resources, including a large number of processors and significant memory, to run efficiently in state-of-the-art applications.

    The report highlights the importance of making formalized algorithmic knowledge and logical software development tools accessible to researchers and programmers. It also discusses the automated support provided for training individuals in the systematic design of reliable software. The research instrumentation described in the report has significantly contributed to the DoD mission by making system verification research feasible and opening the proof system to remote users.

    In summary, the document outlines a comprehensive approach to improving the reliability of software systems through advanced computational infrastructure and formal methods, addressing the critical needs of the DoD while also providing a framework for training and knowledge dissemination in the field of software development.

    Top Stories

    INSIDERLighting Technology

    Feature Image Using Ultrabright X-Rays to Test Materials for Ultrafast Aircraft

    INSIDERManufacturing & Prototyping

    Feature Image New 3D-Printable Nanocomposite Prevents Overheating in Military Electronics

    INSIDERDefense

    Feature Image F-22 Pilot Controls Drone With Tablet

    Technology ReportAR/AI

    Feature Image Talking SDVs and Zonal Architecture with TE Connectivity

    INSIDERManufacturing & Prototyping

    Feature Image New Defense Department Program Seeks 300,000 Drones From Industry by 2027

    INSIDERAerospace

    Feature Image Anduril Completes First Semi-Autonomous Flight of CCA Prototype

    Webcasts