diff --git a/not-so-smart-contracts/cairo/L1_to_L2_address_conversion/README.md b/not-so-smart-contracts/cairo/L1_to_L2_address_conversion/README.md index 4af26af6..4b1bd108 100644 --- a/not-so-smart-contracts/cairo/L1_to_L2_address_conversion/README.md +++ b/not-so-smart-contracts/cairo/L1_to_L2_address_conversion/README.md @@ -8,19 +8,20 @@ Suppose that the following code to initiate L2 deposits from L1. The first examp ```solidity uint256 public constant STARKNET_FIELD_PRIME; // the prime order P of the elliptic curve used -IERC20 public constant token; //some token to deposit on L2 +IERC20 public constant token; // some token to deposit on L2 + event Deposited(uint256 sender, uint256 amount); -function badDepositToL2(uint256 to, uint256 amount) public returns (bool) { - token.transferFrom(to, address(this),amount); - emit Deposited(to,amount); // this message gets processed on L2 +function badDepositToL2(uint256 to, uint256 amount) public returns (bool) { + token.transferFrom(to, address(this), amount); + emit Deposited(to, amount); // this message gets processed on L2 return true; } -function betterDepositToL2(uint256 to, uint256 amount) public returns (bool) { - require(to !=0 && to < STARKNET_FIELD_PRIME, "invalid address"); //verifies 0 < to < P - token.transferFrom(to, address(this),amount); - emit Deposited(to,amount); // this message gets processed on L2 +function betterDepositToL2(uint256 to, uint256 amount) public returns (bool) { + require(to != 0 && to < STARKNET_FIELD_PRIME, "invalid address"); // verifies 0 < to < P + token.transferFrom(to, address(this), amount); + emit Deposited(to, amount); // this message gets processed on L2 return true; } ``` diff --git a/not-so-smart-contracts/cairo/consider_L1_to_L2_message_failure.md b/not-so-smart-contracts/cairo/consider_L1_to_L2_message_failure.md index 47c228da..112b079c 100644 --- a/not-so-smart-contracts/cairo/consider_L1_to_L2_message_failure.md +++ b/not-so-smart-contracts/cairo/consider_L1_to_L2_message_failure.md @@ -9,12 +9,12 @@ For instance, a message can fail to be processed if there is a sudden spike in t Suppose that the following code to initiate L2 deposits from L1, taking the tokens from the user: ```solidity -IERC20 public constant token; //some token to deposit on L2 +IERC20 public constant token; // some token to deposit on L2 -function depositToL2(uint256 to, uint256 amount) public returns (bool) { +function depositToL2(uint256 to, uint256 amount) public returns (bool) { require(token.transferFrom(to, address(this), amount)); - .. - StarknetCore.sendMessageToL2(..); + ... + StarknetCore.sendMessageToL2(...); return true; } ``` diff --git a/not-so-smart-contracts/cairo/namespace_storage_var_collision/README.md b/not-so-smart-contracts/cairo/namespace_storage_var_collision/README.md index 736d6ee7..03124946 100644 --- a/not-so-smart-contracts/cairo/namespace_storage_var_collision/README.md +++ b/not-so-smart-contracts/cairo/namespace_storage_var_collision/README.md @@ -17,7 +17,7 @@ from openzeppelin.a import A from openzeppelin.b import B @external -func increase_balance_a{ +func increase_balance_a { syscall_ptr : felt*, pedersen_ptr : HashBuiltin*, range_check_ptr}(amount : felt): A.increase_balance(amount) @@ -25,7 +25,7 @@ func increase_balance_a{ end @external -func increase_balance_b{ +func increase_balance_b { syscall_ptr : felt*, pedersen_ptr : HashBuiltin*, range_check_ptr}(amount : felt): B.increase_balance(amount) @@ -33,7 +33,7 @@ func increase_balance_b{ end @view -func get_balance_a{ +func get_balance_a { syscall_ptr : felt*, pedersen_ptr : HashBuiltin*, range_check_ptr}() -> (res : felt): let (res) = A.get_balance() @@ -41,7 +41,7 @@ func get_balance_a{ end @view -func get_balance_b{ +func get_balance_b { syscall_ptr : felt*, pedersen_ptr : HashBuiltin*, range_check_ptr}() -> (res : felt): let (res) = B.get_balance() diff --git a/program-analysis/echidna/advanced/collecting-a-corpus.md b/program-analysis/echidna/advanced/collecting-a-corpus.md index 0d5eb19c..d59eb508 100644 --- a/program-analysis/echidna/advanced/collecting-a-corpus.md +++ b/program-analysis/echidna/advanced/collecting-a-corpus.md @@ -13,19 +13,19 @@ We will see how to collect and use a corpus of transactions with Echidna. The ta ```Solidity contract C { - bool value_found = false; - function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public { - require(magic_1 == 42); - require(magic_2 == 129); - require(magic_3 == magic_4+333); - value_found = true; - return; - } - - function echidna_magic_values() public returns (bool) { - return !value_found; - } - + bool value_found = false; + + function magic(uint256 magic_1, uint256 magic_2, uint256 magic_3, uint256 magic_4) public { + require(magic_1 == 42); + require(magic_2 == 129); + require(magic_3 == magic_4 + 333); + value_found = true; + return; + } + + function echidna_magic_values() public returns (bool) { + return !value_found; + } } ``` @@ -69,7 +69,7 @@ Echidna still cannot find the correct magic value. We can verify where it gets s ``` r |contract C { bool value_found = false; -r | function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public { +r | function magic(uint256 magic_1, uint256 magic_2, uint256 magic_3, uint256 magic_4) public { r | require(magic_1 == 42); r | require(magic_2 == 129); r | require(magic_3 == magic_4+333); @@ -164,7 +164,7 @@ This time, the property is violated immediately. We can verify that another `cov ``` *r |contract C { bool value_found = false; -*r | function magic(uint magic_1, uint magic_2, uint magic_3, uint magic_4) public { +*r | function magic(uint256 magic_1, uint256 magic_2, uint256 magic_3, uint256 magic_4) public { *r | require(magic_1 == 42); *r | require(magic_2 == 129); *r | require(magic_3 == magic_4+333); diff --git a/program-analysis/echidna/advanced/end-to-end-testing.md b/program-analysis/echidna/advanced/end-to-end-testing.md index 7149240a..2d1787c2 100644 --- a/program-analysis/echidna/advanced/end-to-end-testing.md +++ b/program-analysis/echidna/advanced/end-to-end-testing.md @@ -135,7 +135,7 @@ import "../SimpleStorage.sol"; contract E2E { SimpleStorage st = SimpleStorage(0x871DD7C2B4b25E1Aa18728e9D5f2Af4C4e431f5c); - function crytic_const_storage() public returns(bool) { + function crytic_const_storage() public returns (bool) { return st.storedData() == 89; } } diff --git a/program-analysis/echidna/advanced/finding-transactions-with-high-gas-consumption.md b/program-analysis/echidna/advanced/finding-transactions-with-high-gas-consumption.md index c5b773c0..a1745498 100644 --- a/program-analysis/echidna/advanced/finding-transactions-with-high-gas-consumption.md +++ b/program-analysis/echidna/advanced/finding-transactions-with-high-gas-consumption.md @@ -15,24 +15,25 @@ We will see how to find the transactions with high gas consumption with Echidna. ```solidity contract C { - uint state; - - function expensive(uint8 times) internal { - for(uint8 i=0; i < times; i++) - state = state + i; - } - - function f(uint x, uint y, uint8 times) public { - if (x == 42 && y == 123) - expensive(times); - else - state = 0; - } - - function echidna_test() public returns (bool) { - return true; - } - + uint256 state; + + function expensive(uint8 times) internal { + for (uint8 i = 0; i < times; i++) { + state = state + i; + } + } + + function f(uint256 x, uint256 y, uint8 times) public { + if (x == 42 && y == 123) { + expensive(times); + } else { + state = 0; + } + } + + function echidna_test() public returns (bool) { + return true; + } } ``` @@ -101,10 +102,10 @@ contract C { function pop() public { addrs.pop(); } - function clear() public{ + function clear() public { addrs.length = 0; } - function check() public{ + function check() public { for(uint256 i = 0; i < addrs.length; i++) for(uint256 j = i+1; j < addrs.length; j++) if (addrs[i] == addrs[j]) diff --git a/program-analysis/echidna/advanced/hevm-cheats-to-test-permit.md b/program-analysis/echidna/advanced/hevm-cheats-to-test-permit.md index 18043590..86804bb1 100644 --- a/program-analysis/echidna/advanced/hevm-cheats-to-test-permit.md +++ b/program-analysis/echidna/advanced/hevm-cheats-to-test-permit.md @@ -2,7 +2,7 @@ ## Introduction -[EIP 2612](https://eips.ethereum.org/EIPS/eip-2612) introduces the function `permit(address owner, address spender, uint value, uint deadline, uint8 v, bytes32 r, bytes32 s)` to the ERC20 abi. This function essentially takes in signature parameters generated through ECDSA combined with the [EIP 712](https://eips.ethereum.org/EIPS/eip-712) standard for typed data hashing, and recovers the author of the signature through `ecrecover()`. It then sets `allowances[owner][spender]` to `value`. +[EIP 2612](https://eips.ethereum.org/EIPS/eip-2612) introduces the function `permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s)` to the ERC20 abi. This function essentially takes in signature parameters generated through ECDSA combined with the [EIP 712](https://eips.ethereum.org/EIPS/eip-712) standard for typed data hashing, and recovers the author of the signature through `ecrecover()`. It then sets `allowances[owner][spender]` to `value`. ## Uses @@ -17,24 +17,22 @@ We use solmate’s implementation of the ERC20 standard that includes the permit In our `TestDepositWithPermit` contract, we need to have the signature signed by an owner for validation. To do this, we can use `hevm`’s `sign` cheatcode, which takes in a message and a private key and creates a valid signature. For this example, we use the private key `0x02` and the following signed message, which essentially represents the permit signature following EIP 712: ```solidity - keccak256( - abi.encodePacked( - "\x19\x01", - asset.DOMAIN_SEPARATOR(), - keccak256( - abi.encode( - keccak256( - "Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)" - ), - owner, - spender, - assetAmount, - asset.nonces(owner), - block.timestamp - ) - ) +keccak256( + abi.encodePacked( + "\x19\x01", + asset.DOMAIN_SEPARATOR(), + keccak256( + abi.encode( + keccak256("Permit(address owner,address spender,uint256 value,uint256 nonce,uint256 deadline)"), + owner, + spender, + assetAmount, + asset.nonces(owner), + block.timestamp ) - ); + ) + ) +); ``` The helper function `getSignature(address owner, address spender, uint256 assetAmount)` returns a valid signature generated via the `sign` cheatcode. Note that the sign cheatcode leaks the private key and thus it is best to use dummy keys when testing. Our keypair data was taken from [this site](https://privatekeys.pw/keys/ethereum/1). Now to test out the signature, we will mint a random amount to the `OWNER` address, the address corresponding to private key `0x02`, which was the signer of the permit signature. We then see if we can use that signature to transfer the owner’s tokens to ourselves. diff --git a/program-analysis/echidna/advanced/optimization_mode.md b/program-analysis/echidna/advanced/optimization_mode.md index c440999b..f02de3d6 100644 --- a/program-analysis/echidna/advanced/optimization_mode.md +++ b/program-analysis/echidna/advanced/optimization_mode.md @@ -15,10 +15,10 @@ Optimization mode is a experimental feature that allows to define a special func and returns a `int256`. Echidna will try find a sequence of transactions to maximize the value returned: ```solidity - function echidna_opt_function() public view returns (int256) { - // if it reverts, Echidna will assumed it returned type(int256).min - return ..; - } +function echidna_opt_function() public view returns (int256) { + // if it reverts, Echidna will assumed it returned type(int256).min + return ...; +} ``` ## Optimizing with Echidna @@ -29,23 +29,15 @@ In this example, the target is the following smart contract (_[../example/opt.so contract TestDutchAuctionOptimization { int256 maxPriceDifference; - function setMaxPriceDifference( - uint256 startPrice, - uint256 endPrice, - uint256 startTime, - uint256 endTime - ) public { - if (endTime < (startTime + 900)) { - revert(); - } - if (startPrice <= endPrice) { - revert(); - } - uint256 numerator = (startPrice - endPrice) * - (block.timestamp - startTime); + function setMaxPriceDifference(uint256 startPrice, uint256 endPrice, uint256 startTime, uint256 endTime) public { + if (endTime < (startTime + 900)) revert(); + if (startPrice <= endPrice) revert(); + + uint256 numerator = (startPrice - endPrice) * (block.timestamp - startTime); uint256 denominator = endTime - startTime; uint256 stepDecrease = numerator / denominator; uint256 currentAuctionPrice = startPrice - stepDecrease; + if (currentAuctionPrice < endPrice) { maxPriceDifference = int256(endPrice - currentAuctionPrice); } diff --git a/program-analysis/echidna/advanced/testing-bytecode.md b/program-analysis/echidna/advanced/testing-bytecode.md index 147e9e73..6950c26b 100644 --- a/program-analysis/echidna/advanced/testing-bytecode.md +++ b/program-analysis/echidna/advanced/testing-bytecode.md @@ -25,10 +25,10 @@ Consider the following bytecode: For which we only know the ABI: ```solidity -interface Target{ - function totalSupply() external returns(uint); - function balanceOf(address) external returns(uint); - function transfer(address, uint) external; +interface Target { + function totalSupply() external returns (uint256); + function balanceOf(address) external returns (uint256); + function transfer(address, uint256) external; } ``` @@ -40,34 +40,36 @@ Because we don't have the source code, we cannot directly add the property in th Instead we will use a proxy contract: ```solidity -interface Target{ - function totalSupply() external returns(uint); - function balanceOf(address) external returns(uint); - function transfer(address, uint) external; +interface Target { + function totalSupply() external returns (uint256); + function balanceOf(address) external returns (uint256); + function transfer(address, uint256) external; } -contract TestBytecodeOnly{ - Target t; +contract TestBytecodeOnly { + Target target; - constructor() public{ - address target_addr; + constructor() { + address targetAddress; // init bytecode - bytes memory target_bytecode = hex"608060405234801561001057600080fd5b506103e86000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506103e86001819055506101fa8061006e6000396000f3fe608060405234801561001057600080fd5b50600436106100415760003560e01c806318160ddd1461004657806370a0823114610064578063a9059cbb146100bc575b600080fd5b61004e61010a565b6040518082815260200191505060405180910390f35b6100a66004803603602081101561007a57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610110565b6040518082815260200191505060405180910390f35b610108600480360360408110156100d257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610128565b005b60015481565b60006020528060005260406000206000915090505481565b806000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540392505081905550806000808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540192505081905550505056fe"; + bytes memory targetCreationBytecode = + hex"608060405234801561001057600080fd5b506103e86000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506103e86001819055506101fa8061006e6000396000f3fe608060405234801561001057600080fd5b50600436106100415760003560e01c806318160ddd1461004657806370a0823114610064578063a9059cbb146100bc575b600080fd5b61004e61010a565b6040518082815260200191505060405180910390f35b6100a66004803603602081101561007a57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610110565b6040518082815260200191505060405180910390f35b610108600480360360408110156100d257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610128565b005b60015481565b60006020528060005260406000206000915090505481565b806000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540392505081905550806000808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008282540192505081905550505056fe"; - uint size = target_bytecode.length; + uint256 size = targetCreationBytecode.length; - assembly{ - target_addr := create(0, 0xa0, size) // 0xa0 was manually computed. It might require different value according to the compiler version + assembly { + targetAddress := create(0, add(targetCreationBytecode, 0x20), size) // Skip the 32 bytes encoded length. } - t = Target(target_addr); + + target = Target(targetAddress); } - function transfer(address to, uint amount) public { - t.transfer(to, amount); + function transfer(address to, uint256 amount) public { + target.transfer(to, amount); } - function echidna_test_balance() public returns(bool){ - return t.balanceOf(address(this)) <= t.totalSupply(); + function echidna_test_balance() public returns (bool) { + return target.balanceOf(address(this)) <= target.totalSupply(); } } ``` @@ -76,7 +78,7 @@ The proxy: - Deploys the bytecode in its constructor - Has one function that will call the target's `transfer` function -- Has one Echidna property `t.balanceOf(address(this)) <= t.totalSupply()` +- Has one Echidna property `target.balanceOf(address(this)) <= target.totalSupply()` ## Run Echidna @@ -94,16 +96,16 @@ Here Echidna found that by calling `transfer(0, 1002)` anyone can mint tokens. The actual source code of the target is: ```solidity -contract C{ - mapping(address => uint) public balanceOf; - uint public totalSupply; +contract C { + mapping(address => uint256) public balanceOf; + uint256 public totalSupply; - constructor() public{ + constructor() public { balanceOf[msg.sender] = 1000; totalSupply = 1000; } - function transfer(address to, uint amount) public{ + function transfer(address to, uint256 amount) public { balanceOf[msg.sender] -= amount; balanceOf[to] += amount; } @@ -124,8 +126,8 @@ def my_func(a: uint256, b: uint256, c: uint256) -> uint256: ``` ```solidity -contract SolidityVersion{ - function my_func(uint a, uint b, uint c) view public{ +contract SolidityVersion { + function my_func(uint256 a, uint256 b, uint256 c) view public { return a * b / c; } } @@ -134,32 +136,32 @@ contract SolidityVersion{ We can test that they return always the same values using the proxy pattern: ```solidity -interface Target{ - function my_func(uint, uint, uint) external returns(uint); +interface Target { + function my_func(uint256, uint256, uint256) external returns (uint256); } -contract SolidityVersion{ - Target t; +contract SolidityVersion { + Target target; - constructor() public{ + constructor() public { address target_addr; // vyper bytecode - bytes memory target_bytecode = hex"61007756341561000a57600080fd5b60043610156100185761006d565b600035601c52630ff198a3600051141561006c57600435602435808202821582848304141761004657600080fd5b80905090509050604435808061005b57600080fd5b82049050905060005260206000f350005b5b60006000fd5b61000461007703610004600039610004610077036000f3"; + bytes memory targetCreationBytecode = hex"61007756341561000a57600080fd5b60043610156100185761006d565b600035601c52630ff198a3600051141561006c57600435602435808202821582848304141761004657600080fd5b80905090509050604435808061005b57600080fd5b82049050905060005260206000f350005b5b60006000fd5b61000461007703610004600039610004610077036000f3"; - uint size = target_bytecode.length; + uint256 size = targetCreationBytecode.length; - assembly{ - target_addr := create(0, 0xa0, size) // 0xa0 was manually computed. It might require different value according to the compiler version + assembly { + target_addr := create(0, add(targetCreationBytecode, 0x20), size) // Skip the 32 bytes encoded length. } - t = Target(target_addr); + target = Target(target_addr); } - function test(uint a, uint b, uint c) public returns(bool){ - assert(my_func(a, b, c) == t.my_func(a, b, c)); + function test(uint256 a, uint256 b, uint256 c) public returns (bool) { + assert(my_func(a, b, c) == target.my_func(a, b, c)); } - function my_func(uint a, uint b, uint c) view internal returns(uint){ + function my_func(uint256 a, uint256 b, uint256 c) view internal returns (uint256) { return a * b / c; } } @@ -177,29 +179,29 @@ assertion in test: passed! 🎉 Adapt the following code to your needs: ```solidity -interface Target{ +interface Target { // public/external functions } -contract TestBytecodeOnly{ - Target t; +contract TestBytecodeOnly { + Target target; - constructor() public{ + constructor() public { address target_addr; // init bytecode - bytes memory target_bytecode = hex""; + bytes memory targetCreationBytecode = hex""; - uint size = target_bytecode.length; + uint256 size = targetCreationBytecode.length; - assembly{ - target_addr := create(0, 0xa0, size) // 0xa0 was manually computed. It might require different value according to the compiler version + assembly { + target_addr := create(0, add(targetCreationBytecode, 0x20), size) // Skip the 32 bytes encoded length. } - t = Target(target_addr); + target = Target(target_addr); } // Add helper functions to call the target's functions from the proxy - function echidna_test() public returns(bool){ + function echidna_test() public returns (bool) { // The property to test } } diff --git a/program-analysis/echidna/advanced/using-multi-abi.md b/program-analysis/echidna/advanced/using-multi-abi.md index 1d599946..8dc63011 100644 --- a/program-analysis/echidna/advanced/using-multi-abi.md +++ b/program-analysis/echidna/advanced/using-multi-abi.md @@ -58,16 +58,15 @@ The test harness will instantiate a new `Flag`, and the invariant under test wil ```solidity contract EchidnaTest { - Flag f; + Flag f; - constructor() { - f = new Flag(); - } - - function test_flag_is_false() public { - assert(f.get() == false); - } + constructor() { + f = new Flag(); + } + function test_flag_is_false() public { + assert(f.get() == false); + } } ``` diff --git a/program-analysis/echidna/basic/assertion-checking.md b/program-analysis/echidna/basic/assertion-checking.md index 41442341..500e01d1 100644 --- a/program-analysis/echidna/basic/assertion-checking.md +++ b/program-analysis/echidna/basic/assertion-checking.md @@ -19,14 +19,14 @@ Let's suppose we have a contract like this one: ```solidity contract Incrementor { - uint private counter = 2**200; - - function inc(uint val) public returns (uint){ - uint tmp = counter; - counter += val; - // tmp <= counter - return (counter - tmp); - } + uint256 private counter = 2 ** 200; + + function inc(uint256 val) public returns (uint256) { + uint256 tmp = counter; + counter += val; + // tmp <= counter + return (counter - tmp); + } } ``` @@ -34,14 +34,14 @@ We want to make sure that `tmp` is less than or equal to `counter` after returni ```solidity contract Incrementor { - uint private counter = 2**200; - - function inc(uint val) public returns (uint){ - uint tmp = counter; - counter += val; - assert (tmp <= counter); - return (counter - tmp); - } + uint256 private counter = 2 ** 200; + + function inc(uint256 val) public returns (uint256) { + uint256 tmp = counter; + counter += val; + assert(tmp <= counter); + return (counter - tmp); + } } ``` @@ -49,16 +49,18 @@ We could also use a special event called `AssertionFailed` with any number of pa ```solidity contract Incrementor { - event AssertionFailed(uint); - uint private counter = 2**200; - - function inc(uint val) public returns (uint){ - uint tmp = counter; - counter += val; - if (tmp > counter) - emit AssertionFailed(counter); - return (counter - tmp); - } + event AssertionFailed(uint256); + + uint256 private counter = 2 ** 200; + + function inc(uint256 val) public returns (uint256) { + uint256 tmp = counter; + counter += val; + if (tmp > counter) { + emit AssertionFailed(counter); + } + return (counter - tmp); + } } ``` @@ -93,7 +95,7 @@ As you can see, Echidna reports an assertion failure in the `inc` function. Addi Assertions can be used as alternatives to explicit properties if the conditions to check are directly related to the correct use of some operation `f`. Adding assertions after some code will enforce that the check happens immediately after it was executed: ```solidity -function f(..) public { +function f(...) public { // some complex code ... assert (condition); @@ -105,7 +107,7 @@ On the contrary, using an explicit boolean property will randomly execute transa ```solidity function echidna_assert_after_f() public returns (bool) { - f(..); + f(...); return(condition); } ``` @@ -122,7 +124,7 @@ Assertions can help to overcome this possible issues. For instance, they can be function f(..) public { // some complex code ... - g(..) // this contains an assert + g(...) // this contains an assert ... } ``` @@ -130,10 +132,10 @@ function f(..) public { If `g` is external, then assertion failure can be **only detected in Solidity 0.8.x or later**. ```solidity -function f(..) public { +function f(...) public { // some complex code ... - contract.g(..) // this contains an assert + contract.g(...) // this contains an assert ... } ``` @@ -141,7 +143,7 @@ function f(..) public { In general, we recommend following [John Regehr's advice](https://blog.regehr.org/archives/1091) on using assertions: - Do not force any side effects during the assertion checking. For instance: `assert(ChangeStateAndReturn() == 1)` -- Do not assert obvious statements. For instance `assert(var >= 0)` where `var` is declared as `uint`. +- Do not assert obvious statements. For instance `assert(var >= 0)` where `var` is declared as `uint256`. Finally, please **do not use** `require` instead of `assert`, since Echidna will not be able to detect it (but the contract will revert anyway). @@ -151,14 +153,14 @@ The following summarizes the run of Echidna on our example (remember to use 0.7. ```solidity contract Incrementor { - uint private counter = 2**200; - - function inc(uint val) public returns (uint){ - uint tmp = counter; - counter += val; - assert (tmp <= counter); - return (counter - tmp); - } + uint256 private counter = 2 ** 200; + + function inc(uint256 val) public returns (uint256) { + uint256 tmp = counter; + counter += val; + assert(tmp <= counter); + return (counter - tmp); + } } ``` diff --git a/program-analysis/echidna/basic/common-testing-approaches.md b/program-analysis/echidna/basic/common-testing-approaches.md index 05f3bc48..8265b0a4 100644 --- a/program-analysis/echidna/basic/common-testing-approaches.md +++ b/program-analysis/echidna/basic/common-testing-approaches.md @@ -19,9 +19,9 @@ We will start with two of them, internal and external: In this testing approach, properties are defined inside the contract to test, with complete access to the internal state of the system. ```solidity -Contract InternalTest is System { +contract InternalTest is System { function echidna_state_greater_than_X() public returns (bool) { - return stateVar > X; + return stateVar > X; } } ``` @@ -36,10 +36,11 @@ In the external testing approach, properties are tested using external calls fro ```solidity contract ExternalTest { constructor() public { - addr = address(0x...); + addr = address(0x...); } + function echidna_state_greater_than_X() public returns (bool) { - return System(addr).stateVar() > X; + return System(addr).stateVar() > X; } } ``` @@ -55,15 +56,15 @@ we add one or more functions that performs external call to it. ```solidity contract ExternalTest { constructor() public { - addr = ..; + addr = ...; } function method(...) public returns (...) { - return System(addr).method(..); + return System(addr).method(); } function echidna_state_greater_than_X() public returns (bool) { - return System(addr).stateVar() > X; + return System(addr).stateVar() > X; } } ``` @@ -78,9 +79,11 @@ There are two important points to consider in this approach: ```solidity contract ExternalTest { ... + function methodUsingF(..., uint256 x) public returns (...) { return System(addr).method(.., f(x)); } + ... } ``` @@ -91,14 +94,15 @@ For instance, if we have a property to ensure that the amount of tokens is limit ```solidity contract ExternalTest { - constructor() public { - addr = ..; - MockERC20(..).mint(..); + constructor() { + addr = ...; + MockERC20(...).mint(...); } function echidna_limited_supply() public returns (bool) { return System(addr).balanceOf(...) <= X; } + ... } ``` @@ -130,15 +134,14 @@ mathematical libraries. **Function override**: Solidity allows to override functions, in order to change the functionality of a piece of code, without affecting the rest of the code base. We can use this to disable certain functions in our tests, in order to allow testing using Echidna: ```solidity -Contract InternalTestOverridingSignatures is System { - - function verifySignature(..) public returns (bool) override { - return true; // signatures are always valid +contract InternalTestOverridingSignatures is System { + function verifySignature(...) public override returns (bool) { + return true; // signatures are always valid } function echidna_state_greater_than_X() public returns (bool) { - executeSomethingWithSignature(..) - return stateVar > X; + executeSomethingWithSignature(...); + return stateVar > X; } } ``` @@ -147,14 +150,16 @@ Contract InternalTestOverridingSignatures is System { Instead of using the code as it is, we will create a “model” of the system in Solidity, using mostly the original code. While there is no defined list of steps to build a model, we can show a generic example. Let’s assume we have a complex system that include this piece of code: ```solidity -Contract System { - … +contract System { + ... + function calculateSomething() public returns (uint256) { - if (booleanState) { - stateSomething = (uint256State1 * uint256State2) / 2**128; - return stateSomething / uint128State; - } - … + if (booleanState) { + stateSomething = (uint256State1 * uint256State2) / 2 ** 128; + return stateSomething / uint128State; + } + + ... } } ``` @@ -164,14 +169,13 @@ We are going to create a model (e.g. copy, paste and modify the original code in transformed into a parameter: ```solidity -Contract SystemModel { - - function calculateSomething(bool boolState, uint256 uint256State1, …) public returns (uint256) { - if (boolState) { - stateSomething = (uint256State1 * uint256State2) / 2**128; - return stateSomething / uint128State; - } - … +contract SystemModel { + function calculateSomething(bool boolState, uint256 uint256State1, ...) public returns (uint256) { + if (boolState) { + stateSomething = (uint256State1 * uint256State2) / 2 ** 128; + return stateSomething / uint128State; + } + ... } } ``` diff --git a/program-analysis/echidna/basic/filtering-functions.md b/program-analysis/echidna/basic/filtering-functions.md index e8417054..833374b8 100644 --- a/program-analysis/echidna/basic/filtering-functions.md +++ b/program-analysis/echidna/basic/filtering-functions.md @@ -20,18 +20,18 @@ contract C { bool state3 = false; bool state4 = false; - function f(uint x) public { + function f(uint256 x) public { require(x == 12); state1 = true; } - function g(uint x) public { + function g(uint256 x) public { require(state1); require(x == 8); state2 = true; } - function h(uint x) public { + function h(uint256 x) public { require(state2); require(x == 42); state3 = true; @@ -59,7 +59,6 @@ contract C { function echidna_state4() public returns (bool) { return (!state4); } - } ``` diff --git a/program-analysis/echidna/basic/property-creation.md b/program-analysis/echidna/basic/property-creation.md index 583c1ca6..509e35fb 100644 --- a/program-analysis/echidna/basic/property-creation.md +++ b/program-analysis/echidna/basic/property-creation.md @@ -20,61 +20,62 @@ Let's suppose we have a contract interface like the one below: ```solidity interface DeFi { - ERC20 t; - function getShares(address user) external returns (uint256) - function createShares(uint256 val) external returns (uint256) - function depositShares(uint256 val) external - function withdrawShares(uint256 val) external - function transferShares(address to) external - ... + ERC20 t; + + function getShares(address user) external returns (uint256); + function createShares(uint256 val) external returns (uint256); + function depositShares(uint256 val) external; + function withdrawShares(uint256 val) external; + function transferShares(address to) external; +} ``` In this example, users can deposit tokens using `depositShares`, mint shares using `createShares`, withdraw shares using `withdrawShares`, transfer all shares to another user using `transferShares`, and get the number of shares for any account using `getShares`. We will start with very basic properties: ```solidity contract Test { - DeFi c; - ERC20 token; + DeFi defi; + ERC20 token; - constructor() { - c = DeFi(..); - token.mint(address(this), ...); - } - - function getShares_never_reverts() public { - (bool b,) = c.call(abi.encodeWithSignature("getShares(address)", address(this))); - assert(b); - } + constructor() { + defi = DeFi(...); + token.mint(address(this), ...); + } - function depositShares_never_reverts(uint256 val) public { - if (token.balanceOf(address(this)) >= val) { - (bool b,) = c.call(abi.encodeWithSignature("depositShares(uint256)", val)); + function getShares_never_reverts() public { + (bool b,) = defi.call(abi.encodeWithSignature("getShares(address)", address(this))); assert(b); } - } - function withdrawShares_never_reverts(uint256 val) public { - if (c.getShares(address(this)) >= val) { - (bool b,) = c.call(abi.encodeWithSignature("withdrawShares(uint256)", val)); - assert(b); + function depositShares_never_reverts(uint256 val) public { + if (token.balanceOf(address(this)) >= val) { + (bool b,) = defi.call(abi.encodeWithSignature("depositShares(uint256)", val)); + assert(b); + } } - } - function depositShares_can_revert(uint256 val) public { - if (token.balanceOf(address(this)) < val) { - (bool b,) = c.call(abi.encodeWithSignature("depositShares(uint256)", val)); - assert(!b); + function withdrawShares_never_reverts(uint256 val) public { + if (defi.getShares(address(this)) >= val) { + (bool b,) = defi.call(abi.encodeWithSignature("withdrawShares(uint256)", val)); + assert(b); + } } - } - function withdrawShares_can_revert(uint256 val) public { - if (c.getShares(address(this)) < val) { - (bool b,) = c.call(abi.encodeWithSignature("withdrawShares(uint256)", val)); - assert(!b); + function depositShares_can_revert(uint256 val) public { + if (token.balanceOf(address(this)) < val) { + (bool b,) = defi.call(abi.encodeWithSignature("depositShares(uint256)", val)); + assert(!b); + } } - } + function withdrawShares_can_revert(uint256 val) public { + if (defi.getShares(address(this)) < val) { + (bool b,) = defi.call(abi.encodeWithSignature("withdrawShares(uint256)", val)); + assert(!b); + } + } } + ``` After you have writen your first version of properties, run Echidna to make sure they work as expected. During this tutorial, we will improve them step by step. It is strongly recommended to run the fuzzer at each step to increase the probability of detecting any potential issues. @@ -85,20 +86,21 @@ But you will be surprised how often an unexpected revert/return uncovers a compl Before we continue, we will improve these properties using [try/catch](https://docs.soliditylang.org/en/v0.6.0/control-structures.html#try-catch). The use of a low-level call forces us to manually encode the data, which can be error prone (an error will always cause calls to revert). Note, this will only work if the codebase is using solc 0.6.0 or later: ```solidity - ... - function depositShares_never_reverts(uint256 val) public { +function depositShares_never_reverts(uint256 val) public { if (token.balanceOf(address(this)) >= val) { - try c.depositShares(val) { /* not reverted */ } catch { assert(false); } + try defi.depositShares(val) { /* not reverted */ } + catch { + assert(false); + } } - } +} - function depositShares_can_revert(uint256 val) public { +function depositShares_can_revert(uint256 val) public { if (token.balanceOf(address(this)) < val) { - try c.depositShares(val) { assert(false); } catch { /* reverted */ } + try defi.depositShares(val) { + assert(false); + } catch { /* reverted */ } } - } - ... - } ``` @@ -108,22 +110,24 @@ If the previous properties are passing, this means that the pre-conditions are g Avoiding reverts doesn't mean that the contract is in a valid state. Let's add some basic preconditions: ```solidity - ... - function depositShares_never_reverts(uint256 val) public { +function depositShares_never_reverts(uint256 val) public { if (token.balanceOf(address(this)) >= val) { - try c.depositShares(val) { /* not reverted */ } catch { assert(false); } - assert(c.getShares(address(this)) > 0); + try defi.depositShares(val) { /* not reverted */ } + catch { + assert(false); + } + assert(defi.getShares(address(this)) > 0); } - } +} - function withdrawShares_never_reverts(uint256 val) public { - if (c.getShares(address(this)) >= val) { - try c.withdrawShares(val) { /* not reverted */ } catch { assert(false); } +function withdrawShares_never_reverts(uint256 val) public { + if (defi.getShares(address(this)) >= val) { + try defi.withdrawShares(val) { /* not reverted */ } + catch { + assert(false); + } assert(token.balanceOf(address(this)) > 0); } - } - ... - } ``` @@ -134,19 +138,21 @@ Uhm, it looks like it is not that easy to specify the value of shares/tokens obt In this generic example, it is unclear if there is a way to calculate how many shares or tokens we should receive after executing the deposit/withdraw operations. Of course, if we have that information, we should use it. In any case, what we can do here is to combine these two properties into a single one to be able check more precisely it's preconditions. ```solidity - ... - function deposit_withdraw_shares_never_reverts(uint256 val) public { +function deposit_withdraw_shares_never_reverts(uint256 val) public { uint256 original_balance = token.balanceOf(address(this)); if (original_balance >= val) { - try c.depositShares(val) { /* not reverted */ } catch { assert(false); } - uint256 shares = c.getShares(address(this); + try defi.depositShares(val) { /* not reverted */ } + catch { + assert(false); + } + uint256 shares = defi.getShares(address(this)); assert(shares > 0); - try c.withdrawShares(shares) { /* not reverted */ } catch { assert(false); } + try defi.withdrawShares(shares) { /* not reverted */ } + catch { + assert(false); + } assert(token.balanceOf(address(this)) == original_balance); } - } - ... - } ``` @@ -159,18 +165,21 @@ Two important considerations for this example: We want Echidna to spend most of the execution exploring the contract to test. So, in order to make the properties more efficient, we should avoid dead branches where there is nothing to do. That's why we can improve `depositShares_never_reverts` to use: ```solidity - function depositShares_never_reverts(uint256 val) public { - if(token.balanceOf(address(this)) > 0) { - val = val % (token.balanceOf(address(this)) + 1); - try c.depositShares(val) { /* not reverted */ } catch { assert(false); } - assert(c.getShares(address(this)) > 0); +function depositShares_never_reverts(uint256 val) public { + if (token.balanceOf(address(this)) > 0) { + val = val % (token.balanceOf(address(this)) + 1); + try defi.depositShares(val) { /* not reverted */ } + catch { + assert(false); + } + assert(defi.getShares(address(this)) > 0); } else { - ... // code to test depositing zero tokens + ... // code to test depositing zero tokens } - } +} ``` -Additionally, combining properties does not mean that we will have to remove simpler ones. For instance, if we want to write `withdraw_deposit_shares_never_reverts`, in which we reverse the order of operations (withdraw and then deposit, instead of deposit and then withdraw), we will have to make sure `c.getShares(address(this))` can be positive. An easy way to do it is to keep `depositShares_never_reverts`, since this code allows Echidna to deposit tokens from `address(this)` (otherwise, this is impossible). +Additionally, combining properties does not mean that we will have to remove simpler ones. For instance, if we want to write `withdraw_deposit_shares_never_reverts`, in which we reverse the order of operations (withdraw and then deposit, instead of deposit and then withdraw), we will have to make sure `defi.getShares(address(this))` can be positive. An easy way to do it is to keep `depositShares_never_reverts`, since this code allows Echidna to deposit tokens from `address(this)` (otherwise, this is impossible). ## Summary: How to write good properties diff --git a/program-analysis/echidna/basic/testing-modes.md b/program-analysis/echidna/basic/testing-modes.md index 2ff7be8f..622812a3 100644 --- a/program-analysis/echidna/basic/testing-modes.md +++ b/program-analysis/echidna/basic/testing-modes.md @@ -20,25 +20,23 @@ By default, the "property" testing mode is used, which reports failures using a ```solidity function echidna_property() public returns (bool) { // No arguments are required - // The following statements can trigger a failure if they revert - publicFunction(..); - internalFunction(..); - contract.function(..); + publicFunction(...); + internalFunction(...); + contract.function(...); // The following statement can trigger a failure depending on the returned value - return ..; + return ...; } // side effects are *not* preserved function echidna_revert_property() public returns (bool) { // No arguments is required - // The following statements can *never* trigger a failure - publicFunction(..); - internalFunction(..); - contract.function(..); + publicFunction(...); + internalFunction(...); + contract.function(...); // The following statement will *always* trigger a failure regardless of the value returned - return ..; + return ...; } // side effects are *not* preserved ``` @@ -65,19 +63,18 @@ Using the "assertion" testing mode, Echidna will report an assert violation if: - An `AssertionFailed` event (with any number of parameters) is emitted by any contract. This pseudo-code summarizes how assertions work: ```solidity -function checkInvariant(..) public { // Any number of arguments is supported - +function checkInvariant(...) public { // Any number of arguments is supported // The following statements can trigger a failure using `assert` - assert(..); - publicFunction(..); - internalFunction(..); + assert(...); + publicFunction(...); + internalFunction(...); // The following statement will always trigger a failure even if the execution ends with a revert - emits AssertionFailed(..); + emits AssertionFailed(...); // The following statement will *only* trigger a failure using `assert` if using solc 0.8.x or newer - // To make sure it works in older versions, use the AssertionFailed(..) event - anotherContract.function(..); + // To make sure it works in older versions, use the AssertionFailed(...) event + anotherContract.function(...); } // side effects are preserved ``` @@ -96,8 +93,9 @@ Functions checking assertions do not require any particular name and are execute ```solidity function deposit(uint256 tokens) public { - assert(tokens > 0); // should be strictly positive - .. + assert(tokens > 0); // should be strictly positive + ... +} ``` Developers _should_ avoid doing that and use `require` instead, but if that is not possible because you are calling some contract that is outside your control, you can use the `AssertionFailure` event. @@ -110,8 +108,7 @@ You should use assertions if your invariant is more natural to be expressed usin function testStake(uint256 toStake) public { uint256 balance = balanceOf(msg.sender); toStake = toStake % (balance + 1); - if (toStake < MINSTAKE) // Pre: minimal stake is required - return; + if (toStake < MINSTAKE) return; // Pre: minimal stake is required stake(msg.sender, toStake); // Action: token staking assert(staked(msg.sender) == toStake); // Post: staking amount is toStake assert(balanceOf(msg.sender) == balance - toStake); // Post: balance decreased @@ -132,6 +129,7 @@ function checkDappTest(..) public { // One or more arguments are required publicFunction(..); internalFunction(..); anotherContract.function(..); + // The following statement will never trigger a failure require(.., “FOUNDRY::ASSUME”); } diff --git a/program-analysis/echidna/exercises/Exercise-1.md b/program-analysis/echidna/exercises/Exercise-1.md index 53b9286a..46e79105 100644 --- a/program-analysis/echidna/exercises/Exercise-1.md +++ b/program-analysis/echidna/exercises/Exercise-1.md @@ -13,36 +13,36 @@ Join the team on Slack at: https://empireslacking.herokuapp.com/ #ethereum We will test the following contract _[./exercise1/token.sol](./exercise1/token.sol)_: ```Solidity - contract Ownership{ + contract Ownership { address owner = msg.sender; - function Owner(){ + function Owner() { owner = msg.sender; } - modifier isOwner(){ + modifier isOwner() { require(owner == msg.sender); _; } } - contract Pausable is Ownership{ + contract Pausable is Ownership { bool is_paused; - modifier ifNotPaused(){ + modifier ifNotPaused() { require(!is_paused); _; } - function paused() isOwner public{ + function paused() isOwner public { is_paused = true; } - function resume() isOwner public{ + function resume() isOwner public { is_paused = false; } } - contract Token is Pausable{ - mapping(address => uint) public balances; - function transfer(address to, uint value) ifNotPaused public{ + contract Token is Pausable { + mapping(address => uint256) public balances; + function transfer(address to, uint256 value) ifNotPaused public { balances[msg.sender] -= value; balances[to] += value; } @@ -64,7 +64,7 @@ The skeleton for this exercise is (_[./exercise1/template.sol](./exercise1/templ contract TestToken is Token { address echidna_caller = msg.sender; - constructor() public{ + constructor() public { balances[echidna_caller] = 10000; } // add the property diff --git a/program-analysis/echidna/exercises/Exercise-2.md b/program-analysis/echidna/exercises/Exercise-2.md index 32f44507..94fbcfdf 100644 --- a/program-analysis/echidna/exercises/Exercise-2.md +++ b/program-analysis/echidna/exercises/Exercise-2.md @@ -15,36 +15,36 @@ Join the team on Slack at: https://empireslacking.herokuapp.com/ #ethereum We will test the following contract _[./exercise2/token.sol](./exercise2/token.sol)_: ```Solidity - contract Ownership{ + contract Ownership { address owner = msg.sender; function Owner() public { owner = msg.sender; } - modifier isOwner(){ + modifier isOwner() { require(owner == msg.sender); _; } } - contract Pausable is Ownership{ + contract Pausable is Ownership { bool is_paused; - modifier ifNotPaused(){ + modifier ifNotPaused() { require(!is_paused); _; } - function paused() isOwner public{ + function paused() isOwner public { is_paused = true; } - function resume() isOwner public{ + function resume() isOwner public { is_paused = false; } } - contract Token is Pausable{ - mapping(address => uint) public balances; - function transfer(address to, uint value) ifNotPaused public{ + contract Token is Pausable { + mapping(address => uint256) public balances; + function transfer(address to, uint256 value) ifNotPaused public { balances[msg.sender] -= value; balances[to] += value; } @@ -66,7 +66,7 @@ The skeleton for this exercise is (_[./exercise2/template.sol](./exercise2/templ import "token.sol"; contract TestToken is Token { address echidna_caller = msg.sender; - constructor(){ + constructor() { paused(); // pause the contract owner = 0x0; // lose ownership } diff --git a/program-analysis/echidna/exercises/Exercise-3.md b/program-analysis/echidna/exercises/Exercise-3.md index 1aab063a..ac4202dd 100644 --- a/program-analysis/echidna/exercises/Exercise-3.md +++ b/program-analysis/echidna/exercises/Exercise-3.md @@ -15,36 +15,36 @@ Join the team on Slack at: https://empireslacking.herokuapp.com/ #ethereum We will test the following contract _[./exercise3/token.sol](./exercise3/token.sol)_: ```Solidity - contract Ownership{ + contract Ownership { address owner = msg.sender; constructor() public { owner = msg.sender; } - modifier isOwner(){ + modifier isOwner() { require(owner == msg.sender); _; } } - contract Pausable is Ownership{ + contract Pausable is Ownership { bool is_paused; - modifier ifNotPaused(){ + modifier ifNotPaused() { require(!is_paused); _; } - function paused() isOwner public{ + function paused() isOwner public { is_paused = true; } - function resume() isOwner public{ + function resume() isOwner public { is_paused = false; } } - contract Token is Pausable{ - mapping(address => uint) public balances; - function transfer(address to, uint value) ifNotPaused public{ + contract Token is Pausable { + mapping(address => uint256) public balances; + function transfer(address to, uint256 value) ifNotPaused public { require(balances[msg.sender] >= value); balances[msg.sender] -= value; balances[to] += value; @@ -59,7 +59,7 @@ Consider the following extension of the token (_[./exercise3/mintable.sol](./exe ```Solidity import "token.sol"; - contract MintableToken is Token{ + contract MintableToken is Token { int totalMinted; int totalMintable; @@ -67,7 +67,7 @@ Consider the following extension of the token (_[./exercise3/mintable.sol](./exe totalMintable = _totalMintable; } - function mint(uint value) isOwner() public{ + function mint(uint256 value) isOwner() public { require(int(value) + totalMinted < totalMintable); totalMinted += int(value); balances[msg.sender] += value; diff --git a/program-analysis/echidna/exercises/Exercise-4.md b/program-analysis/echidna/exercises/Exercise-4.md index 9f093539..aa8f3426 100644 --- a/program-analysis/echidna/exercises/Exercise-4.md +++ b/program-analysis/echidna/exercises/Exercise-4.md @@ -17,36 +17,36 @@ Join the team on Slack at: https://empireslacking.herokuapp.com/ #ethereum We will test the following contract _[./exercise4/token.sol](./exercise4/token.sol)_: ```Solidity - contract Ownership{ + contract Ownership { address owner = msg.sender; - function Owner() public{ + function Owner() public { owner = msg.sender; } - modifier isOwner(){ + modifier isOwner() { require(owner == msg.sender); _; } } - contract Pausable is Ownership{ + contract Pausable is Ownership { bool is_paused; - modifier ifNotPaused(){ + modifier ifNotPaused() { require(!is_paused); _; } - function paused() isOwner public{ + function paused() isOwner public { is_paused = true; } - function resume() isOwner public{ + function resume() isOwner public { is_paused = false; } } - contract Token is Pausable{ - mapping(address => uint) public balances; - function transfer(address to, uint value) ifNotPaused public{ + contract Token is Pausable { + mapping(address => uint256) public balances; + function transfer(address to, uint256 value) ifNotPaused public { balances[msg.sender] -= value; balances[to] += value; } diff --git a/program-analysis/echidna/frequently_asked_questions.md b/program-analysis/echidna/frequently_asked_questions.md index bc51f398..ccafacda 100644 --- a/program-analysis/echidna/frequently_asked_questions.md +++ b/program-analysis/echidna/frequently_asked_questions.md @@ -102,17 +102,17 @@ Use `--format text` and open an issue with the error you see in your console or Sometimes it is useful to create small properties or assertions to test that the tool executed them correctly. For instance, for property mode: ```solidity - function echidna_test() public returns (bool) { - return false; - } +function echidna_test() public returns (bool) { + return false; +} ``` And for assertion mode: ```solidity - function test_assert_false() public { - assert(false); - } +function test_assert_false() public { + assert(false); +} ``` If these are not failing, please [open an issue](https://github.com/crytic/echidna/issues) so we can take a look. diff --git a/program-analysis/echidna/fuzzing_tips.md b/program-analysis/echidna/fuzzing_tips.md index 49b30a7b..e60e2769 100644 --- a/program-analysis/echidna/fuzzing_tips.md +++ b/program-analysis/echidna/fuzzing_tips.md @@ -10,7 +10,7 @@ The following describe fuzzing tips to make Echidna more efficient: To filter inputs, `%` is more efficient than adding `require` or `if` statements. For example, if you are a fuzzing a `operation(uint256 index, ..)` where `index` is supposed to be less than `10**18`, use: ```solidity -function operation(uint index, ...) public{ +function operation(uint256 index, ...) public { index = index % 10**18 ... } @@ -21,7 +21,7 @@ If `require(index <= 10**18)` is used instead, many transactions generated will This can also be generalized define a min and max range, for example: ```solidity -function operation(uint balance, ...) public{ +function operation(uint256 balance, ...) public { balance = MIN_BALANCE + balance % (MAX_BALANCE - MIN_BALANCE); ... } @@ -30,11 +30,11 @@ function operation(uint balance, ...) public{ Will ensure that `balance` is always between `MIN_BALANCE` and `MAX_BALANCE`, without discarding any generated transactions. As expected, this will speed up the exploration, but at the cost of avoiding certain paths in your code. To overcome this issue, the usual solution is to have two functions: ```solidity -function operation(uint balance, ...) public{ +function operation(uint256 balance, ...) public { ... // original code } -function safeOperation(uint balance, ...) public{ +function safeOperation(uint256 balance, ...) public { balance = MIN_BALANCE + balance % (MAX_BALANCE - MIN_BALANCE); // safe balance ... } @@ -47,24 +47,25 @@ So Echidna is free to use any of these, exploring safe and unsafe usage of the i When a dynamic array is used as input, Echidna will limit the size of it to 32 elements: ```solidity -function operation(uint256[] data, ...) public{ +function operation(uint256[] calldata data, ...) public { ... // use of data } ``` -This is because deserializing dynamic arrays is slow and can take some amount of memory during the execution. Dynamic arrays are also problematic since they are hard to mutate. Despite this, Echidna includes some specific mutators to remove/repeat elements or cut elements. These mutators are performed using the collected corpus. In general, we suggest the use of `push(..)` and `pop()` functions to handle the exploration of dynamic arrays used as inputs: +This is because deserializing dynamic arrays is slow and can take some amount of memory during the execution. Dynamic arrays are also problematic since they are hard to mutate. Despite this, Echidna includes some specific mutators to remove/repeat elements or cut elements. These mutators are performed using the collected corpus. In general, we suggest the use of `push(...)` and `pop()` functions to handle the exploration of dynamic arrays used as inputs: ```solidity private uint256[] data; -function push(uint256 x) public{ + +function push(uint256 x) public { data.push(x); } -function pop() public{ +function pop() public { data.pop(); } -function operation(...) public{ +function operation(...) public { ... // use of data } ``` diff --git a/program-analysis/echidna/introduction/how-to-test-a-property.md b/program-analysis/echidna/introduction/how-to-test-a-property.md index c0cc2dae..e583b25c 100644 --- a/program-analysis/echidna/introduction/how-to-test-a-property.md +++ b/program-analysis/echidna/introduction/how-to-test-a-property.md @@ -14,16 +14,16 @@ We will see how to test a smart contract with Echidna. The target is the following smart contract (_[../example/token.sol](../example/token.sol)_): ```Solidity - contract Token{ - mapping(address => uint) public balances; - function airdrop() public{ + contract Token { + mapping(address => uint256) public balances; + function airdrop() public { balances[msg.sender] = 1000; } - function consume() public{ + function consume() public { require(balances[msg.sender]>0); balances[msg.sender] -= 1; } - function backdoor() public{ + function backdoor() public { balances[msg.sender] += 1; } } @@ -53,7 +53,7 @@ Echidna will: The following property checks that the caller can have no more than 1000 tokens: ```Solidity - function echidna_balance_under_1000() public view returns(bool){ + function echidna_balance_under_1000() public view returns (bool) { return balances[msg.sender] <= 1000; } ``` @@ -61,8 +61,8 @@ The following property checks that the caller can have no more than 1000 tokens: Use inheritance to separate your contract from your properties: ```Solidity - contract TestToken is Token{ - function echidna_balance_under_1000() public view returns(bool){ + contract TestToken is Token { + function echidna_balance_under_1000() public view returns (bool) { return balances[msg.sender] <= 1000; } } @@ -102,9 +102,9 @@ $ echidna-test contract.sol --contract MyContract The following summarizes the run of Echidna on our example: ```Solidity - contract TestToken is Token{ + contract TestToken is Token { constructor() public {} - function echidna_balance_under_1000() public view returns(bool){ + function echidna_balance_under_1000() public view returns (bool) { return balances[msg.sender] <= 1000; } } diff --git a/program-analysis/manticore/adding-constraints.md b/program-analysis/manticore/adding-constraints.md index 8fb3ff26..6d96fe42 100644 --- a/program-analysis/manticore/adding-constraints.md +++ b/program-analysis/manticore/adding-constraints.md @@ -19,7 +19,7 @@ documentation of `f()` states that the function is never called with `a == 65`, ```Solidity pragma solidity >=0.4.24 <0.6.0; contract Simple { - function f(uint a) payable public{ + function f(uint256 a) payable public { if (a == 65) { revert(); } diff --git a/program-analysis/manticore/exercises/exercise2.md b/program-analysis/manticore/exercises/exercise2.md index 917891df..f819de17 100644 --- a/program-analysis/manticore/exercises/exercise2.md +++ b/program-analysis/manticore/exercises/exercise2.md @@ -31,7 +31,7 @@ state.platform.transactions[-1].return_data - The data returned needs to be deserialized: ```python -data = ABI.deserialize("uint", data) +data = ABI.deserialize("uint256", data) ``` - You can use the template proposed in [exercise2/template.py](./exercise2/template.py) diff --git a/program-analysis/manticore/getting-throwing-paths.md b/program-analysis/manticore/getting-throwing-paths.md index 2d92e0ed..4cb47d15 100644 --- a/program-analysis/manticore/getting-throwing-paths.md +++ b/program-analysis/manticore/getting-throwing-paths.md @@ -16,7 +16,7 @@ We will now improve [the previous example](running-under-manticore.md) and gener ```Solidity pragma solidity >=0.4.24 <0.6.0; contract Simple { - function f(uint a) payable public{ + function f(uint256 a) payable public { if (a == 65) { revert(); } @@ -47,7 +47,7 @@ The data returned by the last transaction is an array, which can be converted to ```python data = state.platform.transactions[0].return_data -data = ABI.deserialize("uint", data) +data = ABI.deserialize("uint256", data) ``` ## How to generate testcase diff --git a/program-analysis/manticore/running-under-manticore.md b/program-analysis/manticore/running-under-manticore.md index 4d471c77..02d95f6d 100644 --- a/program-analysis/manticore/running-under-manticore.md +++ b/program-analysis/manticore/running-under-manticore.md @@ -14,7 +14,7 @@ We will see how to explore a smart contract with the Manticore API. The target i ```Solidity pragma solidity >=0.4.24 <0.6.0; contract Simple { - function f(uint a) payable public{ + function f(uint256 a) payable public { if (a == 65) { revert(); } @@ -98,7 +98,7 @@ A Solidity contract can be deployed using [m.solidity_create_contract](https://m source_code = ''' pragma solidity >=0.4.24 <0.6.0; contract Simple { - function f(uint a) payable public{ + function f(uint256 a) payable public { if (a == 65) { revert(); } @@ -152,7 +152,7 @@ If the data is symbolic, Manticore will explore all the functions of the contrac #### Named transaction Functions can be executed through their name. -To execute `f(uint var)` with a symbolic value, from user_account, and with 0 ether, use: +To execute `f(uint256 var)` with a symbolic value, from user_account, and with 0 ether, use: ```python3 symbolic_var = m.make_symbolic_value() diff --git a/program-analysis/manticore/symbolic-execution-introduction.md b/program-analysis/manticore/symbolic-execution-introduction.md index 7f559f00..d0c41467 100644 --- a/program-analysis/manticore/symbolic-execution-introduction.md +++ b/program-analysis/manticore/symbolic-execution-introduction.md @@ -16,12 +16,10 @@ This approach produces no false positives in the sense that all identified progr To get an insigh of how DSE works, consider the following example: ```solidity -function f(uint a){ - - if (a == 65) { - // A bug is present - } - +function f(uint256 a) { + if (a == 65) { + // A bug is present + } } ``` @@ -39,9 +37,9 @@ Manticore allows a full control over all the execution of each path. As a result Consider the following example: ```solidity -function unsafe_add(uint a, uint b) returns(uint c){ - c = a + b; // no overflow protection - return c; +function unsafe_add(uint256 a, uint256 b) returns (uint256 c) { + c = a + b; // no overflow protection + return c; } ``` @@ -58,11 +56,11 @@ If it is possible to find a valuation of `a` and `b` for which the path predicat If you consider a fixed version: ```solidity -function safe_add(uint a, uint b) returns(uint c){ - c = a + b; - require(c>=a); - require(c>=b); - return c; +function safe_add(uint256 a, uint256 b) returns (uint256 c) { + c = a + b; + require(c >= a); + require(c >= b); + return c; } ``` diff --git a/program-analysis/slither/exercise1.md b/program-analysis/slither/exercise1.md index c4d5e8ae..b25e1088 100644 --- a/program-analysis/slither/exercise1.md +++ b/program-analysis/slither/exercise1.md @@ -5,7 +5,7 @@ The goal is to create a script that fills a missing feature of Solidity: functio [exercises/exercise1/coin.sol](exercises/exercise1/coin.sol) contains a function that must never be overridden: ```solidity -_mint(address dst, uint val) +_mint(address dst, uint256 val) ``` Use Slither to ensure that no contract that inherits Coin overrides this function. diff --git a/program-analysis/slither/static_analysis.md b/program-analysis/slither/static_analysis.md index 8bbc0b2d..8ce86633 100644 --- a/program-analysis/slither/static_analysis.md +++ b/program-analysis/slither/static_analysis.md @@ -21,8 +21,8 @@ AST are used every time the compiler parses code. It is probably the most basic In a nutshell, an AST is a structured tree where, usually, each leaf contains a variable or a constant and internal nodes are operands or control flow operations. Consider the following code: ```solidity -function safeAdd(uint a, uint b) pure internal returns(uint){ - if(a + b <= a){ +function safeAdd(uint256 a, uint256 b) pure internal returns (uint256) { + if(a + b <= a) { revert(); } return a + b; @@ -106,7 +106,7 @@ An example of data dependency usage can be found in the [dangerous strict equali If your analysis navigates through the CFG and follows the edges, you are likely to see already visited nodes. For example, if a loop is presented as shown below: ```solidity -for(uint i; i < range; ++){ +for(uint256 i; i < range; ++) { variable_a += 1 } ```