Programming language-based security has received renewed interest recently due to the advent of mobile code and the Java language, in particular. Java offers several facilities for obtaining secure code including strong typing, visibility restriction on class members and programmed access to system resources. These protection mechanisms are, however, all local in nature in the sense that they specify what is permitted at a given point in the program. It can be difficult to prove that a given application satisfies a policy expressed in terms of the entire execution of the program.