diff --git a/docs/cvl/index.md b/docs/cvl/index.md index a5e9dc5e..eb3c403f 100644 --- a/docs/cvl/index.md +++ b/docs/cvl/index.md @@ -35,4 +35,5 @@ Changes Since CVL 1 cvl2/changes.md cvl2/migration.md +v5-changes.md ``` diff --git a/docs/cvl/invariants.md b/docs/cvl/invariants.md index 192d5dcc..a63d74f9 100644 --- a/docs/cvl/invariants.md +++ b/docs/cvl/invariants.md @@ -11,7 +11,7 @@ verified by the Prover, but it may still be possible for the contract to violate it. The possible sources of unsoundness are {ref}`preserved`, {ref}`invariant-filters`, and {ref}`invariant-revert`. Invariant proofs are also unsound if some of the methods are filtered out using the -{ref}`--method` or {ref}`--contract` flags. See the linked sections for +{ref}`--method` or {ref}`--parametric_contracts` flags. See the linked sections for details. ``` diff --git a/docs/cvl/methods.md b/docs/cvl/methods.md index 89dff604..9d0f9cdd 100644 --- a/docs/cvl/methods.md +++ b/docs/cvl/methods.md @@ -48,7 +48,7 @@ method_spec ::= "function" [ "returns" "(" evm_types ")" ] [ "envfree" | "with" "(" "env" id ")" ] [ "optional" ] - [ "=>" method_summary [ "UNRESOLVED" | "ALL" ] ] + [ "=>" method_summary [ "" | "UNRESOLVED" | "ALL" | "DELETE" ] ] ";" exact_pattern ::= [ id "." ] id "(" evm_params ")" visibility [ "returns" "(" evm_types ")" ] @@ -335,6 +335,7 @@ There are several kinds of summaries available: - {ref}`auto-summary` are the default for unresolved calls. +(delete-summary)= ### Summary application To decide whether to summarize a given internal or external function call, the @@ -345,9 +346,16 @@ determine whether the call should be replaced by an approximation.[^dont-summari To determine whether a function call is replaced by an approximation, the Prover considers the context in which the function is called in addition to the application policy for its signature. If present, the application policy must -be either `ALL` or `UNRESOLVED`; the default policy is `ALL` with the exception -of `DISPATCHER` summaries, which have a default of `UNRESOLVED`. The decision -to replace a call by an approximation is made as follows: +be either `ALL`, `UNRESOLVED`, or `DELETE`; the default policy is `ALL` with the exception +of `DISPATCHER` summaries, which have a default of `UNRESOLVED`. + +A `DELETE` summary is similar to an `ALL` summary, except that the `DELETE` +summary removes the method from the {term}`scene` entirely. Calling the method +from CVL will produce a rule violation, and {term}`parametric rule`s will not +be instantiated on the deleted method. This can drastically improve +performance if the deleted method is complex. + +The decision to replace a call by an approximation is made as follows: * If the function is called from CVL rather than from contract code then it is never replaced by a summary. diff --git a/docs/cvl/rules.md b/docs/cvl/rules.md index ed411ccf..b2369bec 100644 --- a/docs/cvl/rules.md +++ b/docs/cvl/rules.md @@ -93,8 +93,10 @@ method that violates the rule, and will indicate if some contract methods always satisfy the rule. You can request that the Prover only run with specific methods using the -{ref}`--method` and {ref}`--contract` command line arguments. The set of +{ref}`--method` and {ref}`--parametric_contracts` command line arguments. The set of methods can also be restricted using {ref}`rule filters `. +The Prover will automatically skip any methods that have +{ref}`` `DELETE` summaries ``. If you wish to only invoke methods on a certain contract, you can call the `method` variable with an explicit receiver contract. The receiver must be a diff --git a/docs/cvl/v5-changes.md b/docs/cvl/v5-changes.md new file mode 100644 index 00000000..d042120d --- /dev/null +++ b/docs/cvl/v5-changes.md @@ -0,0 +1,338 @@ +Certora CLI 5.0 Changes +======================= + +The release of `certora-cli` version 5.0 introduces a few small breaking +changes for CVL. These changes improve the coverage for parametric rules and +invariants, disallow Solidity function calls in quantified expressions, +and simplify some rarely-used features. This document explains those changes +and how to work with them. + +```{note} +`certora-cli` 5.0 also includes several new features, bug fixes, and +performance improvements that are not discussed here; see {ref}`prover-release-notes` +for more details. +``` + +```{contents} +``` + +Exhaustive parametric rules +--------------------------- + +Starting with `certora-cli` version 5.0, {term}`parametric rule`s and +{term}`invariant`s will now be checked on the methods of all contracts by +default, instead of just the primary contract. + +This change improves the coverage of rules and can catch important errors. For +example, an invariant that relates a contract's total supply to its balance in +an underlying token contract could be invalidated by calling methods directly on +the underlying token; before this change those violations would not have been +detected. + +This change can break existing specifications in a few ways: + + - A property that should hold cannot be verified. + + - A parametric rule that was never intended to apply to secondary contracts + may be violated by methods of those contracts. + + - Verification may time out on methods of secondary contracts. + +The remainder of this section describes how to address these three failure +modes. + +```{contents} +:local: +``` + +### Fixing properties that should hold + +Most parametric rules and all invariants encode general properties of a system +that should be impossible for any contract to violate. For example, consider a +"solvency" invariant that shows that a vault contract holds enough underlying +tokens to cover any withdrawals: + +```cvl +invariant solvency() + underlying.balanceOf(currentContract) >= currentContract.totalSupply(); +``` + +Any violation of this property would be an important security vulnerability, +regardless of whether it is violated by a method of the vault or a method of +the underlying token. Therefore, it is important to check that no method of +any contract can violate these kinds of properties. However, sometimes +verifying these kinds of properties on methods of secondary contracts will +require additional work. + +Continuing the solvency example, the Prover is likely to find a violation of +the solvency rule in `underlying.transferFrom` where the vault contract has +given an allowance to a third party. If a third party has an allowance, it +will be able to reduce the vault's balance by transferring the vault's tokens +to itself. + +This violation represents an important vulnerability: if the vault mismanages +its allowances, then it may become insolvent. This violation shows that the +solvency of the vault depends on the correct management of its underlying +allowances. + +Therefore, to get the rule to pass, we will need to add another invariant +stating that the vault manages its allowances correctly: + +```cvl +invariant no_vault_allowance() + underlying.allowance(currentContract) == 0; +``` + +We can then use this invariant in the `preserved` block for the original +solvency rule. We are also likely to get violations from the case that the +vault contract itself calls methods on the underlying contract, so we rule that +out as well[^call-note]: + +[^call-note]: Adding this restriction does not ignore any actual contract + behaviors. If the vault does call methods on the underlying contract, it will + only do so from its code, and that call will be analyzed while the Prover is + verifying the calling method. The additional requirement only rules out + spurious counterexamples where the vault makes calls to the underlying token + without having code that does so. + +```cvl +invariant solvency() + underlying.balanceOf(currentContract) >= currentContract.totalSupply() + { + preserved with (env e) { + require e.msg.sender != currentContract; + requireInvariant no_vault_allowance(); + } + } +``` + +There is nothing new about this process of identifying violations and adding +new invariants as necessary; it is the same process you would use for analyzing +any violation. This example just shows that some work may be required when +verifying old specifications with `certora-cli` 5.0. + +The benefit is that by checking methods on secondary contracts, the Prover +forces us to consider a previously unstated assumptions about the contract and +write invariants that could detect important security vulnerabilities. For +this reason, you are encouraged to identify and prove additional invariants +to address counterexamples instead of using the filtering techniques described +in the following sections. + +### Filtering properties that should not be checked + +Some parametric rules encode properties that are only expected to hold on a +specific contract. For example, you might have a rule that ensures that every +successful method invocation is correctly authorized: + +```cvl +rule authorization_check(method f) +filtered { f -> f.isView } +{ + env e; calldataarg args; + + f(e,args); + + assert is_authorized(e.msg.sender, f.selector); +} +``` + +There is no reason to expect this property to hold on any contract besides the +main contract. + +To handle cases like these, `certora-cli` 5.0 introduces two new ways to filter +methods to a specific contract. + +The first and simplest way to restrict verification to a specific contract is +to call the `method` object with a specific receiver contract: + +```{code-block} cvl +:emphasize-lines: 6 + +rule authorization_check(method f) +filtered { f -> f.isView } +{ + env e; calldataarg args; + + currentContract.f(e,args); + + assert is_authorized(e.msg.sender, f.selector); +} +``` + +This syntax will add a filter that will only instantiate `f` with the methods +of `currentContract`. The receiver may be either `currentContract` or a +variable introduced by a `using` clause. + +The second and more flexible way is to use the new `contract` property of the +`method` variable: +```{code-block} cvl +:emphasize-lines: 2 + +rule authorization_check(method f) +filtered { f -> f.isView && f.contract == currentContract } +{ + env e; calldataarg args; + + f(e,args); + + assert is_authorized(e.msg.sender, f.selector); +} +``` + +If `f` is a `method` variable, `f.contract` refers to the contract that contains +the method `f`. + +(v5-contract-option)= +### Focusing on specific contracts + +If you want to focus verification on a specific contract, you can do so using +the {ref}`--parametric_contracts` option. This option takes a list of contracts and only +instantiates parametric rules and invariants on methods of those contracts. + +You can use this option to help transition specs to `certora-cli` 5.0; if `C` +is the main contract being verified, then passing `--parametric_contracts C` will cause +method variables to be instantiated in the same way the would have in older +versions. + +Disallow calls to contract functions in quantified expressions +-------------------------------------------------------------- + +Starting with `certora-cli` version 5.0, the Prover no longer supports +making contract method calls in quantified expression bodies by +default. + +For example, given the simple contract below, you can no longer +use the `method` `getI()` in a quantified expression body. + +```{code-block} solidity +contract example { + + uint i; + + function getI() public view returns (uint256) { + return i; + } +} +``` + +```{code-block} cvl +:emphasize-lines: 4 + +rule there_exists { + // Using getI() in the quantified body will now cause the Prover to + // generate a type-checking error. + require (exists uint256 i . i == getI()); + assert false, "Prover will generate an error before this line"; +} +``` + +In the example rule `there_exists`, the Prover will now generate an error similar +to the following: + +```text +Error in spec file (test2.spec:8:36): Contract function calls such as getI() +are disallowed inside quantified formulas. +``` + +In most simple cases, you can replace contract method calls with either a +{ref}direct storage access <...> or a {ref}ghost . For example the +above function `getI` simply returns the storage variable `i` and you can +change the `require` statement in the `there_exists` rule to use storage access: +`require (exists uint i . i == currentContract.i)`. To use a ghost, declare +the ghost and the hook that populates the ghost with the current value of +the contract variable `i`. + +```{code-block} cvl +ghost uint gI; + +hook Sstore i uint256 v STORAGE { + gI = v; +} +``` + +Finally, replace `getI` in the `require` statement in rule `there_exists` with the +ghost variable `gI`: `require (exists uint i . i == gI)`. + +If you must use contract method calls in quantified expressions, +you can still access the old behavior by specifying the +{ref}`--allow_solidity_calls_in_quantifiers` argument to `certoraRun` on the +command line. + + +Method variable restrictions +---------------------------- + +Starting with `certora-cli` version 5.0, you cannot declare new {ref}`method +variables ` anywhere except the top-level body of a rule. +Declaring new `method` variables inside of `if` statements, hook bodies, CVL +function bodies, preserved blocks, and all other contexts are all disallowed. + +You can still pass `method`-type variables as arguments to CVL functions and +definitions. You can use this feature to rewrite CVL functions that formerly +declared new `method` variables. + +For example, before `certora-cli` 5.0, the following CVL function was valid: + +```cvl +function call_arbitrary() { + method f; env e; calldataarg args; + f(e, args); +} + +rule r { + call_arbitrary(); + assert true; +} +``` + +The declaration of `f` inside of `call_arbitrary` is now disallowed, so `f` must +be passed into `call_arbitrary` instead of declared within it: + +```cvl +function call_arbitrary(method f) { + env e; calldataarg args; + f(e,args); +} + +rule r { + method f; + call_arbitrary(f); + assert true; +} +``` +New `DELETE` summary syntax +--------------------------- + +The syntax of the {ref}``new `DELETE` keyword `` in summaries +has changed. Prior to `certora-cli` 5.0, it was possible to call methods +summarized with `DELETE` summaries from spec, and the user had to annotate the +`DELETE` modifier to indicate how those calls should be treated. + +Starting with `certora-cli` 5.0, calling methods that have been summarized with +a `DELETE` summary is disallowed, and the `DELETE` annotation requires no +additional annotation. + +CLI changes: New Parametric Contracts Attribute +----------------------------------------------- + +As mentioned above the attribute `parametric_contracts` was added to `certora-cli` 5.0. +The attribute accepts the parametric contracts as a list of strings. +The attribute can be set as the CLI flag `--parametric_contracts` or in a `.conf` file. + +**Example** +CLI: + +`certoraRun C1.sol C2.sol C3.sol --parametric_contracts C1 C3 ...` + +Configuration file: + +`"files": [ "C1", "C2", "C3"], +"parametric_contracts": [ "C1", "C3"], +...` + +CLI changes: End of CVL1 Deprecation period +------------------------------------------- + +With the release of `certora-cli` version 5.0, we stop supporting +the CVL1 attributes that were deprecated during the transition to CVL2. +You can find the list of the deprecated attributes [here](https://docs.certora.com/en/latest/docs/cvl/cvl2/changes.html?highlight=cvl2#changes-to-the-command-line-interface-cli). diff --git a/docs/prover/changelog/prover_changelog.md b/docs/prover/changelog/prover_changelog.md index 010c8d51..6c2c4cf8 100644 --- a/docs/prover/changelog/prover_changelog.md +++ b/docs/prover/changelog/prover_changelog.md @@ -1,9 +1,11 @@ +(prover-release-notes)= Prover Release Notes ============= ```{contents} ``` + 4.12.1 (September 17, 2023) --------------------------- diff --git a/docs/prover/cli/options.md b/docs/prover/cli/options.md index 1a508b52..6e5e5825 100644 --- a/docs/prover/cli/options.md +++ b/docs/prover/cli/options.md @@ -134,8 +134,8 @@ certoraRun --method 'deposit(uint)' Note that many shells will interpret the `(` and `)` characters specially, so the method signature argument will usually need to be quoted as in the example. -(--contract)= -### `--contract ...` +(--parametric_contracts)= +### `--parametric_contracts ...` ```{versionadded} 5.0 Prior to version 5, method variables and invariants were only instantiated with @@ -158,7 +158,7 @@ counterexample in a method of the `Underlying` contract defined in the file ```sh certoraRun Main:Example.sol Underlying:Example.sol --verify Main:Example.spec \ - --contract Underlying + --parametric_contracts Underlying ``` (--send_only)= @@ -769,6 +769,23 @@ setting or encoding that models precisely both bitwise operations and `mathint`. This option sets the number of program points to test with the `deepSanity` built-in rule. See {ref}`built-in-deep-sanity`. +(--allow_solidity_calls_in_quantifiers)= +### --allow_solidity_calls_in_quantifiers + +**What does it do?** + +Instructs the Prover to permit contract method calls in quantified expression +bodies. + +**When to use it?** + +Upon instruction from the Certora team. + +**Example** + +`--allow_solidity_calls_in_quantifiers` instructs the Prover to not generate an +error on encountering contract method calls in quantified expression bodies. + (control-flow-splitting-options)= Advanced options that control control flow splitting