Reasoning about External Calls
summary
Paper proposes concrete assertions and a verification calculus that prove internal code cannot lose funds despite invoking unknown external objects. It models a shop/account example, defines scoped invariants (protection relative to the top stack frame), formalises “no currently accessible external object has the key,” and gives a sound Hoare logic plus mechanised proofs and evaluated artifacts. Specifications distinguish the careless (key leaked) from the safe modules and show balance only decreases if a capability is actually accessible.
AI-written summary · about
chapters (8)
- 0:00External calls problem
- 1:02Object capabilities and safety
- 3:13Limiting external call effects
- 5:22Good vs bad module designs
- 8:32Protection and invariants
- 12:48Scoped invariants for calls
- 15:21Verification and specs
- 16:23Summary and Q&A
related talks
23mSpecifying and Verifying Future Conditions
46mKeynote: Formal Verification? No, Formal Reasoning!
17mProving capability safety in the presence of indirect sentries
54mReasoning about Progress of Concurrent Objects
28mReasoning about Distributed Reconfigurable Systems
23mReturn of the Theorem
10mClear as Mud
36mObject Capabilities