Analysis for Stack Inspection

Java's stack inspection mechanism offers a means of securing code
operating in an environment where code from different origins and with
different permissions cooperate. The mechanism provides access to the
run-time stack which can be queried to obtain information about code
requesting a specific service. Stack inspection has turned out to pose
a number of interesting programming language-theoretic questions. In
this talk we will summarise the stack inspection mechanism and
elements of its theory. We will then go into more detail concerning
techniques for verifying security properties of stack inspecting Java
programs by a combination of static analysis and model checking. We
will be addressing the problem of verifying the security of program
fragments; in particular libraries protected by the use of stack
inspection.

Joint work with Frédéric Besson and Thomas de Grenier de Latour.