A Simple Semantics and Static Analysis for Stack Inspection
Programming Languages
2013-09-23 v1
Abstract
The Java virtual machine and the .NET common language runtime feature an access control mechanism specified operationally in terms of run-time stack inspection. We give a denotational semantics in "eager" form, and show that it is equivalent to the "lazy" semantics using stack inspection. We give a static analysis of safety, i.e., the absence of security errors, that is simpler than previous proposals. We identify several program transformations that can be used to remove run-time checks. We give complete, detailed proofs for safety of the analysis and for the transformations, exploiting compositionality of the eager semantics.
Keywords
Cite
@article{arxiv.1309.5144,
title = {A Simple Semantics and Static Analysis for Stack Inspection},
author = {Anindya Banerjee and David A. Naumann},
journal= {arXiv preprint arXiv:1309.5144},
year = {2013}
}
Comments
In Proceedings Festschrift for Dave Schmidt, arXiv:1309.4557