From 8eee16df398a6cf79b9aac7c8801923542d0c808 Mon Sep 17 00:00:00 2001
From: liav-certora <114004726+liav-certora@users.noreply.github.com>
Date: Mon, 6 Jan 2025 14:33:32 +0200
Subject: [PATCH] Liav/cert 7804 trusted methods (#149)

* .

* .

* Update CVLByExample/TrustedMethodsAnalysis/README.md

Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com>

* Update README.md

---------

Co-authored-by: yoav-el-certora <122207807+yoav-el-certora@users.noreply.github.com>
---
 .../TrustedMethodsAnalysis/Example.conf       |  9 +++++
 .../TrustedMethodsAnalysis/Example.sol        | 38 +++++++++++++++++++
 .../ExampleTrustedMethods.json                |  3 ++
 CVLByExample/TrustedMethodsAnalysis/README.md | 24 ++++++++++++
 .../TrustedMethodsAnalysis/trustedMethod.spec |  1 +
 5 files changed, 75 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
 create mode 100644 CVLByExample/TrustedMethodsAnalysis/trustedMethod.spec

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..853476a
--- /dev/null
+++ b/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)
\ 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