Verifying Code That Calls Code You Can't Trust • Sophia Drossopoulou • Bug Bash EU 2026
This talk presents a line of work on specifying and verifying software in open settings, where trusted internal code interacts with untrusted external code. It introduces object capabilities, protection, and scoped invariants as a way to reason about which effects external calls can cause, illustrated with a shop-account example and the Parity multi-sig failure. It then extends the approach to mediating objects through an escrow case study involving honest purses, trust, risk, and a stratified specification that resolves a paradox.
Specifying and verifying robust open systems
Modern software is open: trusted internal code is tightly intertwined with external code whose behaviour may be unknown, buggy, or adversarial. This work, carried out over roughly ten years with James Noble, Susanna Eisenberg and Julian Mackay, and earlier with Mark Miller and Toby Murray, began with a discussion about encapsulation in ECMAScript, membranes, and ownership types. The central question was what encapsulation is meant to guarantee, and in particular what guarantees matter in an open world where external objects may reference internal ones and call into them, and internal objects may call out.
Effects, invariants and capabilities
When internal code passes an external argument and then makes a call to untrusted code, the question is which effects can reach the internal state. There are two broad answers. Some effects can never happen, which is what object invariants guarantee when the relevant state is fully encapsulated and the code is written accordingly. Other effects may happen, but only if the external code obtains a particular object capability. If that capability is controlled, the effect is controlled too.
A shop example makes this concrete. The shop holds an account, the account is guarded by a key, and the key governs withdrawals. When the shop asks an external buyer to pay into the account, the buyer gains access to the account. Whether that is safe depends on three conditions: the account’s balance can only decrease if the caller holds the key, the buyer must not hold the key, and the shop must never leak the key. Two versions of the account class illustrate the difference. In the bad version, the set-key method changes the key unconditionally, so an attacker can replace the key and then transfer funds, an emergent failure similar to the Parity multi-sig wallet hack, in which an attacker made themselves the sole owner and then controlled the wallet. In the good version, the key can only be changed by someone who already holds the previous key.
The talk sets out six goals. The first is a specification language that separates good modules from bad ones. The second is an inference system that proves a module satisfies a specification. The third is reasoning about external calls. The fourth is a tool to carry out such proofs. The fifth is mediation, where an internal object serves several external parties, some honest and some not, and must minimise risk while being explicit about what that risk is. The sixth is a verification tool for mediating objects.
Protection and scoped invariants
The specification approach was reached after three attempts, using temporal logics, then custom specification constructs, and finally invariants. Effects are described by assertions that the effect invalidates, so a decrease in balance invalidates the assertion that the balance is at least some amount.
The key notion is protection. An object is protected from the external world if no external object reachable from the current top frame holds a field pointing to it, and if the receiver is external, the object is not passed as an argument. An object is protected from a given originator if every route from that originator to it passes through good objects that will not hand over a reference. This is like a domination relation: trusted objects dominate the paths to the protected object.
On top of protection sits the scoped invariant. An assertion is a scoped invariant of a module if, whenever execution is in external code and the assertion holds, it continues to hold at every subsequent point where control returns to external code, provided execution does not pop the current top frame. Unlike ordinary loop or object invariants, which may be temporarily broken, scoped invariants are checked across the whole span of a call. They are also distinct from history invariants. A diagram of states, colouring internal and external receivers and marking calls as arrows, makes the scope precise: if the assertion holds at one external state, it holds at all external states within that call, but not necessarily afterwards.
Using these ingredients, three specifications capture the good behaviour. If the key is protected, it remains protected until the current frame is popped. If the key is protected, the balance does not decrease. For the buy method, if the key is protected from the buyer and the balance starts at a given value, the balance afterwards is at least that value. The good and fine modules satisfy these specifications, and the bad module does not. The specifications are agnostic to the API. They do not depend on how the key or balance is represented, whether as ghost fields or as data in a database. They talk about effects and emergent behaviour, which is exactly what the multi-sig failure required.
An inference system
The inference system has three layers. It starts from an underlying core Hoare logic, so as not to reinvent established machinery. Core triples are extended to quadruples, where the precondition and postcondition are supplemented by the requirement that the scoped invariant holds in every intermediate external state. Further rules handle protection, such as the fact that creating a new object does not change which things are protected, and handle viewpoint adaptation, which rewrites assertions from the perspective of a collaborator.
The main technical challenge is proving that scoped invariants are preserved. This requires that the assertion be encapsulated, meaning its footprint lies within the module’s own state, so the module can refuse to let external code read its private fields. Then each public method must be shown to preserve the assertion. Using these rules, the pay method can be shown not to decrease the balance. Several further examples were verified using a proof assistant, and soundness of the system was established by hand.
Tooling
To avoid reinventing tools, the team built a prototype that maps the approach onto Dafny. Existing verification tools assume that the footprint of an assertion is known, whereas the footprint of a protection assertion is not, so this required new thinking about how protection is encoded. The authors believe this has been resolved.
Mediation and the escrow
The mediation problem is illustrated with an escrow service from Mark Miller’s work. A buyer and a seller bring purses containing money and goods, and the escrow must exchange them only if both sides have sufficient funds, without any central authority to trust. A naive escrow implementation fails when a buyer supplies a wrong purse that appears to contain money but does not, which lets the buyer walk away with both money and goods. The fix is to strengthen the protocol and the purse abstraction, making purses honest. An honest purse can sprout further honest purses, and a successful transfer from one honest purse to another vouches for the honesty of the other party. The escrow runs a sequence of such calls to establish mutual trust before performing the exchange.
The resulting specification states that if the escrow returns true, either all parties were honest and the exchange completed or there were insufficient funds, or some parties were dishonest. In the mixed case, the result is false and honest parties are unaffected, thanks to protection. If everyone is dishonest, the result may be true or false, and in the collusion case nothing can be concluded. The authors argue this is a useful specification for buyers and sellers, because it expresses both trust and risk explicitly.
A paradox and its resolution
The specification of honest purses turned out to be circular. Honesty of a purse was defined in terms of dishonesty of others, and dishonesty in turn depended on honesty, which resembles Russell’s paradox and made the whole system unsound. The first ingredient of the fix is stratification: specifications are assigned levels, so that a specification may refer to itself only in positive positions and may refer to lower levels in negative positions. Honest purse sits at level zero, and honest escrow sits at level one, referring to honest purse only negatively, which is permitted.
Open directions
Several goals remain. These include more mechanisation, richer perspectives beyond the current two-world model of internal and external objects, architectures with many stakeholders who do not trust one another, a more expressive toy language and different programming paradigms, serious tools, and a reconsidered framing. The current style forces cumbersome statements such as everyone else is unaffected. The overall conclusions are that the distinction between internal and external objects is worth making in programming languages, that platforms need some notion of encapsulation, that necessary conditions for effects and emergent behaviour matter, and that pre- and postcondition specifications are insufficient for these properties. Analysis should consider whether an object may eventually gain access to another, and should cover both good and bad scenarios as well as mixed honest and dishonest ones. Specification and verification, whether through Hoare-style logics or through testing, are presented as valuable in either form.