Symmaries: Automatic Inference of Formal Security Summaries for Java Programs

TL;DR

Symmaries introduces a scalable, sound framework for automatically inferring formal security summaries of Java bytecode methods. It uses a modular, bottom-up, summary-based static analysis withGuard/Effect contracts over a symbolic SCFG heap model to capture both information flows and aliasing. The approach proves termination-insensitive non-interference and demonstrates scalability to large real-world Java applications, while offering a usable summary format for developers and static analyzers. Key innovations include co-reachability-based summary construction, triangularization for precise updates, and modular inter-procedural analysis that reuses method summaries across call sites.

Abstract

We introduce a scalable, modular, and sound approach for automatically constructing formal security specifications for Java bytecode programs in the form of method summaries. A summary provides an abstract representation of a method's security behavior, consisting of the conditions under which the method can be securely invoked, together with specifications of information flows and aliasing updates. Such summaries can be consumed by static code analysis tools and also help developers understand the behavior of code segments, such as libraries, in order to evaluate their security implications when reused in applications. Our approach is implemented in a tool called Symmaries, which automates the generation of security summaries. We applied Symmaries to Java API libraries to extract their security specifications and to large real-world applications to evaluate its scalability. Our results show that the tool successfully scales to analyze applications with hundreds of thousands of lines of code, and that Symmaries achieves a promising precision depending on the heap model used. We prove the soundness of our approach in terms of guaranteeing termination-insensitive non-interference.

Figures (6)

• Figure 1: An example Java bytecode (left) and the security summary for RandomAccessFile.write (right)
• Figure 2: A heap model and its formal representation $\mathsf{h}\xspace$
• Figure 3: Our Summary-Based Approach
• Figure 4: Computing the symbolic summary of a method $m$.
• Figure 5: Rules for inferring summaries.