Bytecode Verification for Enhanced JVM Access Control

This paper presents an approach to addressing the known weaknesses and security issues of JVM stack inspection in a unified framework. We first propose an enhanced JVM access control mechanism. In this mechanism, values are also associated with security levels. When enforcing access control, this mechanism checks not only the permissions of code on stack as the usual stack inspection, but also the security levels of values to make sure they are used legally. We then present a static type system to verify whether a bytecode program satisfies the security property achieved by this enhanced mechanism. This type system performs modular and context-sensitive analysis at the method level by generating and solving constraints, and path-sensitive analysis at the code block level by using a trace-based approach. In addition, this type system does not need any user annotation for verification.