Reasoning about External Calls

By Prof. Sophia Drossopoulou

Abstract
In today’s complex software, internal, trusted, code is tightly intertwined with external, untrusted, code. By definition, internal code does not trust external code. From an internal perspective, the effects of outgoing calls to external code – external calls — are necessarily unknown and unlimited.

Nevertheless, the effects of external calls can be tamed if internal code is programmed defensively, i.e. to ensure particular effects cannot happen. Tamed effects allow us to prove that internal code preserves assertions about internal and external objects, even in the presence of outgoing calls and callbacks.

In this talk, we address  the specification and verification of internal code that makes external calls, using encapsulation and object capabilities to tame effects. We propose new assertions for access to capabilities, new specifications for tamed effects, and a Hoare logic to verify that a module satisfies its tamed effects specification, even while making external calls. We illustrate the approach though a running example, and outline proof of soundness of the Hoare logic.

Bio
Sophia Drossopoulou is a Professor at Imperial College London. She works on programming languages in general, and in particular on types, concurrency and program verification.

More information