A simple semantics and static analysis for stack inspection

Anindya Banerjee, David A. Naumann

Research output: Contribution to journalConference articlepeer-review

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.

Original languageEnglish
Pages (from-to)284-308
Number of pages25
JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
Volume129
DOIs
StatePublished - 2013
EventSemantics, Abstract Interpretation, and Reasoning About Programs: Essays Dedicated to David A. Schmidt on the Occasion of His 60th Birthday - Manhattan, KS, United States
Duration: 19 Sep 201320 Sep 2013

Fingerprint

Dive into the research topics of 'A simple semantics and static analysis for stack inspection'. Together they form a unique fingerprint.

Cite this