/ elib / legacy

A Theory of Taming Retroactive Theories are Seldom Sound --Norm Hardy

(We recommend reading Taming the Java Interface first.)

Despite Norm's insightful caution, taming is about the construction of retroactive theories. Taming works when the retroactive theories are sound enough. A proper theory of taming requires us to identify when we should and should not expect to be able to create sound retroactive theories.

Work on taming to date has been on taming the Java API in order to obtain, in effect, a capability-oriented class library for E. (Though the same principle should apply for other libraries.) Other approaches to creating such a library are 1) creating one from scratch, or 2) wrapping the Java API in a wholly new API. While both of these approaches are likely safer than taming, they are also a lot more work -- in the case of user interface toolkits, unaffordably more work. The capability-approach to API design is the theory being retroactively imposed, and the Java APIs are the system they are being imposed on -- a system not designed according to capability principles.

We expected to largely succeed at taming Java APIs, and we largely have succeeded; modulo the many problems pointed out by the Taming the Java Interface section of the Darpa Security Review. Why was much success possible in this area? Because well-done, highly modular object design already often resembles good capability design. Where the Java APIs were better by normal oo design principles, they were generally easy to tame. Where they weren't, it was often a mistake to try to tame them. On our next pass over the Java API, we will either wrap (KeyMap) or reimplement (HTML Widget) these, rather than trying to tame them.

There are two kinds of properties that a well designed capability-oriented API written in a capability language would have -- imposed properties and designed properties. Taming should result in an API exhibiting the equivalent of both of these properties.

Imposed Properties

Were the system to be tamed instead written in a capability language, each object would have a certain measure of capability discipline imposed on it, independent of its internal workings. Specifically, it would have some limited set of capabilities it could wield, which determine the limits on the authorities it can exercise. Our first retroactive theory component is to assign to each object a theory of what capabilities it is assumed to be able to hold. When the tamer (the human making taming decisions) has access to the implementation, the object's instance variables (as tamed according to their imposed and designed properties, see below) are often a good initial draft of this theory, to be refined according to other considerations.

Once such a fictional assignment of authority to an object is made, the first and simplest taming decision is to simply disallow any methods on its interface that could cause it to exceed its theorized authorities. For example, E disallows Boolean.getBoolean(String) because this can only be implemented by access to the System properties, and such access exceeds the authorities presumed to be held by the tamed <import:java.lang.Boolean>.

Designed Properties

Each object reference to a tamed object is a capability. As a capability, it provides its client (an object holding it) some authority -- the ability to effect or be effected by the world outside of oneself that the client doesn't otherwise necessarily have. Our second retroactive theory component is to say, for each object type, what authority it provides. This must be a simple and intuitive statement that programmers can think in terms of when using a capability to such an object, and especially when deciding to hand this capability to something else. This statement should also not exceed in authority what a programmer would naturally guess without reading the documentation, though it can be a subset of the natural guess.

Once such a fictional theory of the authority provided by a kind of object is determined, then all methods which would allow a client to exceed this fiction must be diallowed.

The File Example

The taming of java.io.File is the clearest example of why taming according to imposed properties is insufficient. java.io.File objects represent files or directories in the directory tree of a file system. If these File objects were interpreted as capabilities, then it would be as if each designated a place in the file system, but each gave access (by navigation) to the whole file system. Since one can indeed build such a file system abstraction in a pure capability system, an analysis purely in terms of imposed properties will not fix the situation.

However, though the above design is possble in a capability system, it isn't a capability-oriented design. Just as the design of the file system itself provides for the division of storage into a named hierachy, a capability-oriented design should leverage this to provide a corresponding division of the right to access this storage. Starting from the existing Java API, we impose the retroactive theory that a java.io.File instance, if it represents a non-directory normal file, provides the authority to read and write this one file, but no further access to the file system. If it represents a directory, it gives authority to read and edit that directory, and any files and subdirectories transitively under that directory.

This is a purely retroactive theory. It is not in any way related to any of the goals the designers of java.io.File had in mind. Nevertheless, we can succeed at it merely by preventing upward navigation. To do this, we need to

• Suppress getParentFile() (which we failed to do by the time of the review -- a taming bug)
• Suppress resolution of ".." in paths. This cannot be done by taming alone, since it involves altering the behavior of an existing method. This is an example of a technique intermediate between taming and wrapping -- virtualization. In our "sugaring", the wrapping method that imposes this restriction presents the same API as the original. From the perspective of the client, its as if the original interface were changed to impose this restriction.
• Decide on our stance regarding hard and symbolic links. Our initial theory was phrased in terms of "hierarchy", but these links require us to expand our theory somehow.