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 language | English |
---|---|
Pages (from-to) | 284-308 |
Number of pages | 25 |
Journal | Electronic Proceedings in Theoretical Computer Science, EPTCS |
Volume | 129 |
DOIs | |
State | Published - 2013 |
Event | Semantics, 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 2013 → 20 Sep 2013 |