NESA: Relational Neuro-Symbolic Static Program Analysis

TL;DR

NESA introduces a neuro-symbolic, compilation-free static program analysis method leveraging large language models, enabling customizable analysis with reduced hallucinations and improved performance on benchmarks and real-world bugs.

Contribution

The paper presents NESA, a novel neuro-symbolic approach using a restricted Datalog policy language and decomposition to enhance static analysis with LLMs, reducing hallucinations and surpassing existing techniques.

Findings

NESA achieves 66.27% precision and 78.57% recall in taint vulnerability detection.

NESA detects 13 real-world memory leak bugs fixed by developers.

NESA outperforms some industrial approaches in F1 score on TaintBench.

Abstract

Static program analysis plays an essential role in program optimization, bug detection, and debugging. However, reliance on compilation and limited customization hinder its adoption in the real world. This paper presents a compositional neuro-symbolic approach named NESA that facilitates compilation-free and customizable static program analysis using large language models (LLMs) with mitigated hallucinations. Specifically, we propose an analysis policy language, a restricted form of Datalog, to support users decomposing a static program analysis problem into several sub-problems that target simpler syntactic or semantic properties upon smaller code snippets. The problem decomposition enables the LLMs to target more manageable semantic-related sub-problems with reduced hallucinations, while the syntactic ones are resolved by parsing-based analysis without hallucinations. An analysis policy then is evaluated with lazy and incremental prompting, which significantly mitigates the hallucinations and improves the performance. We evaluate NESA for program slicing and bug detection upon benchmark and real-world programs. Evaluation results show that while NESA supports compilation-free and customizable analysis, it can still achieve comparable and even better performance than existing techniques. In a customized taint vulnerability detection upon TaintBench, for example, NESA achieves a precision of 66.27%, a recall of 78.57%, and an F1 score of 0.72, surpassing an industrial approach by 0.20 in F1 score. NESA also detects 13 real-world memory leak bugs, which have been fixed by developers.