Liav/cert 7804 trusted methods

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"],
+}

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;
+    }
+}

CVLByExample/TrustedMethodsAnalysis/ExampleTrustedMethods.json

@@ -0,0 +1,3 @@
+{
+    "0xe0f5206bbd039e7b0592d8918820024e2a7437b9": ["0x7e2a6db8"]
+}

CVLByExample/TrustedMethodsAnalysis/README.md

@@ -0,0 +1,24 @@
+# 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 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 "_".
+
+Run this example using:
+```certoraRun Example.conf```
+[A report of this run](https://prover.certora.com/output/15800/4b6ef8f696284c839d772d6826b1b126?anonymousKey=7ebf992183ae4227631ec8e3df862a5d444dc552)

CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec

@@ -0,0 +1 @@
+use builtin rule trustedMethods;