diff --git a/CLIFlags/README.md b/CLIFlags/README.md new file mode 100644 index 00000000..fbd1bf01 --- /dev/null +++ b/CLIFlags/README.md @@ -0,0 +1,33 @@ +# Examples of CLI Flags for certoraRun + +This is an index of some of the CLI flags available in the certoraRun command along with some examples of runs. Each flag links to its corresponding documentation over at Certora Docs. In this folder you can also see some confs called `.conf` with examples of these flags on some of the other examples available in this repository. + +For more information about available CLI options go to: https://docs.certora.com/en/latest/docs/prover/cli/options.html + +| Flag | Examples | +| ---- | -------- | +| [--verify](https://docs.certora.com/en/latest/docs/prover/cli/options.html#verify) | Every run uses verify ([e.g.](https://prover.certora.com/output/15800/83116717cc7a48f5b53172666a83817e?anonymousKey=0a5ee559275dcb173b18a69caeda4f33a2b8f014)). | +| [--msg](https://docs.certora.com/en/latest/docs/prover/cli/options.html#msg-description) | [Run with a message.](https://prover.certora.com/output/15800/1aa5389f01604c33817e4f9ccf2f70fc?anonymousKey=e6f6fbe19097097df6851846847f5139b930b394) | +| [--rule](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#rule-rule-name) | [An ERC20 run.](https://prover.certora.com/output/15800/21e87636bbdc4f1783c467c70bffbd32?anonymousKey=23b497245d7c1614db30315093f2cd34900f99f9) / [Selecting only 1 rule.](https://prover.certora.com/output/15800/c554c7baf7534fe0940c98c60883bc6f?anonymousKey=1cef55a4c343c50c82b40d7c400ae185ede867d8) | +| [--method](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#method-method-signature) | [An ERC20 run.](https://prover.certora.com/output/15800/21e87636bbdc4f1783c467c70bffbd32?anonymousKey=23b497245d7c1614db30315093f2cd34900f99f9) / [Only 1 method used.](https://prover.certora.com/output/15800/3cf9410d78014c2f91835a5f8aa60767?anonymousKey=8392f2471d7507a21fd990a19ad0611592261f1e) | +| [--parametric_contracts](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#parametric-contracts-contract-name) | [A LiquidityPool run without specifying.](https://prover.certora.com/output/15800/7ba2e8562afd4a5782f282059a0c1f00?anonymousKey=e12b94385957f1ebb14c0c1d8a77ec6f8765da7a) / [With specifying a contract.](https://prover.certora.com/output/15800/309c9ba5749e41b6b5a8b151ab3dd616?anonymousKey=44524f6189d23054e528c2a3ba97cc21112194fd) | +| [--multi_assert_check](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#multi-assert-check) | [false](https://prover.certora.com/output/15800/e11354b5e03441cc9ac1d210fe686347?anonymousKey=911ba098228465f7c6fc0ba1d4d40cbde83bef94) / [true](https://prover.certora.com/output/15800/23c97944b0074bebb7e79ad4cd852984?anonymousKey=6e4c43f376883162646e5c61101abdcf36131c4e) | +| [--independent_satisfy](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#independent-satisfy) | | +| [--rule_sanity](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#rule-sanity) | [none](https://prover.certora.com/output/15800/16fdf7aa282243e591889d9ec27a71ef?anonymousKey=6bdd16c5780e0127246ddc3eea3ee8a22c9729b8) / [basic](https://prover.certora.com/output/15800/2c5aa93c4bc54a939dea395202c0e47c?anonymousKey=bf07b5bdc3a7c7b28fda762942b02456731d2371) / [advanced](https://prover.certora.com/output/15800/e44ef408e1794a8fa32178f63fbe83da?anonymousKey=4afd4e7f98fc3d11d03b0a8522d417a2671f70fe) | +| [--solc](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc) | [ERC20 compiled with solc8.0](https://prover.certora.com/output/15800/aa8e3c59b7434058a1f0927f6cd1da77?anonymousKey=099deb423f4cb86913f8a536309ea8a64511ca46) / [compiled with solc8.10](https://prover.certora.com/output/15800/c67c4072730d40f7b081556ddf78334e?anonymousKey=e9d7ffddc9f338e3a865505fbbe18f095823ae43) | +| [--solc_map](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-map) | | +| [--solc_optimize](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-optimize) | | +| [--solc_via_ir](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-via-ir) | [false](https://prover.certora.com/output/15800/83116717cc7a48f5b53172666a83817e?anonymousKey=0a5ee559275dcb173b18a69caeda4f33a2b8f014) / [true](https://prover.certora.com/output/15800/4a29b3f21b884b8d8fc5550f61fa45b7?anonymousKey=f1909b5b181ae4534377501a3c06c896bfff2d67) | +| [--solc_evm_version](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-evm-version) | [ERC20 with Berlin](https://prover.certora.com/output/15800/1d55dc0613b444f2a690fce8f645d9d1?anonymousKey=9efa9f0b59bfc8c37aa7c9d0d8573c9d99f1c2cf) / [ERC20 with London](https://prover.certora.com/output/15800/115e1f215f344fefb7dd389cb4db9d9f?anonymousKey=75c515fd97ff0ae21b887b5915db180d807dc9d2) | +| [--solc_allow_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#solc-allow-path) | Every conf example in this folder has it. | +| [--packages_path](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages-path) | | +| [--packages](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#packages) | | +| [--optimistic_loop](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-loop) | [false](https://prover.certora.com/output/15800/8db8b5eaeb244ba490394e05edac0fe1?anonymousKey=5067d0c0908cc2f1cb348e8b163bfec327884cee) / [true](https://prover.certora.com/output/15800/89e59b62f44f439c9502363cef4e7b49?anonymousKey=bac549ca44168b6e0b282a980240c247b34d77ee) | +| [--loop_iter](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#loop-iter) | [A run with 1 loop unrolling](https://prover.certora.com/output/15800/9b085d85bcc345d5bd2612f8bea5da98?anonymousKey=a6c544d73525dcb582eba2b971d85d97c16b35db) / [Same run with 3 loop unrolling](https://prover.certora.com/output/15800/0b152fe8cfcc41168429a287fa2ba7f8?anonymousKey=38fd94f0ac9bd36f3cecb23d8275b23b864e2d77) | +| [--optimistic_summary_recursion](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-summary-recursion) | | +| [--summary_recursion_limit](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#summary-recursion-limit) | | +| [--optimistic_hashing](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#optimistic-hashing) | | +| [--hashing_length_bound](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#hashing-length-bound) | | +| [--link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#link) | [Liquidity Pool without linking](https://prover.certora.com/output/15800/e80f04180604458597fecc47c2b64e74?anonymousKey=b893bb90a8858acf903ba4aff1006af89a96d188) / [With linking](https://prover.certora.com/output/15800/f8f4b7a9180b49c1acdff4111a3c8e7a?anonymousKey=4a5b9ea156448922f7a1b4a25311d2b1e5c676ad) | +| [--address](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#address) | | +| [--struct_link](https://docs.certora.com/en/latest/docs/prover/cli/options.html?highlight=bank#struct-link) | | \ No newline at end of file diff --git a/CLIFlags/link.conf b/CLIFlags/link.conf new file mode 100644 index 00000000..c82e46f9 --- /dev/null +++ b/CLIFlags/link.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "../DEFI/LiquidityPool/contracts/Pool.sol", + "../DEFI/LiquidityPool/contracts/Asset.sol", + "../DEFI/LiquidityPool/certora/harness/TrivialReceiver.sol" + ], + "verify": "Pool:../DEFI/LiquidityPool/certora/specs/Full.spec", + // Link a field in the contract to another contract. + "link": [ + "Pool:asset=Asset" + ], + + "parametric_contracts": ["Pool"], + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/loop_iter.conf b/CLIFlags/loop_iter.conf new file mode 100644 index 00000000..283210fc --- /dev/null +++ b/CLIFlags/loop_iter.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "../CVLByExample/NativeBalances/contracts/Auction.sol", + ], + "verify": "Auction:../CVLByExample/NativeBalances/certora/specs/Auction.spec", + // Set number of loop unrolling for loops. + "loop_iter": "3", + + "optimistic_loop": true, + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/method.conf b/CLIFlags/method.conf new file mode 100644 index 00000000..8701c6cd --- /dev/null +++ b/CLIFlags/method.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "../DEFI/ERC20/contracts/ERC20.sol" + ], + "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec", + // Use only specific method for parametric rules and invariants. + "method": "transfer(address,uint256)", + + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/msg.conf b/CLIFlags/msg.conf new file mode 100644 index 00000000..3f60816c --- /dev/null +++ b/CLIFlags/msg.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "../CVLByExample/Invariant/contracts/BallGame.sol:BallGame" + ], + "verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec", + // Add a message. + "msg": "This run will have a message :)", + + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/multi_assert_check.conf b/CLIFlags/multi_assert_check.conf new file mode 100644 index 00000000..3924defd --- /dev/null +++ b/CLIFlags/multi_assert_check.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "../CVLByExample/Optional/contracts/Base.sol", + "../CVLByExample/Optional/contracts/Base.sol:Partial", + ], + "verify": "Base:../CVLByExample/Optional/certora/specs/Base.spec", + // Enable multi asserts. + "multi_assert_check": true, + + "solc_allow_path": "../" +} diff --git a/CLIFlags/optimistic_loop.conf b/CLIFlags/optimistic_loop.conf new file mode 100644 index 00000000..1b73c9f2 --- /dev/null +++ b/CLIFlags/optimistic_loop.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "../DEFI/ERC20/contracts/ERC20.sol" + ], + "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec", + // Consider only paths in which the loop unwind condition holds. + "optimistic_loop": true, + + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/parametric_contract.conf b/CLIFlags/parametric_contract.conf new file mode 100644 index 00000000..47adf846 --- /dev/null +++ b/CLIFlags/parametric_contract.conf @@ -0,0 +1,15 @@ +{ + "files": [ + "../DEFI/LiquidityPool/contracts/Pool.sol", + "../DEFI/LiquidityPool/contracts/Asset.sol", + "../DEFI/LiquidityPool/certora/harness/TrivialReceiver.sol" + ], + "verify": "Pool:../DEFI/LiquidityPool/certora/specs/Full.spec", + // Specify on which contracts to run parametric rules. + "parametric_contracts": ["Pool"], + + "link": [ + "Pool:asset=Asset" + ], + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/rule.conf b/CLIFlags/rule.conf new file mode 100644 index 00000000..76a33598 --- /dev/null +++ b/CLIFlags/rule.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "../DEFI/ERC20/contracts/ERC20.sol" + ], + "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec", + // Select only a specific rule. + "rule": [ + "mintIntegrity" + ], + + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/rule_sanity.conf b/CLIFlags/rule_sanity.conf new file mode 100644 index 00000000..b3ea3dc9 --- /dev/null +++ b/CLIFlags/rule_sanity.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "../CVLByExample/Optional/contracts/Base.sol", + "../CVLByExample/Optional/contracts/Base.sol:Partial", + ], + "verify": "Base:../CVLByExample/Optional/certora/specs/Base.spec", + // Perform sanity check, set to none/basic/advanced. + "rule_sanity": "advanced", + + "solc_allow_path": "../" +} diff --git a/CLIFlags/solc.conf b/CLIFlags/solc.conf new file mode 100644 index 00000000..c863aead --- /dev/null +++ b/CLIFlags/solc.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "../DEFI/ERC20/contracts/ERC20.sol" + ], + "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec", + // Set the Solidity compiler version used. + "solc": "solc8.10", + + "optimistic_loop": true, + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/solc_evm_version.conf b/CLIFlags/solc_evm_version.conf new file mode 100644 index 00000000..b7be2d65 --- /dev/null +++ b/CLIFlags/solc_evm_version.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "../DEFI/ERC20/contracts/ERC20.sol" + ], + "verify": "ERC20:../DEFI/ERC20/certora/specs/ERC20Full.spec", + // Set the EVM version used. + "solc_evm_version": "london", + + "optimistic_loop": true, + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/solc_via_ir.conf b/CLIFlags/solc_via_ir.conf new file mode 100644 index 00000000..ad68801d --- /dev/null +++ b/CLIFlags/solc_via_ir.conf @@ -0,0 +1,10 @@ +{ + "files": [ + "../CVLByExample/Invariant/contracts/BallGame.sol:BallGame" + ], + "verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec", + // Enable IR based code generator. + "solc_via_ir": true, + + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CLIFlags/verify.conf b/CLIFlags/verify.conf new file mode 100644 index 00000000..b4d2f720 --- /dev/null +++ b/CLIFlags/verify.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "../CVLByExample/Invariant/contracts/BallGame.sol:BallGame" + ], + // Verify BallGame contract against the specified spec. + "verify": "BallGame:../CVLByExample/Invariant/certora/specs/BallGameCorrect.spec", + + "solc_allow_path": "../" +} \ No newline at end of file diff --git a/CVLByExample/Ecrecover/Fullecrecover.conf b/CVLByExample/Ecrecover/Fullecrecover.conf new file mode 100644 index 00000000..27544cee --- /dev/null +++ b/CVLByExample/Ecrecover/Fullecrecover.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "Verify.sol" + ], + "optimistic_hashing": true, + "rule_sanity": "advanced", + "verify": "Verify:ecrecover.spec" +} \ No newline at end of file diff --git a/CVLByExample/Ecrecover/ManualMutation/VerifyBug1.sol b/CVLByExample/Ecrecover/ManualMutation/VerifyBug1.sol new file mode 100644 index 00000000..b0d7f96d --- /dev/null +++ b/CVLByExample/Ecrecover/ManualMutation/VerifyBug1.sol @@ -0,0 +1,70 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +// game developer depoloys contract +contract Verify { + + function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external returns (bool) { + return ecrecover(msgHash, v, r, s) == _addr; + } + + +mapping (address => uint256) private nonces; + +function executeMyFunctionFromSignature( + uint8 v, + bytes32 r, + bytes32 s, + address owner, + uint256 myParam, + uint256 deadline +) external { + + bytes32 hash = getHash(owner, myParam, deadline); + + + address signer = ecrecover(hash, v, r, s); + require(signer == owner, "MyFunction: invalid signature"); + require(signer != address(0), "ECDSA: invalid signature"); + + require(block.timestamp < deadline, "MyFunction: signed transaction expired"); + // nonces[owner]++; // forgeting to update the nonces will result in possible multiple execution + + _myFunction(owner, myParam); +} + +function _myFunction(address owner, uint256 myParam) internal { + +} + +function getHash( + address owner, + uint256 myParam, + uint256 deadline +) public returns(bytes32) { + bytes32 eip712DomainHash = keccak256( + abi.encode( + keccak256( + "EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)" + ), + keccak256(bytes("MyContractName")), + keccak256(bytes("1")), + address(this) + ) + ); + + bytes32 hashStruct = keccak256( + abi.encode( + keccak256("MyFunction(address owner,uint256 myParam,uint256 nonce,uint256 deadline)"), + owner, + myParam, + nonces[owner], + deadline + ) + ); + + return keccak256(abi.encodePacked("\x19\x01", eip712DomainHash, hashStruct)); +} + + +} \ No newline at end of file diff --git a/CVLByExample/Ecrecover/ManualMutation/VerifyBug2.sol b/CVLByExample/Ecrecover/ManualMutation/VerifyBug2.sol new file mode 100644 index 00000000..2e81e4cc --- /dev/null +++ b/CVLByExample/Ecrecover/ManualMutation/VerifyBug2.sol @@ -0,0 +1,68 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +// game developer depoloys contract +contract Verify { + + function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external returns (bool) { + return ecrecover(msgHash, v, r, s) == _addr; + } + + +mapping (address => uint256) private nonces; + +function executeMyFunctionFromSignature( + uint8 v, + bytes32 r, + bytes32 s, + address owner, + uint256 myParam, + uint256 deadline +) external { + + bytes32 hash = getHash(/*owner*/ msg.sender, myParam, deadline); // computing the has on the wrong address + + + address signer = ecrecover(hash, v, r, s); + require(signer == owner, "MyFunction: invalid signature"); + require(signer != address(0), "ECDSA: invalid signature"); + + require(block.timestamp < deadline, "MyFunction: signed transaction expired"); + nonces[owner]++; + + _myFunction(owner, myParam); +} + +function _myFunction(address owner, uint256 myParam) internal { + +} + +function getHash( + address owner, + uint256 myParam, + uint256 deadline +) public returns(bytes32) { + bytes32 eip712DomainHash = keccak256( + abi.encode( + keccak256( + "EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)" + ), + keccak256(bytes("MyContractName")), + keccak256(bytes("1")), + address(this) + ) + ); + + bytes32 hashStruct = keccak256( + abi.encode( + keccak256("MyFunction(address owner,uint256 myParam,uint256 nonce,uint256 deadline)"), + owner, + myParam, + nonces[owner], + deadline + ) + ); + + return keccak256(abi.encodePacked("\x19\x01", eip712DomainHash, hashStruct)); +} +} \ No newline at end of file diff --git a/CVLByExample/Ecrecover/Readme.md b/CVLByExample/Ecrecover/Readme.md new file mode 100644 index 00000000..842861cd --- /dev/null +++ b/CVLByExample/Ecrecover/Readme.md @@ -0,0 +1,71 @@ +# Ercecover Example + +## Overview +This repository contains a smart contract named `Verify` that implements a signature verification mechanism using the `ecrecover` function. The contract includes a function `executeMyFunctionFromSignature` that allows a user to execute a specific function if the provided signature is valid. The example demonstrates new CVL feature which is cvl function version of the same ercecover function implemented in CVL. + +## Executions + +1. **Certora Run for ecrecover** + - Command: + ```bash + certoraRun Fullecrecover.conf --server production --prover_version master + ``` + - Execution Link: [Certora Run Output](https://prover.certora.com/output/1512/01ce19bfd3fa4a3b98e216bf2c085c24?anonymousKey=f85d1e9348a4e5f8293700660f90f41eb96aa83e) + +2. **Certora Mutate** + - Command: + ```bash + certoraMutate --mutation_conf mutation.mconf --prover_conf Fullecrecover.conf --server production + ``` + - Mutation Link: [Certora Mutate Output](https://mutation-testing.certora.com/?id=71f2ffd2-80ea-47b5-b3b9-29cc73c91752&anonymousKey=d3f0379a-9a60-4b34-9edb-7210e763a91e) + +The mutation execution contains 2 manual injection bugs locating under ManualMutation folder. + +## Smart Contract + +The smart contract, `Verify`, provides a method `isSigned` for signature verification and `executeMyFunctionFromSignature` for executing a function based on a valid signature. It also includes a method `getHash` for generating a hash used in the signature process. + +The contract follows the EIP-712 standard for domain separation and signature verification. The functions implement checks for signature uniqueness, zero value, determinism, and dependencies on `r` and `s`. + +## Certora Verification Language (CVL) Properties + +### ecrecover Properties + +1. **Zero Value** + - `ecrecover(0, v, r, s) == 0` + +2. **Deterministic** + - `ecrecover(msgHash, v, r, s) == _addr` on different calls + +3. **Uniqueness of Signature** + - `ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash', v, r, s) == 0` where `msgHash' != msgHash` + +4. **Dependency on r and s** + - `ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash, v, r', s) == 0` where `r' != r` + - `ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash, v, r, s') == 0` where `s' != s` + +### High-Level Properties + +1. **Single Verifier** + - A single address can verify a signature, and different addresses cannot verify the same signature. + +2. **Owner Signature Uniqueness** + - For a given address, two different messages cannot have the same valid signature. + +3. **Hash Uniqueness** + - Two different sets of parameters result in unique hash values. + +4. **Only Single User Can Execute** + - Only a single user, specified by the address, can successfully execute a function. + +5. **Signed Params and Deadline** + - The parameters and deadlines signed by the same address are the same. + +6. **Two Different Signatures** + - Two different messages signed by the same address have different signatures. + +7. **Signed Messages Executed Once** + - Once a message is executed, it cannot be executed again. + + +For a comprehensive guide on Certora Verification Language, refer to [Certora Documentation](https://docs.certora.com). \ No newline at end of file diff --git a/CVLByExample/Ecrecover/Verify.sol b/CVLByExample/Ecrecover/Verify.sol new file mode 100644 index 00000000..7e181f63 --- /dev/null +++ b/CVLByExample/Ecrecover/Verify.sol @@ -0,0 +1,70 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.0; + +// game developer depoloys contract +contract Verify { + + function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external returns (bool) { + return ecrecover(msgHash, v, r, s) == _addr; + } + + +mapping (address => uint256) private nonces; + +function executeMyFunctionFromSignature( + uint8 v, + bytes32 r, + bytes32 s, + address owner, + uint256 myParam, + uint256 deadline +) external { + + bytes32 hash = getHash(owner, myParam, deadline); + + + address signer = ecrecover(hash, v, r, s); + require(signer == owner, "MyFunction: invalid signature"); + require(signer != address(0), "ECDSA: invalid signature"); + + require(block.timestamp < deadline, "MyFunction: signed transaction expired"); + nonces[owner]++; + + _myFunction(owner, myParam); +} + +function _myFunction(address owner, uint256 myParam) internal { + +} + +function getHash( + address owner, + uint256 myParam, + uint256 deadline +) public returns(bytes32) { + bytes32 eip712DomainHash = keccak256( + abi.encode( + keccak256( + "EIP712Domain(string name,string version,uint256 chainId,address verifyingContract)" + ), + keccak256(bytes("MyContractName")), + keccak256(bytes("1")), + address(this) + ) + ); + + bytes32 hashStruct = keccak256( + abi.encode( + keccak256("MyFunction(address owner,uint256 myParam,uint256 nonce,uint256 deadline)"), + owner, + myParam, + nonces[owner], + deadline + ) + ); + + return keccak256(abi.encodePacked("\x19\x01", eip712DomainHash, hashStruct)); +} + + +} \ No newline at end of file diff --git a/CVLByExample/Ecrecover/ecrecover.spec b/CVLByExample/Ecrecover/ecrecover.spec new file mode 100644 index 00000000..6d75da2a --- /dev/null +++ b/CVLByExample/Ecrecover/ecrecover.spec @@ -0,0 +1,278 @@ +/*** +This example explains many features of Certora Verification Language. +See https://docs.certora.com for a complete guide. + +Example for ecrecover +***/ + +/* + Declaration of methods that are used in the rules. envfree indicate that + the method is not dependent on the environment (msg.value, msg.sender). + Methods that are not declared here are assumed to be dependent on env. +*/ + + +/*** # ecrecover properties: +# 1. zero value: + ecrecover(0, v, r, s) == 0 +# 2. deterministic + ecrecover(msgHash, v, r, s) == _addr on different calls. +# 3. uniqueness of signature + ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash', v, r, s) == 0 + where msgHash' != msgHash +# 4. Dependency on r and s + ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash, v, r', s) == 0 + where r' != r + ecrecover(msgHash, v, r, s) != 0 => ecrecover(msgHash, v, r, s') == 0 + where s' != s +**/ + + + +methods { + function isSigned(address _addr, bytes32 msgHash, uint8 v, bytes32 r, bytes32 s) external returns (bool) envfree; + function executeMyFunctionFromSignature(uint8 v, bytes32 r, bytes32 s, address owner, uint256 myParam, uint256 deadline) external; + function getHash(address owner, uint256 myParam, uint256 deadline) external returns(bytes32) envfree; +} + + +function ecrecoverAxioms() { + // zero value: + require (forall uint8 v. forall bytes32 r. forall bytes32 s. ecrecover(to_bytes32(0), v, r, s) == 0); + // uniqueness of signature + require (forall uint8 v. forall bytes32 r. forall bytes32 s. forall bytes32 h1. forall bytes32 h2. + h1 != h2 => ecrecover(h1, v, r, s) != 0 => ecrecover(h2, v, r, s) == 0); + // dependency on r and s + require (forall bytes32 h. forall uint8 v. forall bytes32 s. forall bytes32 r1. forall bytes32 r2. + r1 != r2 => ecrecover(h, v, r1, s) != 0 => ecrecover(h, v, r2, s) == 0); + require (forall bytes32 h. forall uint8 v. forall bytes32 r. forall bytes32 s1. forall bytes32 s2. + s1 != s2 => ecrecover(h, v, r, s1) != 0 => ecrecover(h, v, r, s2) == 0); +} + +/* + shows that ecrecover has a single value, i.e two different addresses can not be the result of ecrecover(msgHash, v, r, s) +*/ +rule zeroValue() { + ecrecoverAxioms(); + bytes32 msgHash; uint8 v; bytes32 r; bytes32 s; + assert ecrecover(to_bytes32(0), v, r, s ) == 0; +} + + + + +rule deterministic() { + ecrecoverAxioms(); + bytes32 msgHash; uint8 v; bytes32 r; bytes32 s; + assert ecrecover(msgHash, v, r, s ) == ecrecover(msgHash, v, r, s ); +} + +rule uniqueness() { + ecrecoverAxioms(); + bytes32 msgHashA; bytes32 msgHashB; uint8 v; bytes32 r; bytes32 s; + require msgHashA != msgHashB; + assert ecrecover(msgHashA, v, r, s) != 0 => ecrecover(msgHashB, v, r, s) == 0; +} + +rule dependencyOnS() { + ecrecoverAxioms(); + bytes32 msgHash; uint8 v; bytes32 r; bytes32 s1; bytes32 s2; + require s1 != s2; + assert ecrecover(msgHash, v, r, s1) != 0 => ecrecover(msgHash, v, r, s2) == 0; + //!= ecrecover(msgHash, v, r, s1) ; +} + +rule dependencyOnR() { + ecrecoverAxioms(); + bytes32 msgHash; uint8 v; bytes32 r1; bytes32 r2; bytes32 s; + require r1 != r2; + assert ecrecover(msgHash, v, r1, s) != 0 => ecrecover(msgHash, v, r2, s) == 0 ; +} + +// Rules for a function that checks signature + +rule singleVerifier () +{ + ecrecoverAxioms(); + bytes32 msgHash; uint8 v; bytes32 r; bytes32 s; + address addr1; + address addr2; + require addr1 != addr2 && addr1!=0 && addr2!=0 ; + assert isSigned(addr1, msgHash, v, r, s ) => !isSigned(addr2, msgHash, v, r, s ) ; + +} + + +rule ownerSignatureIsUnique () { + ecrecoverAxioms(); + bytes32 msgHashA; bytes32 msgHashB; + uint8 v; bytes32 r; bytes32 s; + address addr; + require msgHashA != msgHashB; + require addr != 0; + assert isSigned(addr, msgHashA, v, r, s ) => !isSigned(addr, msgHashB, v, r, s ); +} + +rule hashIsUnique( + address ownerA, + uint256 myParamA, + uint256 deadlineA, + address ownerB, + uint256 myParamB, + uint256 deadlineB +) { + bytes32 hashA = getHash(ownerA, myParamA, deadlineA); + bytes32 hashB = getHash(ownerB, myParamB, deadlineB); + assert hashA == hashB => ( ownerA == ownerB && + myParamA == myParamB && + deadlineA == deadlineB ); +} + + +/*** + # High level property : there is only single owner that can be used + A rule which proves that for a given set of parameters only a single owner can execute . + This property is implemented as a relational property - it compares two different executions on the same state. +*/ +rule onlySingleUserCanExecute(uint8 v, + bytes32 r, + bytes32 s, + address alice, + address bob, + uint256 myParam, + uint256 deadline) { + + env e1; + env e2; + ecrecoverAxioms(); + //save the current state + storage init = lastStorage; + //execute and assume succeeded + address temp = ecrecover(getHash(bob, myParam, deadline), v, r, s); + executeMyFunctionFromSignature(e1, v, r, s, alice, myParam, deadline); + // compare another execution on the same state, look at reverting paths + executeMyFunctionFromSignature@withrevert(e2, v, r, s, bob, myParam, deadline) at init; + bool success = !lastReverted; + //if it succeeded it must be the same owner, or an unrealistic hash collision + assert success => ( alice==bob ) ; +} + + +/*** + # High level property : Owner must be the signer of the hash + A rule which proves that for a given set of parameters only a single owner can execute . + This property is implemented as a relational property - it compares two different executions on the same state. +*/ +rule ownerIsSigner(uint8 v, + bytes32 r, + bytes32 s, + address owner, + uint256 myParam, + uint256 deadline) { + + env e; + ecrecoverAxioms(); + //execute and assume succeeded + address signer = ecrecover(getHash(owner, myParam, deadline), v, r, s); + executeMyFunctionFromSignature(e, v, r, s, owner, myParam, deadline); + + assert owner == signer; +} + +/*** + # High level property : params and deadline are signed +make sure the param and deadline are part of the signature +*/ +rule signedParamAndDeadline(uint8 v, + bytes32 r, + bytes32 s, + address owner, + uint256 myParamA, + uint256 deadlineA, + uint256 myParamB, + uint256 deadlineB) { + + env e1; + env e2; + ecrecoverAxioms(); + //save the current state + storage init = lastStorage; + //execute and assume succeeded + executeMyFunctionFromSignature(e1, v, r, s, owner, myParamA, deadlineA); + // compare another execution on the same state, look at reverting paths + executeMyFunctionFromSignature@withrevert(e2, v, r, s, owner, myParamB, deadlineB) at init; + bool success = !lastReverted; + //if it succeeded it must be the same owner, or an unrealistic hash collision + assert success => ( myParamA==myParamB && deadlineA == deadlineB); +} + + +/*** + A signer can sign two different messages, in this case they have different signature +**/ +rule twoDifferent() { + ecrecoverAxioms(); + bytes32 msgHashA; uint8 vA; bytes32 rA; bytes32 sA; + bytes32 msgHashB; uint8 vB; bytes32 rB; bytes32 sB; + require msgHashA != msgHashB; + require ecrecover(msgHashA, vA, rA, sA) != 0 && ecrecover(msgHashB, vB, rB, sB) != 0; + satisfy ecrecover(msgHashA, vA, rA, sA) == ecrecover(msgHashB, vB, rB, sB); + assert ecrecover(msgHashA, vA, rA, sA) == ecrecover(msgHashB, vB, rB, sB) => + (rA != rB || sA != sB || vA != vB ); +} + +/** +Once a message is executed, it can not be executed again +**/ +rule signedMessagesExecutedOnce(uint8 v, + bytes32 r, + bytes32 s, + address signer, + uint256 myParam, + uint256 deadline) { + + env e1; + env e2; + ecrecoverAxioms(); + //execute and assume succeeded + executeMyFunctionFromSignature(e1, v, r, s, signer, myParam, deadline); + //attemp to execute again, on a possible different env + executeMyFunctionFromSignature@withrevert(e2, v, r, s, signer, myParam, deadline); + bool reverted = lastReverted; + assert reverted ; +} + +rule checkHash( + address bob, + uint256 myParam, + uint256 deadline) { + + env e1; + ecrecoverAxioms(); + //execute and assume succeeded + assert getHash(bob, myParam, deadline) == getHash(bob, myParam, deadline); +} + +rule CheckRevertCondition(uint8 v, + bytes32 r, + bytes32 s, + address owner, + uint256 myParam, + uint256 deadline) { + + env e; + ecrecoverAxioms(); + + //execute and assume succeeded + address signer = ecrecover(getHash(owner, myParam, deadline), v, r, s); + + bool msgValue = e.msg.value != 0; + bool signerIsZero = signer == 0; + bool signerDiffFromOwner = signer != owner; + bool noncesOverflow = currentContract.nonces[owner] + 1 > max_uint256; + bool blockTimestampPassDeadline = e.block.timestamp >= deadline; + + bool shouldRevert = noncesOverflow || msgValue || signerIsZero || signerDiffFromOwner || signerDiffFromOwner || blockTimestampPassDeadline ; + executeMyFunctionFromSignature@withrevert(e, v, r, s, owner, myParam, deadline); + assert shouldRevert <=> lastReverted; +} diff --git a/CVLByExample/Ecrecover/mutation.mconf b/CVLByExample/Ecrecover/mutation.mconf new file mode 100644 index 00000000..b4a0c5b0 --- /dev/null +++ b/CVLByExample/Ecrecover/mutation.mconf @@ -0,0 +1,9 @@ +{ + "gambit": { + "filename" : "Verify.sol", + "num_mutants": 5 + }, + "manual_mutants": { + "Verify.sol": "ManualMutation" + } +} \ No newline at end of file diff --git a/CVLByExample/README.md b/CVLByExample/README.md index edbcf4e1..b549646b 100644 --- a/CVLByExample/README.md +++ b/CVLByExample/README.md @@ -37,6 +37,8 @@ | **using** | [`using`](https://github.com/Certora/Examples/blob/master/DEFI/LiquidityPool/certora/specs/pool_link.spec#L14) | | **withrevert** | [`withrevert`](https://github.com/Certora/Examples/blob/master/CVLByExample/Storage/certora/specs/storage.spec#L44) | | **CVL Type** | [mathint](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L23), [method](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L83), [env](https://github.com/Certora/Examples/blob/master/DEFI/ERC20/certora/specs/ERC20Fixed.spec#L20) | +| **ercecover** | [example](https://github.com/Certora/Examples/blob/niv/Add-ecrecover-example/CVLByExample/Ecrecover/ecrecover.spec#L67) | + These examples can serve as an introduction to CVL ( Certora Verification Language ).