Stack Inspection: Theory and Variants

Cedric Fournet and Andy Gordon

Stack inspection is a security mechanism implemented in runtimes such
as the JVM and the CLR to accommodate components with diverse levels
of trust.  Although stack inspection enables the fine-grained
expression of access control policies, it has rather a complex and
subtle semantics. We present a formal semantics and an equational
theory to explain how stack inspection affects program behaviour and
code optimisations.  We discuss the security properties enforced by
stack inspection, and also consider variants with stronger, simpler
properties.