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

Session types describe the sequence and format of messages on point-to-point communication channels. They allow communication protocols to be specified type-theoretically so that their implementations can be verified by static type-checking. Session types were introduced in the setting of process calculus, and later formulated for imperative, functional and object-oriented languages. The quest for a clean integration of session types and objects leads to the idea of embedding session types in a more general setting of typestate, in which the operations available for a given object are state-dependent. We are exploring this idea with a typestate system in which typestate specifications are inspired by session types, and developing an experimental implementation as an extension of Java.

Joint work with Vasco Vasconcelos, Antonio Ravara, Nils Gesbert, Ornela Dardha, Dimitrios Kouzapas

Reasoning about the security of shell scripts is notoriously hard. This is in large part because it is difficult for programmers to deduce the effects of shell scripts on the underlying operating system. First, resource references, such as file paths, are typically resolved lazily and subject to race conditions.? Second, shell scripts are typically run with the same privileges as the invoking user, making it hard to determine or enforce that a script has all (and only) permissions to execute successfully. Third, shell scripts invoke other programs, often arbitrary binaries.

In this talk, I present the preliminary design and implementation of Shill, a secure shell scripting language that uses fine-grained capabilities to restrict access to resources. Capabilities bind resources at the time of their creation, and avoid vulnerabilities arising from lazy name resolution. Shill scripts come with contracts that specify and restrict what capabilities the script may use. A Shill script can invoke an arbitrary binary in a sandbox that limits the privileges of the binary based on a set of capabilities. Capabilities together with contracts and sandboxing enable the caller of a script to reason precisely about which resources a script (and the binaries it calls) may access, and thus, Shill helps reason safely and effectively about the use and composition of scripts. We have implemented Shill on top of FreeBSD, using Racket and the FreeBSD Trusted MAC framework.

Contracts are a popular mechanism for enhancing the interface of components. In the world of first-order functions, programmers embrace contracts because they write them in a familiar language and easily? understand them as a pair of a pre-condition and a post-condition. In a? higher-order world, contracts offer the same expressiveness to? programmers but their meaning subtly differs from the familiar first-order notion. For instance, it is unclear what the behavior of? dependent contracts for higher-order functions or of contracts for mutable data should be. As a consequence, it is difficult to design? monitoring systems for such higher-order worlds.

In response to this problem, we investigate complete monitors, a formal? framework for deciding if a contract system is correct. The intuition behind the framework is that a correct contract system should:
— mediate the exchange of values between contracted components
— and blame correctly in case of contract violations.
The framework reveals flaws in the semantics for dependent contracts? from the literature and suggests a natural fix. In addition, we demonstrate the usefulness of the framework for language design with a? language with contracts for mutable data and a language that mixes typed and untyped imperative programs. The final contribution is the provably correct design of a novel form of contracts, dubbed options contracts, that mix contract checking with random and probabilistic checking.

Communication contracts describe the global interactive behaviour of
concurrent and distributed systems. The challenge is to verify whether
a given program (or collection of programs) adheres a contract. If
that turns out to be the case, properties such as absence of 'message
not understood', undesired races and deadlocks are automatically
guaranteed. We show one such system for Message Passing Interface
programs.

We consider the problem of verifying if a program trace is valid with
respect to a regular program specification, e.g. expressed in terms of
regular expressions or linear temporal logic formulas. Existing
methods only provide yes/no answers. Such answers are unsatisfactory
and not helpful to precisely track down the source of a failure. We
introduce a constructive method which provides detailed explanations about the
outcome of trace validation in a form comprehensible for the user. For
example, we obtain information which parts of the specification have
been exercised in case of success and which parts have been violated
in case of failure. The approach has been fully implemented and is
applied in some real-world projects for testing of synchronously
executed software components.

Deadlock freedom is for concurrent programs what progress is for sequential ones: it indicates the absence of stable (i.e., irreducible) states in which some pending operations cannot be completed. In the particular case of communicating processes, operations are inputs and outputs on channels and deadlocks may be caused by mutual dependencies between communications. In this talk we see how to define an effect system ensuring deadlock freedom of higher-order programs and discuss some of its properties.

The talk covers three topics related (in my opinion) to 
the seminar: behavioral types, resource usage verification (or typestate
checking), and higher-order model checking, and discuss their relationship.
First, I review our earlier work on behavioral types, and
explain how they can be used for analysis of concurrent programs 
and resource usage verification (or, typestate checking) of functional programs.
I will then explain how that line of work has evolved to our more
recent work on resource usage verification based on higher-order 
model checking.