Software Correctness Verification:

Principal Investigator: Mark Pleszkoch

Problem Addressed

Software containing errors and vulnerabilities cannot be trustworthy or secure. Yet despite best efforts, software is often developed and delivered with incorrect and even unknown behavior. In the current state of practice, no practical means exists for automation support of large-scale correctness verification of software with respect to intended behavior. As a result, much time and energy is devoted to inspection and testing activities that can provide only limited evidence of correctness.

Research Approach

The objective of this potential project is to develop a prototype function verification system that will help users to check the correctness of programs based on their actual computed behavior. The system will employ the mathematics-based foundations of function extraction to achieve completeness and correctness of results, but the user will not be exposed to, or required to know, these foundations. The system will provide a proof of concept for function verification technology and a foundation for elaboration into industrial-strength verification systems. In addition, the system will provide a standard, machine-processable form for representing intended behavior. Users will be able to code programs to satisfy intended behavior and execute the system to check correctness.

Function extraction and function verification are closely related. Functional correctness verification requires computing the as-built functional behaviors of program structures, just as in the function extraction process, and then comparing those behaviors to intended behaviors for equivalence or not. As noted, the function-theoretic model of software treats programs as rules for mathematical functions or relations—that is, mappings from domains to ranges. While programs can contain an intractable number of execution paths, they are at the same time composed of a finite number of control structures, each of which implements a mathematical function or relation in the transformation of its inputs into outputs. A theorem defines the mapping of these control structures into procedure-free functional form [1,2]. These mappings are the starting point for the function extraction process and its application to correctness verification.

Expected Benefits

Large-scale software assurance requires a commensurate scale of engineering automation. This project can provide substantial benefits to sponsors who must deal with software failures and vulnerabilities in enterprise operations. It is difficult to achieve trustworthiness and security goals for systems without knowing whether they are correct with respect to intended behavior. Routine availability of functional verification can substantially reduce errors, vulnerabilities, and malicious code in software. FX-based verification technology can replace much of the labor-intensive and error-prone work of program inspection and testing, with corresponding reductions in resource requirements and improvements in product quality [3].

2007 Accomplishments

The function extraction system currently under development provides a foundation for implementing correctness verification capabilities.

2008 Plans

STAR*Lab is ready to extend FX technology for automation of correctness verification for interested sponsors.

References

[2] Mills, H. & Linger, R. “Cleanroom Software Engineering.” Encyclopedia of Software Engineering, 2nd ed. (J. Marciniak, ed.). New York, NY: John Wiley & Sons, 2002.

[3] Hevner, A.; Linger, R.; Collins, R.; Pleszkoch, M.; Prowell, S.; & Walton, G. The Impact of Function Extraction Technology on Next-Generation Software Engineering (CMU/SEI-2005-TR- 015). Pittsburgh, PA: Software Engineering Institute, Carnegie Mellon University, 2005. http://www.sei.cmu.edu/publications/documents/05.reports/05tr015.html.