Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Reasoning about External Calls

Sophia Drossopoulou, Julian Mackay, Susan Eisenbach, James Noble

TL;DR

This work tackles reasoning about external calls in an object-capability setting by introducing protection assertions, a specification language for limited effects, and a Hoare-quadruple verification framework. Central ideas include scoped invariants that hold within a method's dynamic execution and an adaptation mechanism to transfer assertions across call boundaries, enabling sound reasoning about untrusted external code. The authors prove the soundness of their Hoare quadruples, provide a mechanised Coq proof for a running Shop example, and demonstrate how internal modules can guarantee safety properties despite arbitrary external interactions. The approach supports modular verification in open-world settings, offering concrete guarantees about preventing unwanted effects while enabling safe interactions via public interfaces. This work thus advances defensive consistency for multi-component systems by formalizing protection, scoped reasoning, and external-call adherence within a unified verification framework.

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.

Reasoning about External Calls

TL;DR

This work tackles reasoning about external calls in an object-capability setting by introducing protection assertions, a specification language for limited effects, and a Hoare-quadruple verification framework. Central ideas include scoped invariants that hold within a method's dynamic execution and an adaptation mechanism to transfer assertions across call boundaries, enabling sound reasoning about untrusted external code. The authors prove the soundness of their Hoare quadruples, provide a mechanised Coq proof for a running Shop example, and demonstrate how internal modules can guarantee safety properties despite arbitrary external interactions. The approach supports modular verification in open-world settings, offering concrete guarantees about preventing unwanted effects while enabling safe interactions via public interfaces. This work thus advances defensive consistency for multi-component systems by formalizing protection, scoped reasoning, and external-call adherence within a unified verification framework.

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.

Paper Structure

This paper contains 103 sections, 48 theorems, 56 equations, 21 figures.

Table of Contents

  1. Introduction
  2. The problem and our approach
  3. Shop -- Illustrating Limited Effects
  4. 1$^{st}$ Challenge: Specification Language
  5. Protection
  6. Scoped Invariants
  7. 2$^{nd}$ Challenge: A Hoare Logic for Adherence to Specifications
  8. Hoare Quadruples
  9. Well-formed modules and External Calls
  10. Summary
  11. The Underlying Programming Language ${\mathcal{L}}_{ul}$
  12. ${\mathcal{L}}_{ul}$ Syntax and Runtime Configurations
  13. ${\mathcal{L}}_{ul}$ Execution
  14. Fundamental Concepts
  15. Method Calls and Returns
  16. ...and 88 more sections

Key Result

Lemma 3.3

For all $\overline{M}$, $\sigma$, $\sigma'$: $\space \overline{M};\, {\sigma} {\rightsquigarrow^*} \sigma' \ \wedge \ |\sigma|=|\sigma'|\ \ \ \Longrightarrow\ \ \ \forall x\in Prms(\overline{M},\sigma).[ \ \lfloor x \rfloor_{\sigma} = \lfloor x \rfloor_{\sigma'} \ ]$

Figures (21)

  • Figure 1: The current point of execution before buy, during buy, and during pay. Frames $\phi_1$, $\phi_2$ are green as their receiver (this) is internal; $\phi_3$ is red as its receiver is external. Continuations are omitted.
  • Figure 2: Protected from and Protected. -- continuing from Fig, \ref{['f:CurrentPoint']}.
  • Figure 3: Execution. Green disks represent internal states; red disks external states.
  • Figure 4: ${\mathcal{L}}_{ul}$ Syntax. We use $x$, $y$, $z$ for variables, $C$, $D$ for class identifiers, $f$ for field identifier, ${gf}$ for ghost field identifiers, $m$ for method identifiers, $\alpha$ for addresses.
  • Figure 5: ${\mathcal{L}}_{ul}$ operational Semantics
  • ...and 16 more figures

Theorems & Definitions (104)

  • Example 2.1
  • Example 2.2
  • Example 2.3
  • Definition 3.1
  • Definition 3.2: Scoped Execution
  • Lemma 3.3
  • Definition 3.4
  • Definition 3.5: Well-formed states
  • Lemma 3.6
  • Definition 4.1
  • ...and 94 more