July 22, 1997 Meeting

10:00am Andrew Wright : Can you trust your applets? Assuring information security with static analysis

Java-enabled web browsers can down-load and execute portable programs (called applets) on demand. This technology apparently offers the potential for building web programs that distribute computation between client and server as necessary to achieve locality and interactivity. Yet few examples of non-trivial applets exist. To safeguard the security and integrity of the client machine from malicious applets, browser security managers severely restrict interactions between applets and their environment. For instance, applets are usually banned from reading or writing local disk. Such strict security policies prevent applets from performing many useful tasks.

To permit more flexible security policies, we adapt compile-time control-flow and data-flow analysis techniques to estimate an information flow graph for an applet. A path from input i to output j indicates that output j may depend on input i. The absence of a path from input i to output j guarantees that output j is independent of the value of input i. With this graph, we can control the applet's access to local resources. If no path exists from local disk to the network in an applet's information flow graph, the applet can manipulate local data, yet is prevented from leaking sensitive data to the outside world.

In this talk, I will describe a polyvariant control-flow and data-flow analysis framework suitable for advanced languages like Scheme, ML, and Java. I will present experimental results that quantify the effectiveness of different polyvariance strategies, as applied to classical compiler optimizations. While value flow graphs computed according to this framework correctly capture value flow for the purposes of compiler optimizations, they do not capture information flow as required for security analysis. I will show how to adapt this framework to compute information flow graphs, and sketch the correctness theorem that assures security.

10:45pm Break

11:00am Kim B. Bruce : Increasing Java's expressiveness with ThisType and match-bounded polymorphism

Proposing extensions to Java to support polymorphism has become a booming cottage industry. In spite of that, we throw one more candidate in the hat. Our extension includes support for match-bounded polymorphism, exact and inexact types, and ThisType. We show by example how these additions greatly enhance the expressive power of the language, while not changing the meaning of programs written in the current version of Java. Many of the ideas for this extension were derived from our earlier language, LOOM.

11:45am Trevor Jim : Defining Security Policies using Query Certificate Managers

We have designed a special-purpose programming language, QCM, for defining security policies on the Internet. QCM programs maintain a database distributed among the nodes of a loosely-coupled network, and interact by exchanging digitally-signed database queries. The database primitives of QCM naturally support essential security functions such as the definition, distribution, and use of access control lists and public key directories. QCM has a formal semantics based on logic and automata theory which may be used to prove that programs implement desired security policies.

Joint work with Carl A. Gunter.

12:30pm Lunch

1:15pm New Business

1:20pm Vijay Saraswat : The Matrix of Virtual Worlds

Matrix is an architecture for network spaces in Java, intended to support long-living network communities, such as those centered around school-systems (e.g. Meadows). Designed as a successor to the widely-used MOO architecture for network spaces, Matrix supports the notion of multiple (authenticated) users connecting from anywhere in the net to a persistent, shared virtual world consisting of interacting objects and processes (e.g., rooms, doors, windows, exits, furniture, cars, filing cabinets, blackboards, telephony and messaging services etc.). Participants may extend the virtual space by creating objects from pre-existing classes, or by uploading their own Matrix code (e.g. for special kinds of backpacks, wrist-watches, games, notes etc). In principle, participants may interact with each other by jointly navigating the web, and via POTS (plain old text services), graphical user-interfaces, or audio, video and telephony interfaces.

The demands of a peristent, multi-user, user-extensible, network space required solutions for several tricky technical problems in Java. In particular, Matrix supports the notion of resource control (no player may create an unbounded number of objects or threads); coherent snapshotting (the state of the system can be stored out to disk for backup) even in the presence of multiple threads; fine-grained object-level security (e.g., the constructions of one participant cannot be destroyed by another participant); and incremental meta-mutation (the structure of classes and objects may be changed ``on the fly'' without shutting down and restarting the server). In addition, remote method invocation (RMI) based server/client interconnections are supported, paving the way to a peer-peer model for Matrix, the basis for a planned distributed architecture.

A novel aspect of the design of Matrix is that (pure) Java is both the implementation language and the programming language of Matrix --- the Java compiler and Virtual Machine are used to compile and execute Matrix programs. Extensive use is made of Java 1.1 APIs such as Object serialization, RMI, and reflection. Java's Class Loading facilities proved key to providing modified access to the core class libraries (e.g. java.lang.{Object,Thread}) so as to support the computational facilities described above.

(This work is being done in collaboration with Chris Rath and Jim Wilson of AT&T Labs.)

2:20pm Kwang Yi : Towards a Cost-effective Exception Analysis of Standard ML Programs

We present a "practical" analysis that detects potential runtime exceptions that are raised and never handled inside SML programs. This analysis will predict abrupt termination of SML programs, which is SML's only one safety hole.

Even though SML program's control flow and exception flow are in general mutually dependent, analyzing the two flows are safely decoupled. Program's control-flow is firstly estimated from a set of equations defined by simple case analysis of call expressions. For cases where exceptions carry functions (i.e., where control flow analysis needs exception analysis) our control flow analysis uses a crude approximation (by types) to assure its safety against the decoupling. Using this call-graph information, program's function-level exception flow is derived as set-constraints, whose least model is our analysis result. Both of these two analyses are proven safe and the reasons behind each design decision are discussed. A preliminary implementation shows a promising cost-accuracy performance. For the ML-Lex program, for example, the analysis takes 4.58 seconds and it reports 4 may-uncaught exceptions, among which 3 exceptions can really escape. Our final goal is to make the analysis overhead less than 10% of the compilation time (compiling the ML-Lex takes 6 to 7 seconds) and to analyze modules in isolation.

Joint work with Sukyoung Ryu.

3:05pm Break

3:15pm Krishna Kishore Dhara : Behavioral Subtyping in Object-Oriented Languages

Modularity and code reuse are two important features of object-oriented programming. Modularity means that adding new components does not require reverification or respecification of existing components. A common form of reuse in object-oriented programs is to add new subtypes to existing types and to invoke already existing procedures with objects of these new types. In such cases, behavior of programs that contain these procedures also depend on the behavior of the new subtype objects. Reverifying the code that uses existing procedures whenever new types are added is not practical and is not modular. Thus, a notion of behavioral subtyping that allows sound modular reasoning is important for object-oriented programming.

In this talk, we propose two notions of behavioral subtyping for arbitrary abstract data types in the prescence of mutation and aliasing. Strong behavioral subtypes have objects that act like supertype objects in all cases, whereas as weak behavioral subtypes have objects that only need to act like supertype objects when manipulated as supertype objects. Both these notions allow sound modular reasoning based on the static types of variables in programs. Weak behavioral subtyping allows conclusions about programs based on the effects of individual procedures but restricts certain forms of aliasing. Strong behavioral subtyping allows all forms of aliasing but permits conclusions based only on the history constraints of the types. History constraints are the reflexive and transitive properties preserved by objects of a type across different states of a program. We prove that both these behavioral subtype notions are sufficient for sound modular reasoning.

4:00pm Talks End