Specification and Verification of Robust Open Systems: Capabilities, Effects, and Trusted Mediation

Today's complex software is open: trusted internal code is tightly intertwined with untrusted external code whose behaviour may be unknown, or even adversarial. Writing robust internal code in such settings is challenging — programmers must account for the potential effects of calls to external code even when that code cannot be inspected or trusted. These effects can be limited if internal code is written defensively, restricting the effects of external calls by ensuring that these effects can only be caused through access to certain capabilities.

This work addresses the specification and verification of robust internal code that relies on encapsulation and object capabilities to limit the effects of external calls. We propose new assertions for capability access, new specifications for bounding the effects of external calls, and a Hoare logic for verifying that a module satisfies its specification even in the presence of external calls.

We then broaden our scope to the question of risk n the open world. Trusted mediators — such as an escrow — act as intermediaries between mutually distrusting parties who may or may not adhere to agreed protocols. Robust mediator code must not only fulfil its own obligations, but also limit the risk to which the parties are exposed. We address the questions of how such risk can be formally specified, and how we can verify that the mediator's code faithfully adheres to its specification.