From 0be853ae33ddc6c96db337fc64f3c8c3caafecd1 Mon Sep 17 00:00:00 2001 From: Omar Ganiev Date: Thu, 2 Mar 2023 16:51:11 +0400 Subject: [PATCH 1/6] Adding the exact balance check rule --- solidity/exact-balance-check.sol | 43 +++++++++++++++++++++++++++++++ solidity/exact-balance-check.yaml | 18 +++++++++++++ 2 files changed, 61 insertions(+) create mode 100644 solidity/exact-balance-check.sol create mode 100644 solidity/exact-balance-check.yaml diff --git a/solidity/exact-balance-check.sol b/solidity/exact-balance-check.sol new file mode 100644 index 0000000..d985a10 --- /dev/null +++ b/solidity/exact-balance-check.sol @@ -0,0 +1,43 @@ +contract Foobar { + function doit1(address ext) { + // ruleid: exact-balance-check + require( + 1==1 && + (IERC20(ext).balanceOf(address(this)) == 1337) || + 1==2, + "Wrong balance!" + ); + // do smth + } + + function doit2(address ext) { + require( + 1==1 && + (address(ext).balance == 1337) || + 1==2, + "Wrong balance!" + ); + // do smth + } + + function doit_safe(address ext) { + // ok: exact-balance-check + require( + 1==1 && + (IERC20(ext).balanceOf(address(this)) >= 1337) || + 1==2, + "Wrong balance!" + ); + // do smth + } + + function doit2_safe(address ext) { + require( + 1==1 && + (address(ext).balance <= 1337) || + 1==2, + "Wrong balance!" + ); + // do smth + } +} diff --git a/solidity/exact-balance-check.yaml b/solidity/exact-balance-check.yaml new file mode 100644 index 0000000..993f574 --- /dev/null +++ b/solidity/exact-balance-check.yaml @@ -0,0 +1,18 @@ +rules: + - + id: exact-balance-check + message: Testing the balance of an account as a basis for some action has risks associated with unexpected receipt of ether or another token, including tokens deliberately transfered to cause such tests to fail, as an MEV attack. + metadata: + category: logic + references: + - https://entethalliance.org/specs/ethtrust-sl/v1/#req-1-exact-balance-check + mode: taint + pattern-sinks: + - pattern: require(...) + pattern-sources: + - pattern-either: + - pattern: $T.balanceOf(...) == ... + - pattern: $T.balance == ... + languages: + - solidity + severity: ERROR From 918d4b0b5231dfa6ff8fd35e12168a5f048d41ff Mon Sep 17 00:00:00 2001 From: Omar Ganiev Date: Thu, 2 Mar 2023 16:59:54 +0400 Subject: [PATCH 2/6] Fix the exact balance check rule --- solidity/exact-balance-check.sol | 2 ++ 1 file changed, 2 insertions(+) diff --git a/solidity/exact-balance-check.sol b/solidity/exact-balance-check.sol index d985a10..49c65ec 100644 --- a/solidity/exact-balance-check.sol +++ b/solidity/exact-balance-check.sol @@ -11,6 +11,7 @@ contract Foobar { } function doit2(address ext) { + // ruleid: exact-balance-check require( 1==1 && (address(ext).balance == 1337) || @@ -32,6 +33,7 @@ contract Foobar { } function doit2_safe(address ext) { + // ok: exact-balance-check require( 1==1 && (address(ext).balance <= 1337) || From 99e7684c7be9c626a453d7b8c3f3adcf854e5baa Mon Sep 17 00:00:00 2001 From: Omar Ganiev Date: Thu, 2 Mar 2023 17:35:29 +0400 Subject: [PATCH 3/6] Fix the taint mode of the exact balance check rule --- solidity/exact-balance-check.sol | 13 ++++++++----- solidity/exact-balance-check.yaml | 12 ++++++++---- 2 files changed, 16 insertions(+), 9 deletions(-) diff --git a/solidity/exact-balance-check.sol b/solidity/exact-balance-check.sol index 49c65ec..bf726e3 100644 --- a/solidity/exact-balance-check.sol +++ b/solidity/exact-balance-check.sol @@ -1,9 +1,12 @@ contract Foobar { function doit1(address ext) { - // ruleid: exact-balance-check + uint256 bal = IERC20(ext).balanceOf(address(this)); + // ok: exact-balance-check + bal == 1338; require( 1==1 && - (IERC20(ext).balanceOf(address(this)) == 1337) || + // ruleid: exact-balance-check + (bal == 1337) || 1==2, "Wrong balance!" ); @@ -11,9 +14,9 @@ contract Foobar { } function doit2(address ext) { - // ruleid: exact-balance-check require( 1==1 && + // ruleid: exact-balance-check (address(ext).balance == 1337) || 1==2, "Wrong balance!" @@ -22,9 +25,9 @@ contract Foobar { } function doit_safe(address ext) { - // ok: exact-balance-check require( 1==1 && + // ok: exact-balance-check (IERC20(ext).balanceOf(address(this)) >= 1337) || 1==2, "Wrong balance!" @@ -33,9 +36,9 @@ contract Foobar { } function doit2_safe(address ext) { - // ok: exact-balance-check require( 1==1 && + // ok: exact-balance-check (address(ext).balance <= 1337) || 1==2, "Wrong balance!" diff --git a/solidity/exact-balance-check.yaml b/solidity/exact-balance-check.yaml index 993f574..85266b8 100644 --- a/solidity/exact-balance-check.yaml +++ b/solidity/exact-balance-check.yaml @@ -7,12 +7,16 @@ rules: references: - https://entethalliance.org/specs/ethtrust-sl/v1/#req-1-exact-balance-check mode: taint + options: + taint_unify_mvars: true pattern-sinks: - - pattern: require(...) + - patterns: + - pattern-inside: require(...) + - pattern: $X == ... pattern-sources: - - pattern-either: - - pattern: $T.balanceOf(...) == ... - - pattern: $T.balance == ... + - pattern-either: + - pattern: $T.balanceOf($A) + - pattern: $T.balance languages: - solidity severity: ERROR From f8f8a20fc0616d0ff3b0886eb121f177470ca7e6 Mon Sep 17 00:00:00 2001 From: Omar Ganiev Date: Thu, 2 Mar 2023 18:02:38 +0400 Subject: [PATCH 4/6] Another fix for the exact balance check rule --- solidity/exact-balance-check.sol | 11 +++++++++++ solidity/exact-balance-check.yaml | 6 +++--- 2 files changed, 14 insertions(+), 3 deletions(-) diff --git a/solidity/exact-balance-check.sol b/solidity/exact-balance-check.sol index bf726e3..700ffe9 100644 --- a/solidity/exact-balance-check.sol +++ b/solidity/exact-balance-check.sol @@ -24,6 +24,17 @@ contract Foobar { // do smth } + function doit3(address ext) { + require( + 1==1 && + // ruleid: exact-balance-check + (1337 == address(ext).balance) || + 1==2, + "Wrong balance!" + ); + // do smth + } + function doit_safe(address ext) { require( 1==1 && diff --git a/solidity/exact-balance-check.yaml b/solidity/exact-balance-check.yaml index 85266b8..bdb4c1c 100644 --- a/solidity/exact-balance-check.yaml +++ b/solidity/exact-balance-check.yaml @@ -7,12 +7,12 @@ rules: references: - https://entethalliance.org/specs/ethtrust-sl/v1/#req-1-exact-balance-check mode: taint - options: - taint_unify_mvars: true pattern-sinks: - patterns: - pattern-inside: require(...) - - pattern: $X == ... + - pattern-either: + - pattern: $X == ... + - pattern: ... == $X pattern-sources: - pattern-either: - pattern: $T.balanceOf($A) From ea36dd7b0fa238c733981bd7b2bf2f782abf7273 Mon Sep 17 00:00:00 2001 From: Omar Ganiev Date: Thu, 2 Mar 2023 20:02:20 +0400 Subject: [PATCH 5/6] Add the checks-effects-interactions pattern rule --- solidity/checks-effects-interactions-gen.py | 78 ++++ ...checks-effects-interactions-heuristic.yaml | 46 +++ solidity/checks-effects-interactions.sol | 32 ++ solidity/checks-effects-interactions.yaml | 335 ++++++++++++++++++ 4 files changed, 491 insertions(+) create mode 100644 solidity/checks-effects-interactions-gen.py create mode 100644 solidity/checks-effects-interactions-heuristic.yaml create mode 100644 solidity/checks-effects-interactions.sol create mode 100644 solidity/checks-effects-interactions.yaml diff --git a/solidity/checks-effects-interactions-gen.py b/solidity/checks-effects-interactions-gen.py new file mode 100644 index 0000000..36f83d5 --- /dev/null +++ b/solidity/checks-effects-interactions-gen.py @@ -0,0 +1,78 @@ +TEMPLATE = '''rules: + - + id: checks-effects-interactions + message: The Checks-Effects-Interactions pattern ensures that validation of the request, and changes to the state variables of the contract, are performed before any interactions take place with other contracts. When contracts are implemented this way, the scope for Re-entrancy Attacks is reduced significantly. + metadata: + category: logic + references: + - https://entethalliance.org/specs/ethtrust-sl/v1/#req-1-use-c-e-i + patterns: + - pattern-inside: + contract $C { + $TYPE $STORAGE; + ... + } + - pattern-either: + %s + languages: + - solidity + severity: ERROR +''' + +PART = '''- pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + %s + ... + } + ''' + +PLACEHOLDER = '' + +operators = '-+/*%^|&' +for op in operators: + for recursion in xrange(3): + PLACEHOLDER += PART % ('$STORAGE%s %s= ...;' % ('[...]' * recursion, op)) + +for op in '+-': + for recursion in xrange(3): + PLACEHOLDER += PART % ('<... $STORAGE%s%s ...>;' % ('[...]' * recursion, op * 2)) + PLACEHOLDER += PART % ('<... %s$STORAGE%s ...>;' % (op * 2, '[...]' * recursion)) + +print TEMPLATE % PLACEHOLDER + +TEMPLATE2 = ''' - + id: checks-effects-interactions-heuristic + message: The Checks-Effects-Interactions pattern ensures that validation of the request, and changes to the state variables of the contract, are performed before any interactions take place with other contracts. When contracts are implemented this way, the scope for Re-entrancy Attacks is reduced significantly. + metadata: + category: logic + references: + - https://entethalliance.org/specs/ethtrust-sl/v1/#req-1-use-c-e-i + patterns: + - pattern-inside: + contract $C { + ... + } + - pattern: + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $WRITE(...) ...>; + ... + } + - metavariable-regex: + metavariable: $WRITE + regex: (write|change|increase|decrease|delete|remove|add) + languages: + - solidity + severity: ERROR +''' + +#PLACEHOLDER = '' +#for recursion in xrange(3): +# PLACEHOLDER += PART % ('<... $WRITE($STORAGE%s) ...>;' % ('[...]' * recursion)) + +print TEMPLATE2 diff --git a/solidity/checks-effects-interactions-heuristic.yaml b/solidity/checks-effects-interactions-heuristic.yaml new file mode 100644 index 0000000..e163615 --- /dev/null +++ b/solidity/checks-effects-interactions-heuristic.yaml @@ -0,0 +1,46 @@ +rules: + - + id: checks-effects-interactions-heuristic + message: The Checks-Effects-Interactions pattern ensures that validation of the request, and changes to the state variables of the contract, are performed before any interactions take place with other contracts. When contracts are implemented this way, the scope for Re-entrancy Attacks is reduced significantly. + metadata: + category: logic + references: + - https://entethalliance.org/specs/ethtrust-sl/v1/#req-1-use-c-e-i + patterns: + - pattern-inside: + contract $C { + $TYPE $STORAGE; + ... + } + - pattern-either: + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $WRITE($STORAGE) ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $WRITE($STORAGE[...]) ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $WRITE($STORAGE[...][...]) ...>; + ... + } + + - metavariable-regex: + metavariable: $WRITE + regex: (write|change|increase|decrease|delete|remove|add) + languages: + - solidity + severity: ERROR diff --git a/solidity/checks-effects-interactions.sol b/solidity/checks-effects-interactions.sol new file mode 100644 index 0000000..fd385ac --- /dev/null +++ b/solidity/checks-effects-interactions.sol @@ -0,0 +1,32 @@ +contract Sample { + mapping(address => uint) balances; + + function deposit() public payable { + balances[msg.sender] = msg.value; + } + + // ok: checks-effects-interactions + function withdrawSafe(uint amount) public { + require(balances[msg.sender] >= amount); + balances[msg.sender] -= amount; + msg.sender.transfer(amount); + } + + // ruleid: checks-effects-interactions + function withdrawUnsafe(uint amount) public { + require(balances[msg.sender] >= amount); + msg.sender.transfer(amount); + balances[msg.sender] -= amount; + } + + // ruleid: checks-effects-interactions-heuristic + function withdrawUnsafe2(uint amount) public { + require(balances[msg.sender] >= amount); + msg.sender.transfer(amount); + decreaseBalance(msg.sender, amount); + } + + function decreaseBalance(address who, uint amount) private { + balances[who] -= amount; + } +} \ No newline at end of file diff --git a/solidity/checks-effects-interactions.yaml b/solidity/checks-effects-interactions.yaml new file mode 100644 index 0000000..c322c4e --- /dev/null +++ b/solidity/checks-effects-interactions.yaml @@ -0,0 +1,335 @@ +rules: + - + id: checks-effects-interactions + message: The Checks-Effects-Interactions pattern ensures that validation of the request, and changes to the state variables of the contract, are performed before any interactions take place with other contracts. When contracts are implemented this way, the scope for Re-entrancy Attacks is reduced significantly. + metadata: + category: logic + references: + - https://entethalliance.org/specs/ethtrust-sl/v1/#req-1-use-c-e-i + patterns: + - pattern-inside: + contract $C { + $TYPE $STORAGE; + ... + } + - pattern-either: + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE -= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...] -= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...][...] -= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE += ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...] += ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...][...] += ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE /= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...] /= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...][...] /= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE *= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...] *= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...][...] *= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE %= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...] %= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...][...] %= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE ^= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...] ^= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...][...] ^= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE |= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...] |= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...][...] |= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE &= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...] &= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + $STORAGE[...][...] &= ...; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $STORAGE++ ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... ++$STORAGE ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $STORAGE[...]++ ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... ++$STORAGE[...] ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $STORAGE[...][...]++ ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... ++$STORAGE[...][...] ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $STORAGE-- ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... --$STORAGE ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $STORAGE[...]-- ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... --$STORAGE[...] ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $STORAGE[...][...]-- ...>; + ... + } + - pattern: | + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... --$STORAGE[...][...] ...>; + ... + } + + languages: + - solidity + severity: ERROR + + - + id: checks-effects-interactions-heuristic + message: The Checks-Effects-Interactions pattern ensures that validation of the request, and changes to the state variables of the contract, are performed before any interactions take place with other contracts. When contracts are implemented this way, the scope for Re-entrancy Attacks is reduced significantly. + metadata: + category: logic + references: + - https://entethalliance.org/specs/ethtrust-sl/v1/#req-1-use-c-e-i + patterns: + - pattern-inside: + contract $C { + ... + } + - pattern: + function $F(...) { + ... + $ADDR.$FUNC(...); + ... + <... $WRITE(...) ...>; + ... + } + - metavariable-regex: + metavariable: $WRITE + regex: (write|change|increase|decrease|delete|remove|add) + languages: + - solidity + severity: ERROR + From cbe72c6c0fc1d2f51a03ce52a9e6fc99e9e8c924 Mon Sep 17 00:00:00 2001 From: Omar Ganiev Date: Thu, 2 Mar 2023 20:18:28 +0400 Subject: [PATCH 6/6] Delete checks-effects-interactions-heuristic.yaml --- ...checks-effects-interactions-heuristic.yaml | 46 ------------------- 1 file changed, 46 deletions(-) delete mode 100644 solidity/checks-effects-interactions-heuristic.yaml diff --git a/solidity/checks-effects-interactions-heuristic.yaml b/solidity/checks-effects-interactions-heuristic.yaml deleted file mode 100644 index e163615..0000000 --- a/solidity/checks-effects-interactions-heuristic.yaml +++ /dev/null @@ -1,46 +0,0 @@ -rules: - - - id: checks-effects-interactions-heuristic - message: The Checks-Effects-Interactions pattern ensures that validation of the request, and changes to the state variables of the contract, are performed before any interactions take place with other contracts. When contracts are implemented this way, the scope for Re-entrancy Attacks is reduced significantly. - metadata: - category: logic - references: - - https://entethalliance.org/specs/ethtrust-sl/v1/#req-1-use-c-e-i - patterns: - - pattern-inside: - contract $C { - $TYPE $STORAGE; - ... - } - - pattern-either: - - pattern: | - function $F(...) { - ... - $ADDR.$FUNC(...); - ... - <... $WRITE($STORAGE) ...>; - ... - } - - pattern: | - function $F(...) { - ... - $ADDR.$FUNC(...); - ... - <... $WRITE($STORAGE[...]) ...>; - ... - } - - pattern: | - function $F(...) { - ... - $ADDR.$FUNC(...); - ... - <... $WRITE($STORAGE[...][...]) ...>; - ... - } - - - metavariable-regex: - metavariable: $WRITE - regex: (write|change|increase|decrease|delete|remove|add) - languages: - - solidity - severity: ERROR