Trustworthy and Composable Software Systems with Contracts - UMD - January 2017

PI(s): David Van Horn (UMD), Jeffrey Foster (UMD), Michael Hicks (UMD), Sam Tobin-Hochstadt (Indiana)
Researchers: Phuc C. Nguyen (UMD), Nicholas Labich (UMD), David Darais (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 also 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.  We are currently working on the significant engineering effort of integrating this verification technique into a full-featured programming language and interactive development environment.

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.  Our ICFP'14 paper was invited to a special issue of the Journal of Functional Programming, devoted to the best papers of ICFP'14, which appeared in January 2017.  We have presented our most recent work at the National Institute of Informatics (NII), Japan special meeting on "Higher-Order Model Checking" and the Schloss Dagstuhl, Germany seminar on "Language Based Verification Tools for Functional Programs".

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 at the undergraduate honors seminar at UMD in October and at the University of Chile in January 2016. In January 2016, Van Horn presented a tutorial on this material at the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) in St. Petersburg, Florida.  Van Horn presented a tutorial on this material at the 2016 ACM SIGPLAN International Conference on Functional Programming as part of the Programming Languages Mentoring Workshop in Nara Japan.

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