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.
The tech report is very detailed (~70 pages).
The most interesting part of this work is the careful discussion of how various code transformations are effected by stack inspection. Esp. notice the discussion of tail calls.
Posted to implementation by Ehud Lamm on 6/13/02; 8:18:20 AM