Analysis for Stack Inspection

Relatore
Thomas Jensen - IRISA - Rennes, Francia

Data e ora
martedì 13 gennaio 2004 alle ore 16.30

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

Referente
Nicola Fausto Spoto

Referente esterno

Data pubblicazione
28 novembre 2003

Dipartimento
 

Riassunto

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.
ornamento
Inizio pagina