  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 prop- erty for a
given code. While this basic process is relatively straight- forward, ensuring
that the generated properties are (i) compilable, (ii) appropriate, and (iii)
runtime-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 prop- erties. We
have implemented these strategies into a novel system called PropertyGPT, with
623 human-written properties collected from 23 Certora projects. 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, resulting in $8,256 bug bounty rewards.
