Trustworthy and Composable Software Systems with Contracts - UMD - April 2015
Public Audience
Purpose: To highlight project progress. Information is generally at a higher level which is accessible to the interested public. All information contained in the report (regions 1-3) is a Government Deliverable/CDRL.
PI(s): David Van Horn (UMD), Jeffrey Foster (UMD), Michael Hicks (UMD), Sam Tobin-Hochstadt (Indiana)
Researchers: Phuc C. Nguyen (UMD), Nicholas Labich (UMD), Andrew Kent (Indiana)
Fundamental research:
Modern software systems are composed of large sets of interacting components constructed in a variety of programming languages that provide varying degrees of assurance that the components are well-behaved. Ill-defined program behaviors such as buffer overruns, code injection, and race conditions are the keystone of most security vulnerabilities and system failures.
This research project aims to investigate compositional verification techniques using language-based mechanisms for specifying and enforcing program properties called contracts. Initial results (ICFP'14, PLDI'15) confirm that behavioral properties of programs can be verified using this approach and we hypothesize that the approach scales to cover multi-language programs and security properties.
We have recently made a theoretical breakthrough showing how to generate counterexamples that witness contract violations. This is important for testing and debugging software that uses contracts. We have proved that our method is both "sound" and "relatively complete," which means the approach is powerful and capable of generating a large class of counterexamples. These results have been accepted to appear at PLDI'15. Our software artifact is currently under review as part of the artifact evaluation process at PLDI'15. Our ICFP'14 was invited to submit the "best of" special issue of the Journal of Functional Programming devoted to ICFP'14.
Community Interaction:
Our initial results providing a foundation for contract verification have been presented at the National Institute of Informatics (NII), Japan special meeting on "Software Contracts for Communication, Monitoring, and Security" and the Schloss Dagstuhl, Germany seminar on "Scripting Languages and Frameworks: Analysis and Verification". In September, we presented the results at the ACM SIGPLAN Internation Conference on Functional Programming, one of the premier publication venues for programming language research.
We have launched an interactive web service for experimenting with the system at http://scv.umiacs.umd.edu/. We have advertised the service widely to the PL community.
Educational:
We have given tutorials on the formal method tools and techniques used to develop the system in the hopes of advancing the best practices used to develop high-assurance software. Van Horn has been invited to lecture on the methods at a graduate summer school hosted by the University of Utah in July, 2014. The presentation of the ICFP 2014 paper was recorded and made available on YouTube; it has been circulated among the programming language community. The content of that research has been incorporated into the UMD graduate class "Program Analysis and Understanding". It was also presented to the undergraduate honors seminar in October. We continue to develop our tool in the pedagogically oriented programming environment accompanying the textbook "How to Design Programs". We are investigating a web interface for the system so that users can experiment with the system without needing to install specialized software. Our prototype is now available online.
HARD PROBLEM(S) ADDRESSED
This refers to Hard Problems, released November 2012.
Scalability and Composability
PUBLICATIONS
Papers published in this quarter as a result of this research. Include title, author(s), venue published/presented, and a short description or abstract. Identify which hard problem(s) the publication addressed. Papers that have not yet been published should be reported in region 2 below.
Relatively Complete Counterexamples for Higher-Order Programs, Phuc C. Nguyen and David Van Horn, Proceedings of the the 36th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, Oregon, June 2015.
In this paper, we study the problem of generating inputs to a higher-order program causing it to error. We first study the problem in the setting of PCF, a typed, core functional language and contribute the first relatively complete method for constructing counterexamples for PCF programs. The method is relatively complete in the sense of Hoare logic; completeness is reduced to the completeness of a first-order solver over the base types of PCF. In practice, this means an SMT solver can be used for the effective, automated generation of higher-order counterexamples for a large class of programs.
We achieve this result by employing a novel form of symbolic execution for higher-order programs. The remarkable aspect of this symbolic execution is that even though symbolic higher-order inputs and values are considered, the path condition remains a first-order formula. Our handling of symbolic function application enables the reconstruction of higher-order counterexamples from this first-order formula.
After establishing our main theoretical results, we sketch how to apply the approach to untyped, higher-order, stateful languages with first-class contracts and show how counterexample generation can be used to detect contract violations in this setting. To validate our approach, we implement a tool generating counterexamples for erroneous modules written in Racket.
This paper addresses the hard problem of Scalability and Composability.
ACCOMPLISHMENT HIGHLIGHTS
- Develeped a foundational theory of contract verification
- Proved our approach "sound": software verified by the approach is provably free of contract violations
- Proved our approach "relatively complete": the approach verifies a large, well-defined class of programs
- Built and evaluated an implementation based on our theoretical results
- Made a web service of our tool available.