Trustworthy and Composable Software Systems with Contracts - UMD - October 2015

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.

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 2014, we presented results at the ACM SIGPLAN International Conference on Functional Programming; in June 2015, we presented results at the ACM SIGPLAN International Conference of Programming Language Design and Implementation. Both are premier publication venues for programming language research.  We have submitted to a special issue of the Journal of Functional Programming (by invitation) to contain the best papers of ICFP'14 (currently under review).

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, 2015. 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. In January 2016, Van Horn will present the tutorial on this material at POPL.

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. 

HARD PROBLEM(S) ADDRESSED

Scalability and Composability

PUBLICATIONS
None this quarter.

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