Security Prover

Introduction to the Security Prover scan engine

Prover is a dynamic scanning engine that runs code and explores the state space of all its execution processes. During exploration, Prover detects vulnerabilities based on execution characteristics such as property changes and execution paths. Meanwhile, Prover can prove the absence of critical vulnerabilities like reentrancy through sufficient constraint conditions. Thus, the Prover engine both detects vulnerabilities and verifies the existence of critical vulnerabilities in the code.

To implement the Prover product, we built a symbolic execution engine based on the semantic layer, supporting automatic generation of code state spaces and allowing users to write Prover scripts in Solidity to mine state spaces.

Prover's vulnerability detection includes: compiling contract files to generate AST trees, dynamically executing statements and recording the process. Finally, it determines whether there are vulnerabilities based on the state space, execution paths, and built-in rules.

Prover's safety proofs define safety proof conditions for each type of vulnerability, such as reentrancy, after obtaining the state space, thereby proving that corresponding vulnerabilities will not occur in the code.

Prover's property proofs use user-defined MAIN functions to verify that contract properties do not violate rules during contract execution.

Compared to static engines, Prover has higher reliability and lower false alarm rates because the code state spaces it analyzes are truly executable.