When Web browsers began to support Java, JavaScript, and other forms of mobile code, they created the new problem of trying to run untrusted code within a trusted user-level process. By studying the security of Java, a wide variety of bugs were found, many of which pointed to flaws in the underlying design of the system.

In order to make a mobile code system secure, there must be an architecture which can protect sensitive system resources, such as the file system and network. Unfortunately, mobile code systems have trusted and untrusted parts tightly interacting with each other, making traditional security architectures less feasible.

This talk describes an approach used in current Java systems called stack inspection. While stack inspection has proven itself to be useful, it has been criticized for its seemingly ad-hoc nature. I will present a formal model of stack inspection using a belief logic. This model captures the complex trust relationships in a mobile code system. I use the model to show how the state of a stack inspection system can be reduced to a finite-state automaton, simplifying the implementation and yielding significant speedups. I also show how stack inspection can be extended to support secure remote procedure calls in a novel manner.