No.050 Software Contracts for Communication, Monitoring, and Security

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.

In this work, we tackle the problem of 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
that leverages contracts as a rich source of symbolic values, including
unknown behavioral values, and employs an updatable heap of contract
invariants to reason about flow-sensitive facts. The approach is able to
analyze first-class contracts, recursive data structures, unknown
functions, and control-flow-sensitive reasoning about 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.