Gnosis

`execTransaction`

A reentrancy vulnerability exists, since checkSignatures is called before nonce is incremented:

https://github.com/gnosis/safe-contracts/blob/v0.1.0/contracts/GnosisSafe.sol#L90-L92

Here checkSignatures can call an external contract, ISignatureValidator.isValidSignature():

https://github.com/gnosis/safe-contracts/blob/v0.1.0/contracts/GnosisSafe.sol#L161

which may initiate the same transaction using the same calldata, where nonce will remain the same, and thus the same txHashData will be generated, allowing the same signatures to be used to approve the same transaction multiple times.

At least, a malicious owner can execute a transaction multiple times, without the approval of the other owners, as long as gas remains. Moreover, if a benign owner calls another malicious contract for the signature validation, the malicious contract can exploit it even if he is not an owner.

Recommendation: Increment nonce before calling checkSignatures.

zero and precompiled contract addresses

execTransaction does not reject the case of to being the zero address 0x0, which may lead to an internal transaction to the zero address, via the following function call sequence:

Unlike a regular transaction to the zero address, which creates a new account, an internal transaction to the zero address behaves the same as other transactions to non-zero addresses, i.e., sending the ether to the zero address account (which indeed exists: https://etherscan.io/address/0x0000000000000000000000000000000000000000) and executing the code associated to it (which is empty in this case).

Although it is the users' responsibility that ensures correctness of the transaction data, it is quite possible that a certain user may not be aware of the difference between regular and internal transactions to the zero address, sending a transaction data to execTransaction with to == 0x0, expecting that it creates a new account. Since an internal transaction to the zero address mostly succeeds (note that it spends a little gas, without needing to pay the G_newaccount (25,000) gas fee since the zero-address account already exists), it may cause the ether stuck at 0x0, which could be serious when the user attaches a large amount of ether as a startup fund for the new account.

Recommendation:

reject execTransaction when to == address(0).

Minor Related Note:

handlePayment sends the ether to receiver:

https://github.com/gnosis/safe-contracts/blob/v0.1.0/contracts/GnosisSafe.sol#L120

where receiver is non-zero, since tx.origin cannot be zero. But, receiver could be still a non-owned account, especially one of the precompiled (0x1 - 0x8) contract addresses. Here receiver.send(amount) will succeed even with the small gas stipend 2300 for some precompiled contracts (at least, 0x2, 0x3, 0x4, and 0x6). Below is the gas cost for executing each precompiled contract.

0x1: ECREC: 3000
0x2: SHA256: 60 + 12 * (byte-size-of-call-data)
0x3: RIP160: 600 + 120 * (byte-size-of-call-data)
0x4: ID: 15 + 3 * (byte-size-of-call-data)
0x5: MODEXP: (complex-gas-cost-model)
0x6: ECADD: 500
0x7: ECMUL: 40000
0x8: ECPAIRING: 100000 + ...

`checkSignatures`

Local validity check

checkSignatures checks only the first threshold number of signatures. Thus, the validity of the remaining signatures does not matter. Also, the sortedness of the whole signatures is not required, as long as the first threshold number of signatures are locally sorted. However, we have not found an attack exploiting this.

Another questionable behavior is in the case where there are threshold valid signatures in total, but some of them at the beginning are invalid. Currently, checkSignatures fails in this case. A potential issue for this behavior is that a bad owner intentionally sends an invalid signature to veto the transaction. He can always veto if his address is the first (the smallest) among the owners. On the other hand, a good owner is hard to veto some bad transaction if his address is the last (the lartest) among the owners. Is this intended?

No explicit check for the case `2 <= v <= 26`

According to the signature encoding scheme, a signature with 2 <= v <= 26 is not valid, but the code does not have an explicit check for the case, relying on ecrecover to implicitly reject the case. It may be considered to have the explicit check for the robustness, if the additional gas cost is affordable, since we have not verified the underlying C implementation of secp256k1, and there might exist unknown zero-day vulnerabilities (especially for the unusual cases).

Exceptional behavior of `isValidSignature`

For the following code:

if (!ISignatureValidator(currentOwner).isValidSignature(data, contractSignature)) {

It is not clear what will happen if the external isValidSignature function does not return at all. Similarly, what if the currentOwner contract does not implement isValidSignature function at all, but have the default fallback function? (Note that the default fallback function cannot return anything.)

It depends on the bytecode behavior. If the bytecode does not reset the return memory address, it may reuse the garbage value previously returned by the lastOwner.isValidSignature, and it is exploitable.

Even if the current Solidity compiler generates the robust bytecode, a future version may not. Thus, it is required to re-verify the bytecode once the compiler version is updated.

In the current bytecode, it checks the existence of the return value using returndatasize: https://github.com/runtimeverification/verified-smart-contracts/blob/master/gnosis/generated/GnosisSafe.evm#L9704-L9721

Memory copy

In checkSignatures, the argument signatures is first loaded into the local memory from the call data (not into the stack). Then, when it calls isValidSignature, it performs the memory-to-memory copy to prepare for the contractSignature argument (part of the signatures bytes). Now, it is required in the bytecode that these two memory regions do not overlap. Otherwise the memory-to-memory copy is not sound.

It also depends on the compiler version.

`signatures` size limit

Considering the current max block gas limit (~8M) and the gas cost for the local memory usage (i.e., n^2/512 + 3n for n bytes), the size of signatures must be (much) less than 2^16 (i.e., 64KB).

Specification

We first define the-first-invalid-signature-index as follows:

A1: for all i < the-first-invalid-signature-index, signatures[i] is valid.
A2: signatures[the-first-invalid-signature-index] is NOT valid.

Now we formulate the behavior of checkSignatures as follows:

T1: checkSignatures returns true if the-first-invalid-signature-index >= threshold.
T2: otherwise, returns false.

To prove that, we need the loop invariant as follows: For some i such that 0 <= i < threshold and i <= the-first-invalid-signature-index:

L1: if i < threshold <= the-first-invalid-signature-index, then return true.
L1: else (i.e., if i <= the-first-invalid-signature-index < threshold), then return false.

====

Proof sketch.

The top level specification:

T1: by L1 with i = 0.
T2: by L2 with i = 0.

The loop invariant:

L1: By A1, signatures[i] is valid. Then by M1, it goes back to the loop head, and we have two cases:
- Case 1: i + 1 = threshold: it jumps out of the loop, and return true.
- Case 2: i + 1 < threshold: by circular reasoning with L1.
L2:
- Case 1: i = the-first-invalid-signature-index: By A2, signatures[i] is NOT valid. Then, by M2, we conclude.
- Case 2: i < the-first-invalid-signature-index: By A1, signatures[i] is valid. Then, by M1, it goes to the loop head, and by the circular reasoning with L2, we conclude (since we know that i + 1 <= the-first-invalid-signature-index < threshold).

We need to prove the following claims, but it can be done with looking at the loop body only.

M1: if signatures[i] is valid, it continues to the next iteration (i.e., goes back to the loop head).
M2: if signatures[i] is NOT valid, it returns false.

[checkSignatures]
pc: PC_FUN_BEGIN => PC_FUN_END
wordStack: CONSUME_HASH : DATA_HASH : WS => RESULT : WS             ; some arguments on stack (?)
localMem: MEM:IMap => storeRange(MEM, HAVOC_START, HAVOC_WIDTH, _)  ; localMem is updated but we don't care (?)
proxy_storage: STORAGE:IMap                                         ; storage is not updated (?)
+requires:                                                          ; some arguments on memory (?)
    andBool selectRange(MEM, DATA_LOC, DATA_WIDTH) ==K DATA_BUF
    andBool selectRange(MEM, SIGS_LOC, SIGS_WIDTH) ==K SIGS_BUF
    andBool select(STORAGE, #hashedLocation({COMPILER}, {THRESHOLD}, .IntList)) ==Int THRESHOLD

[checkSignatures-success]
+requires:
    andBool #fii(SIGS_BUF, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER) >=Int THRESHOLD
+ensures:
    andBool RESULT ==Int 1

[checkSignatures-failure]
+requires:
    andBool #fii(SIGS_BUF, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER) <Int THRESHOLD
+ensures:
    andBool RESULT ==Int 0


[checkSignatures-loop]
pc: PC_LOOP_HEAD => PC_FUN_END  ; no meaningful stuff after the loop
+requires:
    andBool 0 <=Int I andBool I <Int THRESHOLD
    andBool I <=Int #fii(SIGS_BUF, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)

[checkSignatures-loop-success]
+requires:
    andBool #fii(SIGS_BUF, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER) >=Int THRESHOLD
+ensures:
    andBool RESULT ==Int 1

[checkSignatures-loop-failure]
+requires:
    andBool #fii(SIGS_BUF, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER) <Int THRESHOLD
+ensures:
    andBool RESULT ==Int 0


[checkSignatures-loop-body]
+requires:
    andBool CURRENT_OWNER ==Int #signer(SIGS_BUF, I)

[checkSignatures-loop-body-success]
pc: PC_LOOP_HEAD
wordStack: (LAST_OWNER => CURRENT_OWNER) : (I => I +Int 1) : WS
+requires:
    andBool #isValid(SIGS_BUF, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)

[checkSignatures-loop-body-failure]
pc: PC_LOOP_HEAD => PC_FUN_END
wordStack: LAST_OWNER : I : WS
+requires:
    andBool notBool #isValid(SIGS_BUF, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)
+ensures:
    andBool RESULT ==Int 0


; syntax Int  ::= #fii        ( WordStack , Int , WordStack , IMap , Int ) [function, smtlib(fii)] // first-invalid-signature-index
; syntax Bool ::= #isValid    ( WordStack , Int , WordStack , IMap , Int ) [function, smtlib(isValid)]
; syntax Bool ::= #isValidSig ( WordStack , Int , WordStack , IMap , Int ) [function, smtlib(isValidSig)]
; syntax Bool ::= #isValidSignature ( Int , WordStack , WordStack ) [function, smtlib(isValidSignature)] // ISignatureValidator(currentOwner).isValidSignature(data, contractSignature)
; syntax Int  ::= #signer ( WordStack , Int , WordStack ) [function]
; syntax Int  ::= #sigR   ( WordStack , Int ) [function]
; syntax Int  ::= #sigS   ( WordStack , Int ) [function]
; syntax Int  ::= #sigV   ( WordStack , Int ) [function]
;
; rule 0 <=Int #fii(_,_,_,_,_)          => true
; rule         #fii(_,_,_,_,_) <Int ??? => true
;
; // axiomatization of #fii
;
; rule #isValid(SIGS, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER) => true  requires I  <Int #fii(SIGS, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)
; rule #isValid(SIGS, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER) => false requires I ==Int #fii(SIGS, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)
;
; // axiomatization of #isValid
;
; rule #isValid   (SIGS, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)
;   => #isValidSig(SIGS, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)
;      andBool #signer(SIGS, I, DATA_HASH) >Int #signer(SIGS, I -Int 1, DATA_HASH)
;      andBool select(STORAGE, #hashedLocation({COMPILER}, {OWNERS}, #signer(SIGS, I, DATA_HASH))) =/=Int 0
;
; rule #signer(_, I, _) => 0 requires I <Int 0  // address lastOwner = address(0);
;
; // axiomatization of #isValidSig for each signature type
;
; rule #isValidSig(SIGS, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)
;   => #isValidSignature(#signer(SIGS, I, DATA_HASH),                                                     // currentOwner
;                        DATA_BUF,                                                                        // data
;                        #bufSeg(SIGS, #sigS(SIGS,I) +Int 32, #asWord(#bufSeg(SIGS, #sigS(SIGS,I), 32)))) // contractSignature
;   requires #sigV(SIGS, I) ==Int 0
;
; rule #isValidSig(SIGS, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)
;   => MSG_SENDER ==Int #sigR(SIGS, I)
;      orBool select(STORAGE, #hashedLocation({COMPILER}, {APPROVED_HASHES}, #sigR(SIGS, I) DATA_HASH)) =/=Int 0
;   requires #sigV(SIGS, I) ==Int 1
;
; /* in case the above doesn't work
; rule #isValidSig(SIGS, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER) => true
;   requires #sigV(SIGS, I) ==Int 1 andBool MSG_SENDER ==Int #sigR(SIGS, I)
;
; rule #isValidSig(SIGS, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)
;   => select(STORAGE, #hashedLocation({COMPILER}, {APPROVED_HASHES}, #sigR(SIGS, I) DATA_HASH)) =/=Int 0
;   requires #sigV(SIGS, I) ==Int 1 andBool MSG_SENDER =/=Int #sigR(SIGS, I)
; */
;
; rule #isValidSig(SIGS, I, DATA_HASH, DATA_BUF, STORAGE, MSG_SENDER)
;   => notBool #ecrecEmpty(#ecrecData(SIGS, I, DATA_HASH))
;   requires #sigV(SIGS, I) =/=Int 0
;    andBool #sigV(SIGS, I) =/=Int 1
;
; // definition of #signer
;
; rule #signer(SIGS, I, DATA_HASH) => #symEcrec(#ecrecData(SIGS, I, DATA_HASH)) requires I >=Int 0 andBool   #sigV(SIGS, I) =/=Int 0 andBool #sigV(SIGS, I) =/=Int 1   andBool notBool #ecrecEmpty(#ecrecData(SIGS, I, DATA_HASH))
; rule #signer(SIGS, I, DATA_HASH) => 0                                         requires I >=Int 0 andBool   #sigV(SIGS, I) =/=Int 0 andBool #sigV(SIGS, I) =/=Int 1   andBool         #ecrecEmpty(#ecrecData(SIGS, I, DATA_HASH))
; rule #signer(SIGS, I, DATA_HASH) => #sigR(SIGS, I)                            requires I >=Int 0 andBool ( #sigV(SIGS, I)  ==Int 0  orBool #sigV(SIGS, I)  ==Int 1 )
;
; syntax WordStack ::= #ecrecData ( WordStack , Int , WordStack ) [function]
; rule #ecrecData(SIGS, I, DATA_HASH) => #encodeArgs(#bytes32(DATA_HASH), #uint8(#sigV(SIGS,I)), #bytes32(#sigR(SIGS,I)), #bytes32(#sigS(SIGS,I)))
;
; // definition of #sigR, #sigS, #sigV
;
; rule #sigR(SIGS, I) => #asWord(#bufSeg(SIGS, 65 *Int I        , 32))
; rule #sigS(SIGS, I) => #asWord(#bufSeg(SIGS, 65 *Int I +Int 32, 32))
; rule #sigV(SIGS, I) =>         #bufElm(SIGS, 65 *Int I +Int 64)

OwnerManager

`addOwnerWithThreshold`

Although it is very unlikely, but if ownerCount is corrupted (possibly due to the hash collision), ownerCount++ may have the overflow, resulting in ownerCount being zero, provided that threshold == _threshold. In the case of threshold != _threshold, however, if ownerCount++ has the overflow, changeThreshold will always revert since the following two requirements cannot be satisfied at the same time, where ownerCount is zero:

        // Validate that threshold is smaller than number of owners.
        require(_threshold <= ownerCount, "Threshold cannot exceed owner count");
        // There has to be at least one Safe owner.
        require(_threshold >= 1, "Threshold needs to be greater than 0");

Gas consumption

`[checkSignatures-loop-body-success-v1-owner]`

gas: #gas(INITGAS, NONMEMGAS, MEMGAS)
  => #gas(INITGAS, NONMEMGAS +Int 1061, MEMGAS +Int (Cmem(BYZANTIUM, FINAL_MEM_USAGE) -Int Cmem(BYZANTIUM, MU)))
; FINAL_MEM_USAGE ==Int #memoryUsageUpdate(MU, SIGS_LOC +Int (65 *Int I +Int 65), 32)

`[checkSignatures-loop-body-success-v1-not-owner]`

gas: #gas(INITGAS, NONMEMGAS, MEMGAS)
  => #gas(INITGAS, NONMEMGAS +Int 6622, MEMGAS +Int (Cmem(BYZANTIUM, FINAL_MEM_USAGE) -Int Cmem(BYZANTIUM, MU)))
; FINAL_MEM_USAGE ==Int #memoryUsageUpdate(MU, SIGS_LOC +Int (65 *Int I +Int 65), 32)

`[checkSignatures-loop-body-success-v_else]`

gas: #gas(INITGAS, NONMEMGAS, MEMGAS)
  => #gas(INITGAS, NONMEMGAS +Int Cgascap(..) +Int 1334 -Int Cgascap(..) +Int 3496, MEMGAS +Int (Cmem(BYZANTIUM, FINAL_MEM_USAGE) -Int Cmem(BYZANTIUM, MU)))
; == #gas(INITGAS, NONMEMGAS +Int 4830, MEMGAS +Int (Cmem(BYZANTIUM, FINAL_MEM_USAGE) -Int Cmem(BYZANTIUM, MU)))
; FINAL_MEM_USAGE ==Int #memoryUsageUpdate(MU, NEXT_LOC +Int 128 , 32)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Gnosis

`execTransaction`

zero and precompiled contract addresses

Minor Related Note:

`checkSignatures`

Local validity check

No explicit check for the case `2 <= v <= 26`

Exceptional behavior of `isValidSignature`

Memory copy

`signatures` size limit

Specification

OwnerManager

`addOwnerWithThreshold`

Gas consumption

`[checkSignatures-loop-body-success-v1-owner]`

`[checkSignatures-loop-body-success-v1-not-owner]`

`[checkSignatures-loop-body-success-v_else]`

Clone this wiki locally

Gnosis

execTransaction

zero and precompiled contract addresses

Minor Related Note:

checkSignatures

Local validity check

No explicit check for the case 2 <= v <= 26

Exceptional behavior of isValidSignature

Memory copy

signatures size limit

Specification

OwnerManager

addOwnerWithThreshold

Gas consumption

[checkSignatures-loop-body-success-v1-owner]

[checkSignatures-loop-body-success-v1-not-owner]

[checkSignatures-loop-body-success-v_else]

Clone this wiki locally

`execTransaction`

`checkSignatures`

No explicit check for the case `2 <= v <= 26`

Exceptional behavior of `isValidSignature`

`signatures` size limit

`addOwnerWithThreshold`

`[checkSignatures-loop-body-success-v1-owner]`

`[checkSignatures-loop-body-success-v1-not-owner]`

`[checkSignatures-loop-body-success-v_else]`