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
This Brief includes a Technical Support Package (TSP).
Infrastructure for Development of Secure, Reliable Software
(reference AFRL-0096) is currently available for download from the TSP library.
Don't have an account? Sign up here.
Top Stories
INSIDERManned Systems
Turkey's KAAN Combat Aircraft Completes First Flight - Mobility Engineering...
INSIDERMaterials
FAA Expands Boeing 737 Investigation to Manufacturing and Production Lines -...
INSIDERImaging
New Video Card Enables Supersonic Vision System for NASA's X-59 Demonstrator -...
INSIDERManned Systems
Stratolaunch Approaches Hypersonic Speed in First Powered TA-1 Test Flight -...
INSIDERUnmanned Systems
Army Ends Future Attack and Reconnaissance Helicopter Development Program -...
ArticlesEnergy
Can Solid-State Batteries Commercialize by 2030? - Mobility Engineering...
Webcasts
AR/AI
From Data to Decision: How AI Enhances Warfighter Readiness
Energy
April Battery & Electrification Summit
Manufacturing & Prototyping
Tech Update: 3D Printing for Transportation in 2024
Test & Measurement
Building an Automotive EMC Test Plan
Manufacturing & Prototyping
The Moon and Beyond from a Thermal Perspective
Software
Mastering Software Complexity in Automotive: Is Release Possible...