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.