Reasoning about External Calls

TL;DR

This paper presents a new logical framework for reasoning about internal code that interacts with external, untrusted code, ensuring safety through capabilities and formal verification methods.

Contribution

It introduces new assertions, specifications, and a Hoare logic for verifying internal code that relies on encapsulation and object capabilities when making external calls.

Findings

Proposed a Hoare logic for external call reasoning

Mechanised proofs demonstrating soundness

Verified safety properties of internal modules

Abstract

In today's complex software, internal trusted code is tightly intertwined with external untrusted code. To reason about internal code, programmers must reason about the potential effects of calls to external code, even though that code is not trusted and may not even be available. The effects of external calls can be limited, if internal code is programmed defensively, limiting potential effects by limiting access to the capabilities necessary to cause those effects. This paper addresses the specification and verification of internal code that relies on encapsulation and object capabilities to limit the effects of external calls. We propose new assertions for access to capabilities, new specifications for limiting effects, and a Hoare logic to verify that a module satisfies its specification, even while making external calls. We illustrate the approach though a running example with mechanised proofs, and prove soundness of the Hoare logic.