Symmaries: Automatic Inference of Formal Security Summaries for Java Programs

TL;DR

Symmaries is a tool that automatically generates formal security summaries for Java bytecode, aiding developers and static analysis tools in understanding and verifying security properties of code.

Contribution

This paper presents a scalable, sound method for automatically inferring formal security summaries for Java programs, implemented in the Symmaries tool.

Findings

Successfully scales to large applications with hundreds of thousands of lines of code.

Achieves promising precision depending on the heap model.

Proves soundness in terms of termination-insensitive non-interference.

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.