# Security Prover

## 简介

Prover是一个动态扫描引擎，能够运行代码并探索其所有执行过程的状态空间。在探索过程中，Prover根据执行特征（如property变化和执行路径）来检测是否存在漏洞。同时，通过一些充分的约束条件，Prover能够证明代码中不包含某些关键漏洞，如 reentrancy。因此，Prover引擎既具有漏洞检测功能，又能验证代码中是否存在某些关键漏洞。

\
为实现Prover产品，我们构建了基于语义层的符号执行引擎，支持自动生成代码状态空间，并允许用户用Solidity编写Prover脚本以挖掘状态空间。

Prover的漏洞检测功能包括：编译合约文件生成AST树；动态执行语句，记录执行过程；最后依据状态空间、执行路径和内置规则判断是否存在漏洞。

Prover的安全性证明在获取状态空间后，定义各类漏洞的安全证明条件，如重入漏洞，从而证明代码中不会发生相应漏洞。

Prover的property证明通过用户自定义MAIN函数，验证合约执行过程中合约的property不会违反规则。

相比静态引擎，Prover具有更高的可靠性和更低的误报率，因为其分析的代码状态空间是真实可执行的。


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.metatrust.io/docs-zh/introduction/metascan/security-prover.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.