Active Learning of Points-To Specifications

TL;DR

ATLAS automatically infers points-to specifications for libraries by synthesizing unit tests and observing their behavior, improving static analysis precision without manual effort.

Contribution

It introduces ATLAS, a novel tool that automatically generates points-to specifications through test synthesis and execution, enhancing static analysis accuracy.

Findings

ATLAS successfully infers specifications for Java standard library.

Improves static information flow analysis results on Android apps.

Outperforms existing handwritten specifications in precision.

Abstract

When analyzing programs, large libraries pose significant challenges to static points-to analysis. A popular solution is to have a human analyst provide points-to specifications that summarize relevant behaviors of library code, which can substantially improve precision and handle missing code such as native code. We propose ATLAS, a tool that automatically infers points-to specifications. ATLAS synthesizes unit tests that exercise the library code, and then infers points-to specifications based on observations from these executions. ATLAS automatically infers specifications for the Java standard library, and produces better results for a client static information flow analysis on a benchmark of 46 Android apps compared to using existing handwritten specifications.