Trustworthy Proxies: Virtualizing Objects with Invariants

Reference

Van Cutsem, Tom; Miller, Mark S. “Trustworthy Proxies: Virtualizing Objects with Invariants.” In Proceedings of the 27th European Conference on Object-Oriented Programming (ECOOP 2013), Montpellier, France, July 2013. LNCS 7920, pp. 154-178, Springer. URL

Summary

This ECOOP paper is the design rationale for the Proxy API that became standard in ECMAScript 6. Proxies are wrapper objects that virtualise an interface by intercepting all operations via trap functions - a technique essential for membranes, revocable references, access-control wrappers, profilers, taint tracking, higher-order contracts, and lazy/remote object references. The problem the paper addresses: in a language that also has language invariants (e.g., ES5’s non-extensibility and non-configurability - “frozen” objects), can a proxy faithfully virtualise an object that has such invariants without giving up on the language’s guarantee that those invariants hold?

The authors formalise the tension. A “universal, monotonic” language invariant (such as Object.isFrozen(x) ⇒ x.p consistently designates the same value forever) is what lets developers, compilers, and security reviewers locally reason about objects in a dynamic language. A naive proxy API breaks this: a proxy could return different values each time for a property of a target that is frozen, defeating the invariant. The paper’s key contribution is the design of a Proxy API in which proxies refer directly to a target object, and the proxy machinery verifies invariants after each trap call, raising a TypeError if a trap would violate a target’s invariant. This is called invariant enforcement. With it, the language-level frozen-object guarantee holds for proxies too, so clients can still blindly trust Object.isFrozen.

The paper introduces a formal calculus, λ_TP (lambda-TP), an extension of the lambda calculus with proxies and invariant enforcement, and uses it to prove that invariants are preserved. It then demonstrates several important ocap-flavoured access-control abstractions built on trustworthy proxies: revocable membrane references, read-only views, and contract wrappers. This design is foundational to the secure-EcmaScript / hardened-JS / Agoric-SES story, and is the plumbing beneath Object.freeze-based ocap disciplines in modern JS - including MetaMask’s LavaMoat, Endo, and the Spritely-adjacent JavaScript tooling. It is the companion paper to Distributed Electronic Rights in JavaScript (ESOP 2013).

Key Ideas

Proxies = trap-based virtualisation; handlers intercept get, set, has, delete, etc.
Language invariants: universal, monotonic properties of objects (non-extensibility, non-configurability, frozen) that clients and compilers rely on.
The trust problem: naive proxies can claim to wrap a frozen target yet return inconsistent values; isFrozen would have to return false for all proxies, losing transparency.
Invariant enforcement: proxy holds a direct reference to its target; after each trap, the runtime checks that the returned value is consistent with the target’s invariants; inconsistency throws.
λ_TP calculus: formal model of proxies + invariant enforcement in the lambda calculus.
Membranes: with trustworthy proxies, one can build revocable membranes that transitively wrap all outgoing references and revoke the whole object subgraph atomically.
Foundational for SES/hardened-JS: without trustworthy proxies, freezing is not sufficient to ground ocap claims across wrapper boundaries.
This design became ES6 Proxies and the modern JS reflection API.

Connections

The Heart of Spritely - Distributed Objects and Capability Security
E Language - membrane / facet patterns come straight from the E tradition.
CapTP - remote object references across vats are naturally implemented as trustworthy proxies.
Capability Security, Object Capability Security
Ambient Authority - membranes built on proxies are the main device for stripping ambient authority from mobile code.
Confused Deputy - read-only views and attenuated proxies prevent confused-deputy scenarios.
Principle of Least Authority - attenuated proxies are POLA at the reference level.
Distributed Security
Security Kernel Lambda Calculus - λ_TP is a close cousin, also a lambda calculus for ocap reasoning.
Capability Revocation - revocable membranes are the definitive technique, enabled by this API.
Promise Pipelining - remote promises in JS are implemented on top of proxy-like handlers.

Conceptual Contribution

A proxy API can be made trustworthy - able to virtualise objects that carry language-enforced invariants without letting the invariants be broken - if proxies hold direct references to their targets and the runtime verifies, after every trap, that the trap’s behaviour is consistent with the target’s invariants. This single design decision turns proxies from a mere interposition hack into a sound foundation for membranes, revocable references, contracts, and attenuated capabilities in JavaScript.

Tags

#capability-security #proxies #javascript #ecmascript-6 #membranes #invariants #ecoop-2013 #van-cutsem #mark-miller #ocap #lambda-calculus #revocation #hardened-js

Summary

Rees describes Scheme 48, a programming environment whose design is guided by operating-system security principles. The security kernel is W7, a call-by-value lambda-calculus with extensions for abstract data types, object mutation, and hardware access. Each user or subsystem runs in a separate evaluation environment holding the objects representing that user’s privileges; because environments determine availability of object references, protection and sharing are controlled by construction.

The paper describes experience with Scheme 48 as the programming environment for Cornell’s mobile robots (no underlying OS) and as a secure multi-user workstation environment, arguing that lexical scope + first-class environments are a natural substrate for capability-style security among cooperating agents.

Key Ideas

Lambda-calculus as minimal security kernel via capability-style environments.

Scheme 48 (W7): modules, macros, dynamic isolation, portable across platforms.

Trust mediated by controlling which names bind to which objects.

Authentication via capsules (tamper-proof labelled objects).

Applied to robots and multi-user Scheme environments.

Conceptual Contribution

Claim: Lexical scope and first-class environments in a lambda-calculus variant (W7) are a sufficient security kernel: protection reduces to controlling which names bind to which object references.

Mechanism: Implements Scheme 48 as a capability-style environment where each user/subsystem runs in its own environment; authentication via capsules (tamper-proof labelled objects); deployed on Cornell mobile robots (no OS) and as multi-user workstation environment.

Concepts introduced/used: Capability Security, Lambda Calculus, Lexical Scope, Scheme 48, Capsules, Distributed Security, Multi-Agent Systems

Stance: foundational / engineering

Relates to: Provides a principled, capability-based alternative to the input-validation discipline of Seven Turrets Of Babel and the static DDoS analysis of A Language-Based Approach To Prevent DDoS; relevant to sandboxing malicious tools described in MalTool Malicious Tool Attacks.

Summary

The second paper in Spritely’s three-part design series, this whitepaper lays out the technical core of Goblins — a distributed, transactional, object-programming environment built around object capability security (OCap). The thesis: secure peer-to-peer applications should feel like ordinary programming, not like a separate security discipline, and capability security makes that achievable. The operative slogan is “If you don’t have it, you can’t use it” — authority is conveyed only by holding a reference, never ambient.

The paper works through (1) capability security as ordinary reference-passing, motivated against Access Control Lists and the confused-deputy problem; (2) Goblins itself — a distributed object programming model with promise pipelining, vats as containers of synchronous turns, turns as cheap local transactions, and time-travel debugging; (3) OCapN — a new cross-implementation protocol for secure distributed object communication; (4) portable encrypted storage for capabilities; (5) library/application safety implications. Implementations exist for Guile and Racket Schemes, with a roadmap toward language-heterogeneous object invocation.

Goblins is the modern distillation of a three-decade lineage running through Mark Miller’s E language, the CapTP protocol, Jonathan Rees’s capability-kernel argument, and Carl Hewitt’s actor formalism. It reframes agent communication as object-reference passing over the network, offering an alternative substrate to the ACL/RPC-stack approach that dominates modern LLM-agent protocols.

Key Ideas

Principle of Least Authority (POLA): grant each piece of code only the authority it needs, no more

Object capability security: authority = unforgeable object reference. Lexical scoping + no ambient authority + no global mutable state

Confused-deputy problem: why ACLs fail when a privileged program is tricked into acting for an attacker

Vat: an isolated synchronous execution context; objects live inside vats; vats communicate asynchronously

Turn: an atomic event loop iteration inside a vat; turns are transactional — errors roll back the turn’s local state

Promise pipelining (from CapTP): chain calls on a reference before the prior call resolves, reducing round trips

Time-travel distributed debugging: replay turns deterministically across the network

OCapN (Object Capability Network): protocol for secure, cross-language distributed object invocation

Revocation and accountability as programmable patterns over references

“If you don’t have it, you can’t use it” — the design-level simplification capability security provides

Conceptual Contribution

Claim: Secure peer-to-peer applications become routine when authority is conveyed only by holding an unforgeable object reference — no ambient authority, no global mutable state, lexical scope as the capability kernel — and when the network distribution of such references is itself designed as an ordinary message-passing object system.

Mechanism: Goblins realises the E-language tradition in Scheme (Guile, Racket): objects live in vats; each vat runs atomic turns that serve as cheap local transactions; asynchronous inter-vat invocation uses promise pipelining to collapse round-trips; persistence, upgrade, and cross-language interop are handled by OCapN — a capability-preserving transport protocol. Time-travel debugging exploits the turn-level determinism.

Concepts introduced/used: Object Capability Security, Principle of Least Authority, Ambient Authority, Confused Deputy, Vat Model, Turn (Goblins), Promise Pipelining, OCapN, CapTP, E Language, Time-Travel Debugging, Capability Revocation

Stance: engineering / foundational design doc

Relates to: A modern engineering culmination of the capability-security thread rooted in Security Kernel Lambda Calculus (Rees 1995, explicitly cited) — lexical scope as a capability kernel, extended into a full distributed system. The vat model is a direct descendant of A Universal Modular Actor Formalism for Artificial Intelligence (Hewitt 1973) and sibling to Programming Erlang Second Edition but with security-by-reference as a first-class concern. Frames a structural alternative to the modern LLM-agent protocol stack: where Agent-to-Agent Protocol / Model Context Protocol / Agent Network Protocol layer trust on top of ACL/RPC primitives, OCapN encodes trust in the reference graph itself. The flat context trust model that ClawWorm Self-Propagating Attacks Across LLM Agent Ecosystems exploits and that MalTool Malicious Tool Attacks, AI Agents Under Threat catalogue is precisely the ambient-authority failure capability security is designed to prevent — making Goblins / OCapN a serious candidate substrate for Inter-Agent Trust Models - A Comparative Study’s Constraint trust dimension.

Trustworthy Proxies: Virtualizing Objects with Invariants

Reference

Summary

Key Ideas

Connections

Conceptual Contribution

Tags

Backlinks