A Simple Semantics and Static Analysis for Java Security
Anindya Banerjee, David A. Naumann · 2001
: Security in Java depends on an access control mechanism specied 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 signicantly 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. This material is based upon work supported by the National Science Foundation under Grants EIA-9806835 and INT-9813854. A Simple Semantics and Static Analysis for Java Security Anindya Banerjee a;1 a Stevens Institute of Technology, Hoboken, NJ 07030 USA David A. Naumann b;2 b Stevens Institute of Technology, Hoboken, NJ 07030 USA Abstract Security in Java depends on an access control mechanism specied 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 signi- cantly 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. 1