Secure Information Flow in Java via Reachability Analysis of Pushdown System

Automated verification of noninterference is commonly considered more precise than type-based approach on enforcing secure information flow for program. We propose an approach on model checking symbolic pushdown system generated from Java bytecode, and develop a deployment-time verification framework to ensure noninterference of bytecode. In order to overcome the constraints brought by the nature of object-oriented language and application scenario, we extend self-composition to low-recorded self-composition to reduce the partial correctness judgements on safety property to reachability analysis. In this variation, meta-level indices of heap are recorded into the self-composed pushdown system for the construction of auxiliary interleaving assignments and branch condition to illegal-flow state. Our experiments show that the approach is more scalable than previous work based on automated verification.