Sophia Drossopoulou: Verifying Trusted Code in an Open World

For the last decade, my collaborators and I have studied what guarantees encapsulation should provide in an open world. The question arose from discussions about object capabilities, membranes and ownership types: these mechanisms can protect state, but we must first specify the properties we want them to guarantee.

In an open system, trusted internal objects interact with external objects whose behavior is unknown. External code may be honest or malicious, may call back into internal code and may hold references to other objects. When trusted code calls an untrusted object, we need to reason about the possible effects on internal state.

There are two complementary forms of guarantee. Encapsulation and object invariants can make some effects impossible. Other effects may be possible only when the external object has a particular capability; controlling access to that capability then controls who can cause the effect.

Consider a shop with an account and a key required to withdraw funds. A buyer is external, but the shop passes it an account so it can pay. Can the buyer steal money? The answer is no if withdrawals require the key, the buyer cannot access it, and the shop does not leak it.

Different account implementations show why whole-module behavior matters. A safe version permits setting the key only during initialization; another permits changing it only with the old key. An unsafe version permits anyone to replace the key and then transfer money. The combination of two individually available calls creates the harmful effect.

The historical multisignature-wallet incident illustrates this kind of emergent behavior: initialization and later operations can combine in an unintended way. We want a specification language that distinguishes safe and unsafe modules, and an inference system that can establish whether a module meets its specification.

For the shop, the goal is to prove that after the external payment call the balance may rise but cannot fall, provided the required protections hold. We also want tooling that can verify such properties rather than relying solely on an informal argument.

A second problem concerns mediation. An internal service may sit between several external objects without knowing which are honest. The service should provide useful behavior while limiting the risk to honest parties, and its specification should state clearly what risk remains.

The central form of the desired guarantee is that an effect cannot occur unless the object causing it has access to a capability. For the account, a decrease in balance is the effect and the key is the capability. We have explored temporal logic, custom specification constructs and invariants as ways to express this idea.

An effect can be described by an assertion it would invalidate. For example, lowering a balance below a threshold invalidates the assertion that it remains at least that threshold. To reason about access, we also need a precise notion of an external object being unable to obtain the capability.

We call an object protected when relevant external objects reachable from the current top frame do not directly point to it, and it is not passed as an argument to an external receiver. The reachability context matters: an unrelated external object elsewhere in the heap does not by itself invalidate this definition.

We also define protection relative to a particular object. Informally, paths from that object to the protected capability must pass through trusted objects that do not release it. This resembles domination: the trusted objects stand between an external origin and the capability.

The other key ingredient is a scoped invariant. Like familiar loop or object invariants, it need not hold at every intermediate step. The property must hold whenever execution is in an external state during a particular call scope, provided it held at the relevant starting point.

The scope ends when the current frame is popped. Within that scope, arbitrary internal and external calls can occur, but the invariant must hold again at the external states covered by the definition. This is different from claiming that it holds forever across the entire execution history.

For the account, we can state that a protected key remains protected within the scope, and that the balance does not decrease while the key is protected. A method-level specification then says that if the key is protected from the buyer before the call, the balance afterwards is at least its original value.

These specifications describe observable effects rather than prescribing a particular API representation. The balance and key could be represented in different ways, including through ghost fields or a database. The aim is to capture emergent behavior across calls, not just a single method’s local result.

To prove such specifications, we build on an underlying Hoare logic rather than starting from scratch. We extend ordinary precondition-and-postcondition triples to quadruples that also describe what must hold at intermediate external states during execution.

The proof system needs rules for protection and encapsulation. To establish a scoped invariant, the relevant assertion must concern encapsulated module state, and public methods must preserve it across their calls. The reasoning also needs to adapt the assertion to the viewpoint of the caller or callee.

Once a module’s scoped invariant is established, it can be used to reason about an external call. In the shop example, that supports the conclusion that calling the buyer’s payment method cannot reduce the protected account balance. The researchers have checked examples and given a handwritten soundness proof.

The team also has a prototype mapping to Dafny. A technical challenge is that protection assertions involve reachability whose footprint is not fixed in the way many existing verification tools expect. The tooling is a research prototype rather than a finished general-purpose solution.

For mediation, consider an escrow service between a buyer and seller. The buyer supplies money and the seller supplies goods, but neither trusts the other. The desired service exchanges them when both sides have enough, and otherwise leaves the parties’ holdings unchanged.

The parties provide external purse objects. An ideal specification would say that a successful exchange transfers the agreed money and goods without affecting other purses, while failure leaves them unchanged. The difficulty is that the mediator cannot assume that every supplied purse behaves honestly.

A simple escrow creates temporary purses, asks the buyer to transfer money and the seller to transfer goods, and then completes the exchange. If the second transfer fails, it attempts to return the money. This works only if the objects’ reported results can be trusted.

A dishonest buyer’s purse can falsely report that it transferred money. The escrow may then continue and deliver the goods even though payment never arrived. This counterexample shows that the original code does not satisfy the desired specification in the presence of arbitrary external objects.

The proposed response is a stronger protocol and a notion of an honest purse. An honest purse creates honest purses and can provide information about the trustworthiness of another purse through successful transfers. A failed transfer can mean insufficient funds or dishonesty, so the specification must distinguish those cases.

Before the exchange, additional interactions establish relationships of trust among the relevant purses. The resulting specification describes what follows when participants are honest, when honest and dishonest objects are mixed, and when all are dishonest and may collude. It also states which unexposed objects remain unaffected.

These specifications are behavioral and hypothetical: honesty is defined through what can happen across calls, not simply by inspecting a class or a stored field. That creates a difficulty when the definition refers to honesty both positively and negatively, making a circular definition unsound.

The team’s solution is stratification. A specification may refer positively to specifications at its own level and negatively only to lower levels. In the example, the purse and escrow properties occupy different levels, avoiding the problematic negative self-reference.

A verification tool for mediation is still being designed as a mapping to Dafny. The team wants more mechanization, richer languages and more than two viewpoints, because real systems can have multiple stakeholders who do not trust one another.

Another priority is framing: repeatedly specifying that every unrelated object remains unaffected is cumbersome. Better ways to describe what does not change would make these specifications easier to write and use.

The broader lesson is to distinguish internal from external objects, provide some encapsulation, and ask what capabilities are necessary for an effect. Traditional preconditions and postconditions alone can be cumbersome when the concern is behavior emerging across multiple calls.

We should also reason about good, bad and mixed cases, including whether one object can eventually reach another. Protection is one proposed definition, not the only possible design. Specifications and verification—whether by logic or testing—help make those assumptions explicit.