Analysis for Stack Inspection

Thomas Jensen - IRISA - Rennes, Francia

Data e ora
martedì 13 gennaio 2004 alle ore 16.30

Ca' Vignal 3 - Piramide, Piano 0, Sala Verde

Nicola Fausto Spoto

Referente esterno

Data pubblicazione
28 novembre 2003



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

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