Checking security of Java bytecode by abstract interpretation
- 11 March 2002
- proceedings article
- Published by Association for Computing Machinery (ACM)
- p. 229-236
- https://doi.org/10.1145/508791.508839
Abstract
We present a method to certify a subset of the Java bytecode, with respect to security. The method is based on abstract interpretation of the operational semantics of the language. We define a concrete small-step enhanced semantics of the language, able to keep information on the flow of data and control during execution. A main point of this semantics is the handling of the influence of the information flow on the operand stack. We then define an abstract semantics, keeping only the security information and forgetting the actual values. This semantics can be used as a static analysis tool to check security of programs. The use of abstract interpretation allows, on one side, being semantics based, to accept as secure a wide class of programs, and, on the other side, being rule based, to be fully automated.Keywords
This publication has 19 references indexed in Scilit:
- Abstract interpretation of operational semantics for secure information flowInformation Processing Letters, 2002
- A semantic approach to secure information flowScience of Computer Programming, 2000
- From system F to typed assembly languageACM Transactions on Programming Languages and Systems, 1999
- A type system for Java bytecode subroutinesACM Transactions on Programming Languages and Systems, 1999
- What's in a region?ACM Letters on Programming Languages and Systems, 1993
- A security flow control algorithm and its denotational semantics correctness proofFormal Aspects of Computing, 1992
- Abstract Interpretation FrameworksJournal of Logic and Computation, 1992
- An Axiomatic Approach to Information Flow in ProgramsACM Transactions on Programming Languages and Systems, 1980
- Certification of programs for secure information flowCommunications of the ACM, 1977
- A lattice model of secure information flowCommunications of the ACM, 1976