Journal of Functional Programming

Table of Contents - 2005 - Volume 15, Issue 02  



Special Issue on Language Based Security

Interfaces for stack inspection

FRÉDÉRIC BESSON a1, THOMAS DE GRENIER DE LATOUR a1 and THOMAS JENSEN a1
a1 IRISA/CNRS and INRIA-Rennes, Campus de Beaulieu, F-35042 Rennes, France (email: fbesson@irisa.fr, degrenie@irisa.fr, jensen@irisa.fr)

Article author query
besson f   [Google Scholar] 
de grenier de latour t   [Google Scholar] 
jensen t   [Google Scholar] 
 

Abstract

Stack inspection is a mechanism for programming secure applications in the presence of code from various protection domains. Run-time checks of the call stack allow a method to obtain information about the code that (directly or indirectly) invoked it in order to make access control decisions. This mechanism is part of the security architecture of Java and the .NET Common Language Runtime. A central problem with stack inspection is to determine to what extent the local checks inserted into the code are sufficient to guarantee that a global security property is enforced. A further problem is how such verification can be carried out in an incremental fashion. Incremental analysis is important for avoiding re-analysis of library code every time it is used, and permits the library developer to reason about the code without knowing its context of deployment. We propose a technique for inferring interfaces for stack-inspecting libraries in the form of secure calling context for methods. By a secure calling context we mean a pre-condition on the call stack sufficient for guaranteeing that execution of the method will not violate a given global property. The technique is a constraint-based static program analysis implemented via fixed point iteration over an abstract domain of linear temporal logic properties.

(Published Online March 3 2005)