From cb0e51c331e4e10928319163b49fe1558731ef0c Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sun, 11 Feb 2024 01:33:56 +0200 Subject: [PATCH 1/8] to be tested - to-storage copies --- docs/user-guide/gaps.md | 82 ++++++++++++++++++++++++++++++++++++++++- 1 file changed, 81 insertions(+), 1 deletion(-) diff --git a/docs/user-guide/gaps.md b/docs/user-guide/gaps.md index 830b8deb..bc18e51d 100644 --- a/docs/user-guide/gaps.md +++ b/docs/user-guide/gaps.md @@ -180,4 +180,84 @@ is sufficient both by running the basic sanity rule, and if loops appear only under certain conditions, to write specialized sanity rules that force the Prover to reason about these particular code paths. -Mutation testing can also be useful here. \ No newline at end of file +Mutation testing can also be useful here. + +### 'Hidden' compiler-generated loops + +#### Copying Solidity memory arrays to storage + +When the Solidity compiler generates code for copying +a non-primitive object (could be a `bytes` buffer or a `struct` with a `bytes` field), +it generates two loops. +The first loop resets any previous remaining data written into the target storage slot. +The second loop copies the new object into the relevant storage slot. + +Consider the following contract: +```solidity +contract test { + struct ScheduledExecution { + address where; + bool execute; + bytes data; + } + + ScheduledExecution[] myArray; + + function testPush(address where, bool executed) public { + bytes memory data = abi.encodeWithSelector( + this.testPush.selector, + "aa" + ); + myArray.push(ScheduledExecution(where, executed, data)); + } +} +``` + +The push to `myArray` generates the two aforementioned loops. +If we wish to analyze this code with the Prover, there are two questions to be answered: + +1. Do we need to set a value for `--loop_iter` which is bigger than 1? + +Yes - the `data` local variable is put into a `struct ScheduledExecution` that is +put into an array in storage. +This is done by the compiler using a 'copy-loop'. +The selector component `this.testPush.selector` requires one iteration. +the string `aa` requires three iterations: according to the [ABI specification](https://docs.soliditylang.org/en/v0.8.24/abi-spec.html), +it consists of an offset to a dynamic buffer, the size of the buffer, +and then the (short) data element fitting in one word (32 bytes). +Therefore, `--loop_iter` should be set to XXX(SG). + + +2. Do we need to set `--optimistic_loop`? + +Yes - when we copy `data` from memory to storage, the Solidity compiler +also generates code that nullifies the previous data. +As we don't know (and probably don't wish to constrain) the size of the previous data, +we have to enable `--optimistic_loop`. + +Consider for example: +```solidity +function testPush(address where, bool executed) public { + bytes memory data = abi.encodeWithSelector( + this.testPush.selector, + "aa",”bb” + ); + myArray[0] = ScheduledExecution(where, executed, data); + bytes memory data2 = abi.encodeWithSelector( + this.testPush.selector, + "aa" + ); + myArray[0] = data2; +} +``` + +When we update `myArray[0]` with `data2`, the Solidity compiler will put zeroes +in the space that was occupied by `data` beyond the length of `data2`. + + +To test our configuration, we use the following specification: +```cvl +use builtin rule sanity; +``` + +and make sure the rule passes for the `testPush` method. \ No newline at end of file From d6949049e894a31ca50dcb2f4a96a1429755cf92 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sun, 11 Feb 2024 01:36:50 +0200 Subject: [PATCH 2/8] update --- docs/user-guide/gaps.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/user-guide/gaps.md b/docs/user-guide/gaps.md index bc18e51d..330aa21f 100644 --- a/docs/user-guide/gaps.md +++ b/docs/user-guide/gaps.md @@ -253,7 +253,8 @@ function testPush(address where, bool executed) public { When we update `myArray[0]` with `data2`, the Solidity compiler will put zeroes in the space that was occupied by `data` beyond the length of `data2`. - +As the difference between `data.length` and `data2.length` +could theoretically be unbounded (e.g. if instead of `"bb"` we had an arbitrary `bytes` buffer). To test our configuration, we use the following specification: ```cvl From d0e97f9e765ed881eef9fe74c18d8b72fe11efff Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 16 Feb 2024 12:29:10 +0200 Subject: [PATCH 3/8] further elaboration on the loop subject --- docs/user-guide/gaps.md | 90 ++++++++++++++++++++++++++++++----------- 1 file changed, 66 insertions(+), 24 deletions(-) diff --git a/docs/user-guide/gaps.md b/docs/user-guide/gaps.md index 330aa21f..2c2bd551 100644 --- a/docs/user-guide/gaps.md +++ b/docs/user-guide/gaps.md @@ -194,7 +194,8 @@ The second loop copies the new object into the relevant storage slot. Consider the following contract: ```solidity -contract test { +// MemoryToStorage.sol +contract MemoryToStorage { struct ScheduledExecution { address where; bool execute; @@ -225,40 +226,81 @@ The selector component `this.testPush.selector` requires one iteration. the string `aa` requires three iterations: according to the [ABI specification](https://docs.soliditylang.org/en/v0.8.24/abi-spec.html), it consists of an offset to a dynamic buffer, the size of the buffer, and then the (short) data element fitting in one word (32 bytes). -Therefore, `--loop_iter` should be set to XXX(SG). +Therefore, `--loop_iter` should be set to 3. +To test our configuration, we use the following specification: +```cvl +// sanity.spec +use builtin rule sanity; +``` + +Therefore: +```bash +certoraRun MemoryToStorage.sol --verify MemoryToStorage:sanity.spec --loop_iter 3 // Passes +certoraRun MemoryToStorage.sol --verify MemoryToStorage:sanity.spec --loop_iter 2 // Violates sanity +``` 2. Do we need to set `--optimistic_loop`? Yes - when we copy `data` from memory to storage, the Solidity compiler also generates code that nullifies the previous data. -As we don't know (and probably don't wish to constrain) the size of the previous data, +As we do not know (and probably not wishing to constrain) the size of the previous data, we have to enable `--optimistic_loop`. -Consider for example: -```solidity -function testPush(address where, bool executed) public { - bytes memory data = abi.encodeWithSelector( - this.testPush.selector, - "aa",”bb” - ); - myArray[0] = ScheduledExecution(where, executed, data); - bytes memory data2 = abi.encodeWithSelector( - this.testPush.selector, - "aa" - ); - myArray[0] = data2; +While the sanity rule does not check for auto-generated assertions, +any run with assertions would generate an additional sub-rule for auto-generated assertions +that will fail without `--optimistic_loop`. + +Given the following specification: +```cvl +// simpleAssert.spec +rule simpleAssert { + env e; + calldataarg arg; + method f; + f(e,arg); + assert true; } ``` -When we update `myArray[0]` with `data2`, the Solidity compiler will put zeroes -in the space that was occupied by `data` beyond the length of `data2`. -As the difference between `data.length` and `data2.length` -could theoretically be unbounded (e.g. if instead of `"bb"` we had an arbitrary `bytes` buffer). +We have that: +```bash +certoraRun MemoryToStorage.sol --verify MemoryToStorage:simpleAssert.spec --loop_iter 3 --optimistic_loop // Passes +certoraRun MemoryToStorage.sol --verify MemoryToStorage:simpleAssert.spec --loop_iter 3 // Violated with "Unwinding condition in a loop" +``` -To test our configuration, we use the following specification: -```cvl -use builtin rule sanity; +Note that running with `--optimistic_loop` on the above example imposes an assumption +on the size of the previous buffer written in `myArray[0].data`. +One could have more complex flows where `--loop_iter 3` is not sufficient to properly +unroll the erasure loop. + +Consider for example this revised contract: +```solidity +// MemoryToStorage2.sol +contract MemoryToStorage { + ... + + function testPush(address where, bool executed) public { + require (myArray[0].data.length == 225); + bytes memory data = abi.encodeWithSelector( + this.testPush.selector, + "aa" + ); + myArray[0] = ScheduledExecution(where, executed, data); + } +} ``` -and make sure the rule passes for the `testPush` method. \ No newline at end of file +The only difference in this new functionality is that we assume that the previous data has size of 225 bytes. +When we update `myArray[0]` with `data`, the Solidity compiler will put zeroes +in the space that was occupied by `myArray[0].data` beyond the length of `data`. +If the previous buffer size was 224 for example, then since the size of the new `data` is 128, +it means we need to clean `224 - 128 = 96` bytes, or 3 words. +This is of course feasible with `--loop_iter 3`. +However, here we require the previous buffer size to be 225, which means we need to clean 4 extra words, +thus requiring a minimal `--loop_iter` value of 4. + +```bash +certoraRun MemoryToStorage2.sol:MemoryToStorage --verify MemoryToStorage:sanity.spec --loop_iter 3 // Violates sanity +certoraRun MemoryToStorage2.sol:MemoryToStorage --verify MemoryToStorage:sanity.spec --loop_iter 4 // Passes +``` \ No newline at end of file From 59797d0395d3d604c03ed44827301eac8b8d97d4 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 16 Feb 2024 12:30:19 +0200 Subject: [PATCH 4/8] subtitle added --- docs/user-guide/gaps.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/docs/user-guide/gaps.md b/docs/user-guide/gaps.md index 2c2bd551..f501ad78 100644 --- a/docs/user-guide/gaps.md +++ b/docs/user-guide/gaps.md @@ -269,6 +269,8 @@ certoraRun MemoryToStorage.sol --verify MemoryToStorage:simpleAssert.spec --loop certoraRun MemoryToStorage.sol --verify MemoryToStorage:simpleAssert.spec --loop_iter 3 // Violated with "Unwinding condition in a loop" ``` +##### Is `--loop_iter 3` always sufficient? + Note that running with `--optimistic_loop` on the above example imposes an assumption on the size of the previous buffer written in `myArray[0].data`. One could have more complex flows where `--loop_iter 3` is not sufficient to properly From 7cf39aac8f141f05f73a0dbd98b254928ae187c4 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 16 Feb 2024 12:31:46 +0200 Subject: [PATCH 5/8] formatting --- docs/user-guide/gaps.md | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/docs/user-guide/gaps.md b/docs/user-guide/gaps.md index f501ad78..1c581bd2 100644 --- a/docs/user-guide/gaps.md +++ b/docs/user-guide/gaps.md @@ -236,8 +236,11 @@ use builtin rule sanity; Therefore: ```bash -certoraRun MemoryToStorage.sol --verify MemoryToStorage:sanity.spec --loop_iter 3 // Passes -certoraRun MemoryToStorage.sol --verify MemoryToStorage:sanity.spec --loop_iter 2 // Violates sanity +// Passes: +certoraRun MemoryToStorage.sol --verify MemoryToStorage:sanity.spec --loop_iter 3 + +// Violates sanity: +certoraRun MemoryToStorage.sol --verify MemoryToStorage:sanity.spec --loop_iter 2 ``` 2. Do we need to set `--optimistic_loop`? @@ -265,8 +268,11 @@ rule simpleAssert { We have that: ```bash -certoraRun MemoryToStorage.sol --verify MemoryToStorage:simpleAssert.spec --loop_iter 3 --optimistic_loop // Passes -certoraRun MemoryToStorage.sol --verify MemoryToStorage:simpleAssert.spec --loop_iter 3 // Violated with "Unwinding condition in a loop" +// Passes: +certoraRun MemoryToStorage.sol --verify MemoryToStorage:simpleAssert.spec --loop_iter 3 --optimistic_loop + +// Violated with "Unwinding condition in a loop": +certoraRun MemoryToStorage.sol --verify MemoryToStorage:simpleAssert.spec --loop_iter 3 ``` ##### Is `--loop_iter 3` always sufficient? @@ -303,6 +309,9 @@ However, here we require the previous buffer size to be 225, which means we need thus requiring a minimal `--loop_iter` value of 4. ```bash -certoraRun MemoryToStorage2.sol:MemoryToStorage --verify MemoryToStorage:sanity.spec --loop_iter 3 // Violates sanity -certoraRun MemoryToStorage2.sol:MemoryToStorage --verify MemoryToStorage:sanity.spec --loop_iter 4 // Passes +// Violates sanity: +certoraRun MemoryToStorage2.sol:MemoryToStorage --verify MemoryToStorage:sanity.spec --loop_iter 3 + + // Passes: +certoraRun MemoryToStorage2.sol:MemoryToStorage --verify MemoryToStorage:sanity.spec --loop_iter 4 ``` \ No newline at end of file From 27677e95c1b1201b2131ab9a143e779170d18741 Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 16 Feb 2024 12:35:20 +0200 Subject: [PATCH 6/8] formatting --- docs/user-guide/gaps.md | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/docs/user-guide/gaps.md b/docs/user-guide/gaps.md index 1c581bd2..d45f4f52 100644 --- a/docs/user-guide/gaps.md +++ b/docs/user-guide/gaps.md @@ -197,19 +197,19 @@ Consider the following contract: // MemoryToStorage.sol contract MemoryToStorage { struct ScheduledExecution { - address where; - bool execute; - bytes data; + address where; + bool execute; + bytes data; } ScheduledExecution[] myArray; function testPush(address where, bool executed) public { - bytes memory data = abi.encodeWithSelector( - this.testPush.selector, - "aa" - ); - myArray.push(ScheduledExecution(where, executed, data)); + bytes memory data = abi.encodeWithSelector( + this.testPush.selector, + "aa" + ); + myArray.push(ScheduledExecution(where, executed, data)); } } ``` @@ -258,11 +258,11 @@ Given the following specification: ```cvl // simpleAssert.spec rule simpleAssert { - env e; - calldataarg arg; - method f; - f(e,arg); - assert true; + env e; + calldataarg arg; + method f; + f(e,arg); + assert true; } ``` From 54f4727d68429ca0fb9f5b9b9260dc70324bdecc Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Fri, 16 Feb 2024 15:23:23 +0200 Subject: [PATCH 7/8] WIP - revert causes parsing --- docs/user-guide/gaps.md | 105 +++++++++++++++++++++++++++++++++++++++- 1 file changed, 104 insertions(+), 1 deletion(-) diff --git a/docs/user-guide/gaps.md b/docs/user-guide/gaps.md index d45f4f52..17428629 100644 --- a/docs/user-guide/gaps.md +++ b/docs/user-guide/gaps.md @@ -314,4 +314,107 @@ certoraRun MemoryToStorage2.sol:MemoryToStorage --verify MemoryToStorage:sanity. // Passes: certoraRun MemoryToStorage2.sol:MemoryToStorage --verify MemoryToStorage:sanity.spec --loop_iter 4 -``` \ No newline at end of file +``` + + +## Reverts + +The Solidity compiler is generating checks for revert conditions that are not always spelled-out by the user +using `require` and `assert` statements. +Usually, these involve assumptions on the structure of the provided user data. + +This section will present a few examples where Prover-presented revert causes +are stemming from compiler-generated checks, so that users can be more informed +about debugging such revert causes. + +### Payability + +Payability is the simplest kind of compiler-generated checks, as they are controlled by the user. + +Consider the example contract: +```solidity +contract Payability { + function foo() external {} +} +``` + +Specification: +```cvl +rule revertCheck { + env e; + foo@withrevert(e); + assert !lastReverted; +} +``` + +We are expected to get the following revert cause: +``` +!(safe_math_narrow:bif(e.msg.value)==0x0) +``` + +Which is telling us, that `e.msg.value` being non-zero is the cause for the revert. +(`safe_math_narrow` is a Prover-internal cast operation.) +This can be easily fixed with the revised rule: +```cvl +rule revertCheck { + env e; + require e.msg.value == 0; + foo@withrevert(e); + assert !lastReverted; +} +``` + +### Basic type assumptions when passing arguments from CVL + +When we pass arguments from CVL to Solidity, +CVL attempts to add the same assumptions that Solidity code has on the +sizes of the arguments provided to it. +This holds for types such as `bytes` and `string`, +but not for generalized `calldata` buffers (passed with `calldataarg` variable type in CVL). + +Therefore, given the following trivial Solidity code: +```solidity +contract StringInput { + function foo(string memory s) external {} +} +``` + +the following rule would be proven: +```cvl +rule revertCheckString { + env e; + string s; + require e.msg.value == 0; + foo@withrevert(e, s); + assert !lastReverted; +} +``` + +While using `calldataarg` instead would lead to a violation: +```cvl +rule revertCheckCalldataarg { + env e; + calldataarg arg; + require e.msg.value == 0; + foo@withrevert(e, arg); + assert !lastReverted; +} +``` + +The run could trigger a few different kinds of reverts. +Even the simplest revert cause is a bit tricky to parse: +`CANON12[0x4]>MASK64` + +It says that the value of `CANON12` (an internal name representing the `calldata` input to `foo`) +at offset `0x4`, which is in fact holding the pointer to the string in calldata, is bigger than `2^64-1` +(shortened as `MASK64`, a mask where the 64 less-significant-bits are set to 1). +It is a usual sanity check instrumented by Solidity to avoid huge calldata buffers +that consume a high amount of gas to process. + +;### Strings-in-storage invariant +; +;TODO +; +;### Assumptions on array elements +; +;TODO \ No newline at end of file From 21aa673beb6d620ca63787640e4824d2d7fbcf5b Mon Sep 17 00:00:00 2001 From: Shelly Grossman Date: Sat, 17 Feb 2024 14:16:00 +0200 Subject: [PATCH 8/8] Expanding on a more complicated revert cause --- docs/user-guide/gaps.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/docs/user-guide/gaps.md b/docs/user-guide/gaps.md index 17428629..26613e69 100644 --- a/docs/user-guide/gaps.md +++ b/docs/user-guide/gaps.md @@ -411,6 +411,20 @@ at offset `0x4`, which is in fact holding the pointer to the string in calldata, It is a usual sanity check instrumented by Solidity to avoid huge calldata buffers that consume a high amount of gas to process. +A trickier sanity check instrumented by the Solidity compiler that could be highlighted by +the Prover is the following: +`(0x20+0x4+arg34_data[0x4]+arg34_data[0x4+arg34_data[0x4]])>arg34_length` + +It says that a certain complex expression is greater than `arg34_length`. +`arg34` is the internal Prover-generated name of the `calldataarg arg` variable, and +`arg34_length` is the variable holding its size (as would be returned by `CALLDATASIZE` instruction), +and `arg34_data` is the raw `calldata` buffer itself. +So we can see it is a bound check that makes sure we are not accessing beyond `CALLDATASIZE`. +Specifically, `0x20 + 0x4 + arg34_data[0x4]` is a pointer to the beginning of the `string` +argument in calldata (first 4 bytes are the `sighash`, another word is for the pointer slot, +`arg34_data[0x4]` holds the relative offset to the string) +`arg34_data[0x4+arg34_data[0x4]]` holds the length of the string. + ;### Strings-in-storage invariant ; ;TODO