Secure Information Flow in Java by Optimized Reachability Analysis of Weighted Pushdown System

A semantic-based approach is commonly considered more precise than the type-based approach to enforcing secure information flow for the program. As a standard criterion to formalize secure information flow, noninterference has not been analyzed with semantic-based approaches at bytecode level. We propose a semantic-based approach to model checking weighted pushdown system for noninterference. In order to overcome the limitations brought by the language feature and application scenario, we extend ordinary self-composition to low-recorded self composition. In this extension the meta-level indices of heap are recorded, and the auxiliary interleaving assignments, as well as the branch condition to illegal-flow state, are modeled to validate the reachability analysis. We prove the correctness that unreachability of illegal-flow state implies the noninterference property of bytecode program. We also propose three model optimizations: companion methods elimination, parameter reordering, and inner-block optimized abstraction of additional code. The experimental results show the availability, efficiency and scalability of our approach, and the effectiveness of the optimizations.