Trustworthy and Composable Software Systems with Contracts - July 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): Foster, Hicks, Tobin-Hochstadt, Van Horn
Researchers: Nguyen

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 hypothesis the approach scales to cover multi-language programs and security properties.

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

Not only have our results been presented, we have also 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.

Educational:

We intend to propose a tutorial based on the above work to be presented at the ACM SIGPLAN-SIGACT Symposium on the Principles of Programming Languages in January 2015 in Mumbai, India.  The tutorial, if accepted, would reach a large number of the world's best researchers in language-based security.

HARD PROBLEM(S) ADDRESSED

This refers to Hard Problems, released November 2012.

Scalability and Composability

Metrics

PUBLICATIONS
Report papers written as a results of this research. If accepted by or submitted to a journal, which journal. If presented at a conference, which conference.

Soft Contract Verification, Nguyen, Tobin-Hochstadt, Van Horn.  To appear in proceedings of The 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 2014.

ACCOMPLISHMENT HIGHLIGHTS