From 63b859a36eda6e4dca46b66b37ef04af89da54e3 Mon Sep 17 00:00:00 2001 From: liav-certora Date: Sun, 29 Dec 2024 13:34:34 +0200 Subject: [PATCH 1/4] . --- .../TrustedMethodsAnalysis/Example.conf | 9 +++++ .../TrustedMethodsAnalysis/Example.sol | 38 +++++++++++++++++++ .../ExampleTrustedMethods.json | 3 ++ CVLByExample/TrustedMethodsAnalysis/README.md | 20 ++++++++++ 4 files changed, 70 insertions(+) create mode 100644 CVLByExample/TrustedMethodsAnalysis/Example.conf create mode 100644 CVLByExample/TrustedMethodsAnalysis/Example.sol create mode 100644 CVLByExample/TrustedMethodsAnalysis/ExampleTrustedMethods.json create mode 100644 CVLByExample/TrustedMethodsAnalysis/README.md diff --git a/CVLByExample/TrustedMethodsAnalysis/Example.conf b/CVLByExample/TrustedMethodsAnalysis/Example.conf new file mode 100644 index 0000000..c6e8899 --- /dev/null +++ b/CVLByExample/TrustedMethodsAnalysis/Example.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "./Example.sol:Example" + ], + "process": "emv", + "solc": "solc8.25", + "verify": "Example:./trustedMethod.spec", + "prover_resource_files": ["trustedMethods:ExampleTrustedMethods.json"], +} \ No newline at end of file diff --git a/CVLByExample/TrustedMethodsAnalysis/Example.sol b/CVLByExample/TrustedMethodsAnalysis/Example.sol new file mode 100644 index 0000000..f3d5bb4 --- /dev/null +++ b/CVLByExample/TrustedMethodsAnalysis/Example.sol @@ -0,0 +1,38 @@ +contract Example{ + address public constant foo = 0xE0f5206BBD039e7b0592d8918820024e2a7437b9; + + //We trust the contract address and the sighash + function callTrusted() external returns (uint){ + Foo bar = Foo(foo); + return bar.trusted(); + } + + //We trust the contract address, but not the sighash of the call. + function callUntrusted() external returns (uint){ + Foo bar = Foo(foo); + return bar.untrusted(); + } + + //We neither trust the sighash, nor the contract address. + function callUntrusted(address userTrustedContractAddress) external returns (uint){ + Foo bar = Foo(userTrustedContractAddress); + return bar.untrusted(); + } + + //We trust the sighash, but the contract address is unknown. + function callUntrustedDespiteKnownSighash(address userTrustedContractAddress) external returns (uint){ + Foo bar = Foo(userTrustedContractAddress); + return bar.trusted(); + } +} + +contract Foo{ + //Sighash: 0xb23d4266 + function untrusted() external returns (uint){ + return 1; + } + //Sighash: 0x7e2a6db8 + function trusted() external returns (uint){ + return 2; + } +} diff --git a/CVLByExample/TrustedMethodsAnalysis/ExampleTrustedMethods.json b/CVLByExample/TrustedMethodsAnalysis/ExampleTrustedMethods.json new file mode 100644 index 0000000..bbbbed7 --- /dev/null +++ b/CVLByExample/TrustedMethodsAnalysis/ExampleTrustedMethods.json @@ -0,0 +1,3 @@ +{ + "0xe0f5206bbd039e7b0592d8918820024e2a7437b9": ["0x7e2a6db8"] +} \ No newline at end of file diff --git a/CVLByExample/TrustedMethodsAnalysis/README.md b/CVLByExample/TrustedMethodsAnalysis/README.md new file mode 100644 index 0000000..c28bedb --- /dev/null +++ b/CVLByExample/TrustedMethodsAnalysis/README.md @@ -0,0 +1,20 @@ +# Trusted Method Analysis + +This feature checks for external calls and checks the calls against an allow lists by specifying a new built in parametric rule: `use builtin rule trustedMethods`. + +The rule succeeds if all external calls are fully resolved (i.e. sighash and target) and are on the defined trusted methods list. Otherwise the analysis reports violated for this method. This entails that the rule fails as soon as there is any call that is unresolved due to a missing target or a missing unresolved sighash, for instance as the deployed contract requires linking. + +The allow list must be set via `"prover_resource_files": ["trustedMethods:ExampleTrustedMethods.json"]` in the config file. + +**How to specify custom trusted methods** + +You can use a different set of trusted methods by specifying your own `trustedMethod.json` file in the following format: +``` +{ + "0xe0f5206bbd039e7b0592d8918820024e2a7437b9": ["0x4c6c6213","0x8f6462c3",...], + "0xe918820024e2a7437b90f5206bbd039e7b0592d8": ["0x62134c6c","0x2c38f646",...] +} +``` +And the adding `"prover_resource_files": ["trustedMethods:trustedMethod.json"]` to the config file. + +It's also possible to define a wildcard for the contract address or for the method sighash by using "_". \ No newline at end of file From 8ddace150fba2d95ee325cb2288ab62c4968827d Mon Sep 17 00:00:00 2001 From: liav-certora Date: Sun, 29 Dec 2024 13:40:39 +0200 Subject: [PATCH 2/4] . --- CVLByExample/TrustedMethodsAnalysis/README.md | 6 +++++- CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec | 1 + 2 files changed, 6 insertions(+), 1 deletion(-) create mode 100644 CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec diff --git a/CVLByExample/TrustedMethodsAnalysis/README.md b/CVLByExample/TrustedMethodsAnalysis/README.md index c28bedb..b125fa4 100644 --- a/CVLByExample/TrustedMethodsAnalysis/README.md +++ b/CVLByExample/TrustedMethodsAnalysis/README.md @@ -17,4 +17,8 @@ You can use a different set of trusted methods by specifying your own `trustedMe ``` And the adding `"prover_resource_files": ["trustedMethods:trustedMethod.json"]` to the config file. -It's also possible to define a wildcard for the contract address or for the method sighash by using "_". \ No newline at end of file +It's also possible to define a wildcard for the contract address or for the method sighash by using "_". + +Run this example using: +```certoraRun Example.conf``` +[A report of this run](https://vaas-stg.certora.com/output/15800/7329f2dcf86c49f6b96891439eeaa467?anonymousKey=cde57e9e5f2ab7c5300399cdaa97585add830664) \ No newline at end of file diff --git a/CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec b/CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec new file mode 100644 index 0000000..4f0b6d5 --- /dev/null +++ b/CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec @@ -0,0 +1 @@ +use builtin rule trustedMethods; \ No newline at end of file From 8a4d325521c62f3669927a5be9ee6e2aa3c0139f Mon Sep 17 00:00:00 2001 From: liav-certora <114004726+liav-certora@users.noreply.github.com> Date: Mon, 30 Dec 2024 12:05:45 +0200 Subject: [PATCH 3/4] Update CVLByExample/TrustedMethodsAnalysis/README.md Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com> --- CVLByExample/TrustedMethodsAnalysis/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CVLByExample/TrustedMethodsAnalysis/README.md b/CVLByExample/TrustedMethodsAnalysis/README.md index b125fa4..708d2e3 100644 --- a/CVLByExample/TrustedMethodsAnalysis/README.md +++ b/CVLByExample/TrustedMethodsAnalysis/README.md @@ -15,7 +15,7 @@ You can use a different set of trusted methods by specifying your own `trustedMe "0xe918820024e2a7437b90f5206bbd039e7b0592d8": ["0x62134c6c","0x2c38f646",...] } ``` -And the adding `"prover_resource_files": ["trustedMethods:trustedMethod.json"]` to the config file. +And adding `"prover_resource_files": ["trustedMethods:trustedMethod.json"]` to the config file. It's also possible to define a wildcard for the contract address or for the method sighash by using "_". From 93719d8326f090c6cd1bf8a691ab2d2c0acaf48d Mon Sep 17 00:00:00 2001 From: liav-certora Date: Sun, 5 Jan 2025 13:00:13 +0200 Subject: [PATCH 4/4] Update README.md --- CVLByExample/TrustedMethodsAnalysis/README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CVLByExample/TrustedMethodsAnalysis/README.md b/CVLByExample/TrustedMethodsAnalysis/README.md index 708d2e3..853476a 100644 --- a/CVLByExample/TrustedMethodsAnalysis/README.md +++ b/CVLByExample/TrustedMethodsAnalysis/README.md @@ -21,4 +21,4 @@ It's also possible to define a wildcard for the contract address or for the meth Run this example using: ```certoraRun Example.conf``` -[A report of this run](https://vaas-stg.certora.com/output/15800/7329f2dcf86c49f6b96891439eeaa467?anonymousKey=cde57e9e5f2ab7c5300399cdaa97585add830664) \ No newline at end of file +[A report of this run](https://prover.certora.com/output/15800/4b6ef8f696284c839d772d6826b1b126?anonymousKey=7ebf992183ae4227631ec8e3df862a5d444dc552) \ No newline at end of file