Contracts enable mutually suspicious parties to cooperate safely through the exchange of rights. Smart contracts are programs whose behavior enforces the terms of the contract. This paper shows how such contracts can be specified elegantly and executed safely, given an appropriate distributed, secure, persistent, and ubiquitous computational fabric. JavaScript provides the ubiquity but must be significantly extended to deal with the other aspects. The first part of this paper is a progress report on our efforts to turn JavaScript into this fabric. To demonstrate the suitability of this design, we describe an escrow exchange contract implemented in 42 lines of JavaScript code.

JavaScript is widely used to provide client-side functionality in Web applications. To provide services ranging from maps to advertisements, Web applications may incorporate untrusted JavaScript code from third parties. The trusted portion of each application may then expose an API to untrusted code, interposing a reference monitor that mediates access to security-critical resources. However, a JavaScript reference monitor can only be effective if it cannot be circumvented through programming tricks or programming language idiosyncrasies. In order to verify complete mediation of critical resources for applications of interest, we define the semantics of a restricted version of JavaScript devised by the ECMA Standards committee for isolation purposes, and develop and test an automated tool that can soundly establish that a given API cannot be circumvented or subverted. Our tool reveals a previously-undiscovered vulnerability in the widely-examined Yahoo! AD Safe filter and verifies confinement of the repaired filter and other examples from the Object-Capability literature.

Proxies are a powerful approach to implement meta-objects in object-oriented languages without having to resort to metacircular interpretation. We introduce such a meta-level API based on proxies for Javascript. We simultaneously introduce a set of design principles that characterize such APIs in general, and compare similar APIs of other languages in terms of these principles. We highlight how principled proxy-based APIs improve code robustness by avoiding interference between base and meta-level code that occur in more common reflective intercession mechanisms.

Browsers do not currently support the secure sharing of JavaScript objects between principals. We present this problem as the need for object views, which are consistent and controllable versions of objects. Multiple views can be made for the same object and customized for the recipients. We implement object views with a JavaScript library that wraps shared objects and interposes on all access attempts. The security challenge is to fully mediate access to objects shared through a view and prevent privilege escalation. We discuss how object views can be deployed in two settings: same-origin sharing with rewriting-based JavaScript isolation systems like Google Caja, and inter-origin sharing between browser frames over a message-passing channel.

In 1973, John Reynold's and James Morris' Gedanken language retrofit object-capability security into an Algol-like base. Today, there are active projects retrofitting Java, Javascript, Python, Mozart/Oz, OCaml, Perl, and Pict. These represent a variety of approaches, with different tradeoffs regarding legacy compatibility, safety, and expressivity. In this talk I propose a taxonomy of these approaches, and discuss some of the lessons learned to date.

Concurrent Prolog supports object-oriented programming with a clean semantics and additional programming constructs such as incomplete messages, unification, direct broadcasting, and concurrency synchronization [Shapiro 1983a]. While it provides excellent computational support, we claim it does not provide good notation for expressing the abstractions of object-oriented programming. We describe a preprocessor that remedies this problem. The resulting language, Vulcan, is then used as a behicle for exploring new variants of object-oriented programming which become possible in this framework.