Skip to content

Gnosis

Jump to bottom
Daejun Park edited this page Jan 7, 2019 · 27 revisions

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");
Clone this wiki locally