fd812ee954
Co-authored-by: futreall <86553580+futreall@users.noreply.github.com> Co-authored-by: Marco <wudmytrotest200@gmail.com> Co-authored-by: Dmitry <98899785+mdqst@users.noreply.github.com> Co-authored-by: Dmytrol <46675332+Dimitrolito@users.noreply.github.com> Co-authored-by: Noisy <125606576+donatik27@users.noreply.github.com> Co-authored-by: Danil <37103154+Danyylka@users.noreply.github.com> Co-authored-by: CrazyFrog <anna.shuraeva13@gmail.com> Co-authored-by: Bryer <0xbryer@gmail.com> Co-authored-by: Viktor Pavlik <160131789+Vikt0rPavlik@users.noreply.github.com> Co-authored-by: Skylar Ray <137945430+sky-coderay@users.noreply.github.com> Co-authored-by: Brawn <nftdropped@gmail.com> Co-authored-by: fuder.eth <139509124+vtjl10@users.noreply.github.com> Co-authored-by: FT <140458077+zeevick10@users.noreply.github.com> Co-authored-by: Ann Wagner <chant_77_swirly@icloud.com> Co-authored-by: Hopium <135053852+Hopium21@users.noreply.github.com> Co-authored-by: Arr00 <13561405+arr00@users.noreply.github.com> Co-authored-by: Hadrien Croubois <hadrien.croubois@gmail.com>
61 lines
3.1 KiB
Markdown
61 lines
3.1 KiB
Markdown
# Running the certora verification tool
|
|
|
|
These instructions detail the process for running Certora Verification Tool on OpenZeppelin Contracts.
|
|
|
|
Documentation for CVT and the specification language is available [here](https://certora.atlassian.net/wiki/spaces/CPD/overview).
|
|
|
|
## Prerequisites
|
|
|
|
Follow the [Certora installation guide](https://docs.certora.com/en/latest/docs/user-guide/getting-started/install.html) in order to get the Certora Prover Package and the `solc` executable folder in your path.
|
|
|
|
> **Note**
|
|
> An API Key is required for local testing. Although the prover will run on a GitHub Actions' CI environment on selected Pull Requests.
|
|
|
|
## Running the verification
|
|
|
|
The Certora Verification Tool proves specs for contracts, which are defined by the `./specs.json` file along with their pre-configured options.
|
|
|
|
The verification script `./run.js` is used to submit verification jobs to the Certora Verification service.
|
|
|
|
You can run it from the root of the repository with the following command:
|
|
|
|
```bash
|
|
node certora/run.js [[CONTRACT_NAME:]SPEC_NAME] [OPTIONS...]
|
|
```
|
|
|
|
Where:
|
|
|
|
- `CONTRACT_NAME` matches the `contract` key in the `./spec.json` file and may be empty. It will run all matching contracts if not provided.
|
|
- `SPEC_NAME` refers to a `spec` key from the `./specs.json` file. It will run every spec if not provided.
|
|
- `OPTIONS` extend the [Certora Prover CLI options](https://docs.certora.com/en/latest/docs/prover/cli/options.html#certora-prover-cli-options) and will respect the preconfigured options in the `specs.json` file.
|
|
|
|
> **Note**
|
|
> A single spec may be configured to run for multiple contracts, whereas a single contract may run multiple specs.
|
|
|
|
Example usage:
|
|
|
|
```bash
|
|
node certora/run.js AccessControl # Run the AccessControl spec against every contract implementing it
|
|
```
|
|
|
|
## Adapting to changes in the contracts
|
|
|
|
Some of our rules require the code to be simplified in various ways. Our primary tool for performing these simplifications is to run verification on a contract that extends the original contracts and overrides some of the methods. These "harness" contracts can be found in the `certora/harness` directory.
|
|
|
|
This pattern does require some modifications to the original code: some methods need to be made virtual or public, for example. These changes are handled by applying a patch
|
|
to the code before verification by running:
|
|
|
|
```bash
|
|
make -C certora apply
|
|
```
|
|
|
|
Before running the `certora/run.js` script, it's required to apply the corresponding patches to the `contracts` directory, placing the output in the `certora/patched` directory. Then, the contracts are verified by running the verification for the `certora/patched` directory.
|
|
|
|
If the original contracts change, it is possible to create a conflict with the patch. In this case, the verify scripts will report an error message and output rejected changes in the `patched` directory. After merging the changes, run `make record` in the `certora` directory; this will regenerate the patch file, which can then be checked into git.
|
|
|
|
For more information about the `make` scripts available, run:
|
|
|
|
```bash
|
|
make -C certora help
|
|
```
|