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

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) 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, we presented the results at the ACM SIGPLAN Internation Conference on Functional Programming, one of the premier publication venues for programming language research.

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.

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.

• Soft Contract Verification.  Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn.  The ACM SIGPLAN International Conference on Functional Programming.  http://dx.doi.org/10.1145/2628136.2628156
  
  Abstract: Behavioral software contracts are a widely used mechanism for governing the flow of values between components. However, run-time monitoring and enforcement of contracts imposes significant overhead and delays discovery of faulty components to run-time.

  To overcome these issues, we present soft contract verification, which aims to statically prove either complete or partial contract correctness of components, written in an untyped, higher-order language with first-class contracts. Our approach uses higher-order symbolic execution, leveraging contracts as a source of symbolic values including unknown behavioral values, and employs an updatable heap of contract invariants to reason about flow-sensitive facts. We prove the symbolic execution soundly approximates the dynamic semantics and that verified programs can't be blamed.

  The approach is able to analyze first-class contracts, recursive data structures, unknown functions, and control-flow-sensitive refinements of values, which are all idiomatic in dynamic languages. It makes effective use of an off-the-shelf solver to decide problems without heavy encodings. The approach is competitive with a wide range of existing tools - including type systems, flow analyzers, and model checkers - on their own benchmarks.
   
• Higher-Order Contract Counterexamples.  Poster presented at The ACM SIGPLAN International Conference on Functional Programming.  Provides a method for generating witnesses to contract violations.

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