Checking Security of Java Bytecode by Abstract Interpretation

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.