PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation

TL;DR

This paper introduces PropertyGPT, a novel LLM-based tool that automatically generates, refines, and verifies smart contract properties, significantly improving property coverage and vulnerability detection in blockchain security.

Contribution

It presents a new retrieval-augmented approach for property generation, integrating static analysis feedback and formal verification to enhance accuracy and reliability.

Findings

Achieved 80% recall in property generation compared to ground truth.

Detected 26 CVEs and 12 zero-day vulnerabilities in tested smart contracts.

Uncovered vulnerabilities leading to over $8,000 in bug bounty rewards.

Abstract

With recent advances in large language models (LLMs), this paper explores the potential of leveraging state-of-the-art LLMs,such as GPT-4, to transfer existing human-written properties (e.g.,those from Certora auditing reports) and automatically generate customized properties for unknown code. To this end, we embed existing properties into a vector database and retrieve a reference property for LLM-based in-context learning to generate a new property for a given code. While this basic process is relatively straightforward, ensuring that the generated properties are (i) compilable, (ii) appropriate, and (iii) verifiable presents challenges. To address (i), we use the compilation and static analysis feedback as an external oracle to guide LLMs in iteratively revising the generated properties. For (ii), we consider multiple dimensions of similarity to rank the properties and employ a weighted algorithm to identify the top-K properties as the final result. For (iii), we design a dedicated prover to formally verify the correctness of the generated properties. We have implemented these strategies into a novel LLM-based property generation tool called PropertyGPT. Our experiments show that PropertyGPT can generate comprehensive and high-quality properties, achieving an 80% recall compared to the ground truth. It successfully detected 26 CVEs/attack incidents out of 37 tested and also uncovered 12 zero-day vulnerabilities, leading to $8,256 in bug bounty rewards.