GnosisSafe Formal Verification

Goal and Scope

The goal of the formal verification engagement is to formally verify security-critical properties of the GnosisSafe smart contract. We formally specified the security properties and verified them against the GnosisSafe smart contract bytecode using the KEVM verifier. The code is from commit ID 427d6f7e779431333c54bcb4d4cde31e4d57ce96 of the gnosis/safe-contracts Github repository.

The scope of the formal verification is the GnosisSafe contract without enabling any add-on modules. Specifically, this includes the following functions:

executeTransaction of GnosisSafe.sol:
- only for the case of operation == CALL and payment in Ether.
- including encodeTransactionData, checkSignatures, and handlePayment functions.
changeMasterCopy of MasterCopy.sol
addOwner, removeOwner, and swapOwner of OwnerManager.sol
enableModule, and disableModule of ModuleManager.sol
execTransactionFromModule of ModuleManager.sol
- only for the case that modules is empty.

The formal verification is limited in scope within the boundary of the Solidity contract only.

Assessment

The signatureSplit function does not check the index is within the bound of the signatures sequence. Although no out-of-bound index is passed to the function throughout the current GnosisSafe contract, it is recommended to either add the index bound check or mention the implicit requirement in the document to prevent any future implementation from violating this condition.

all the address arguments are assumed to be within the range of addresses, i.e., its first 96 (= 256 - 160) bits are zero. otherwise, the fist 96 bits are simply ignored, without any exception. thus, any client of this function should check the validity of addresses before passing them to the functions.

issues:

no validity check for the signature encoding

when v is 0 or 1, the owner r should be within the range of address: otherwise, the upper bits are truncated
when v is 0,
- the offset s should be within the bound, i.e., s + 32 <= signatures.length: otherwise, it will read some garbage value from the memory
- the dynamic signature data pointed by s should be well-formed:
  - the first 4 bytes denote the length of the dynamic data, i.e., dynamic-data-length := mload(signatures + s + 32): otherwise, it may try to read a large memory chunk
  - the signatures buffer should be large enough to hold the dynamic data, i.e., signatures.length >= s + 32 + dynamic-data-length: otherwise, it will read some garbage value from the memory
- (optional) each dynamic data should not be pointed by different signatures: otherwise, the same dynamic data will be used to check the validity of different signatures
- (optional) different dynamic data should not be overlapped

screening for isValidSignature of each owner. it may be considered to scan the isValidSignature function whenever adding a new owner (either in the contract or the client side), to ensure that it has no dangerous opcode.

Formal Specification

Our formal specification of the security and functional correctness properties of GnosisSafe can be found at: https://github.com/runtimeverification/verified-smart-contracts/blob/master/gnosis/gnosis-spec.ini

Here we explain the formal specification for each function.

`signatureSplit`

signatureSplit is an internal function that takes a sequence of signatures and an index, and returns the indexed signature as a tuple of its v, r, and s fields.

We formally verified that the function admits the following behaviors.

Input/Output Behaviors

The function takes two inputs, signatures and pos, where signatures is passed through the memory while pos is through the stack.

The input stack is given as follows:

POS : SIGS_LOC : RETURN_LOC : WS

where POS is the value of pos, and SIGS_LOC is the starting location of the memory that stores the signatures data.

(NOTE: RETURN_LOC is the return address (PC value), and WS is the caller's stack frame, which are not relevant for this function's behavior.)

The memory stores the signatures data starting at the location SIGS_LOC, where it first stores the size of the data SIGS_LEN, followed by the actual data buffer SIGNATURES, as illustrated below:

|<-  32  ->|<-    SIGS_LEN    ->|
+----------+--------------------+
| SIGS_LEN |     SIGNATURES     |
+----------+--------------------+
^          ^                    ^
|          |                    |
SIGS_LOC   SIGS_LOC + 32        SIGS_LOC + 32 + SIGS_LEN

The function's return value is a tuple of (v, r, s), which is pushed into the stack, as in the following output stack:

RETURN_LOC : S : R : V : WS

where

S: 32 bytes from the offset 65 * POS + 32 of SIGNATURES
R: 32 bytes from the offset 65 * POS of SIGNATURES
V: 1 byte at the offset 65 * POS + 64 of SIGNATURES

Other Behaviors

The function cannot be directly called from outside, since it is an internal function. An external transaction to this function will silently terminates with no effect (and no exception).

The function does not update the storage, as it is specified as a pure function.

Pre-condition

We assume that:

the size of stack is small enough to avoid the stack overflow
the maximum memory location accessed, i.e., SIGS_LOC + 32 + (65 * POS + 65), is small enough to avoid the integer overflow

The above assumptions are practically reasonable. If they are not satisfied, the function will throw.

Also, we had to assume the following condition that the function implicitly requires:

no index out of bound, i.e., (POS + 1) * 65 <= SIGS_LEN

Currently, this requirement is satisfied for all use cases of this function.

`encodeTransactionData`

encodeTransactionData is a public function that calculates the hash value of the given transaction data.

We formally verified that the function admits the following behaviors.

Input/Output Behaviors

Although it is a public function, i.e., it can be called internally or externally, we consider only the internal use case, where the inputs are passed through the stack and the memory.

The input stack consists of the following:

NONCE : REFUND_RECEIVER : GAS_TOKEN : GAS_PRICE : DATA_GAS : SAFE_TX_GAS : OPERATION : DATA_LOC : VALUE : TO : RETURN_LOC : WS

where the first ten elements are the function arguments in the reverse order, while DATA_LEN_LOC is a memory pointer to the actual data buffer. Note that OPERATION is encoded as unit8.

The memory stores the data buffer starting at the location DATA_LOC, where it first stores the size of the buffer, followed by the actual buffer bytes, as illustrated below:

|<-  32  ->|<-    DATA_LEN    ->|
+----------+--------------------+
| DATA_LEN |      DATA_BUF      |
+----------+--------------------+
^          ^                    ^
|          |                    |
DATA_LOC   DATA_LOC + 32        DATA_LOC + 32 + DATA_LEN

The output stack consists of:

RETURN_LOC : OUT_LOC : WS

The actual return value (buffer) is stored in the memory at the starting location OUT_LOC, as follows:

|<- 32 ->|<- 1 ->|<- 1 ->|<-      32      ->|<-    32    ->|
+--------+-------+-------+------------------+--------------+
|   66   |  0x19 |  0x01 | DOMAIN_SEPARATOR | SAFE_TX_HASH |
+--------+-------+-------+------------------+--------------+
^        ^               ^                  ^              ^
|        |               |                  |              |
OUT_LOC  OUT_LOC + 32    OUT_LOC + 34       OUT_LOC + 66   OUT_LOC + 98

The first 32 bytes denote the length of the buffer, and the remaining 66 bytes denote the result of abi.encodePacked(byte(0x19), byte(0x01), domainSeparator, safeTxHash). Note that the first two elements, 0x19 and 0x01, are not aligned, because of the use of abi.encodePacked instead of abi.encode.

Here, SAFE_TX_HASH is the result of abi.encode(SAFE_TX_TYPEHASH, to, value, keccak256(data), operation, safeTxGas, dataGas, gasPrice, gasToken, refundReceiver, _nonce), where each argument is 32-byte aligned with zero padding on the left.

NOTE: If this function is called externally, the return value is encoded as follows:

|<- 32 ->|<- 32 ->|<- 1 ->|<- 1 ->|<-      32      ->|<-    32    ->|<- 30 ->|
+--------+--------+-------+-------+------------------+--------------+--------+
|   32   |   66   |  0x19 |  0x01 | DOMAIN_SEPARATOR | SAFE_TX_HASH |    0   |
+--------+--------+-------+-------+------------------+--------------+--------+

Here, the prefix (the first 32 bytes) and the postfix (the last 30 bytes) are attached. The prefix is the offset to the start of the result buffer, and the postfix is the zero padding for the alignment.

The output memory is as follows:

|<-  32  ->|<-    DATA_LEN    ->|<- X ->|<-               384                 ->|<- 32 ->|<- 1 ->|<- 1 ->|<-      32      ->|<-    32    ->|
+----------+--------------------+-------+---------------------------------------+--------+-------+-------+------------------+--------------+
| DATA_LEN |      DATA_BUF      |   0   |                 ...                   |   66   |  0x19 |  0x01 | DOMAIN_SEPARATOR | SAFE_TX_HASH |
+----------+--------------------+-------+---------------------------------------+--------+-------+-------+------------------+--------------+
^          ^                    ^       ^                                       ^        ^       ^       ^                  ^              ^
|          |                    |       |                                       |                                                          |
DATA_LOC   DATA_LOC + 32        |       DATA_LOC + 32 + ceil32(DATA_LEN)        DATA_LOC + 32 + ceil32(DATA_LEN) + 384                     DATA_LOC + 32 + ceil32(DATA_LEN) + 482
                                |                                               ^
                                DATA_LOC + 32 + DATA_LEN                        |
                                                                                OUTPUT_LOC

where X = ceil32(DATA_LEN) - DATA_LEN.

The function writes to the memory starting from DATA_LOC + 32 + ceil32(DATA_LEN). The first 384 bytes are used for executing keccak256 to compute safeTxHash, i.e., 352 bytes for preparing for 11 arguments (= 32 * 11), and 32 bytes for holding the return value. The next 98 bytes are used for passing the return value, as described above.

Other Behaviors

The function does not update the storage, as it is specified as a view function.

msg.value must be zero, since the function is not payable. Otherwise, it throws.

Pre-condition

We assume that:

the call depth is small enough to avoid the call depth overflow
the size of stack is small enough to avoid the stack overflow
the maximum memory location accessed, i.e., DATA_LOC + 32 + ceil32(DATA_LEN) + 482, is small enough to avoid the integer overflow

The above assumptions are practically reasonable. If they are not satisfied, the function will throw.

We also assume that:

the to, gasToken, and refundReceiver argument values are all within the range of addresses, i.e., its first 96 (= 256 - 160) bits are zero. Otherwise, the fist 96 bits are simply ignored.
the operation is either 0, 1, or 2.
the maximum size of data is 2^32. (This is practically reasonable bound considering the current block gas limit. See the size limit discussion.)

`handlePayment`

handlePayment is a private function that pays the gas cost to the receiver in either Ether or tokens.

Here we consider only the case of payment in Ether. The token payment is out of the scope.

We formally verified that the function admits the following behaviors.

Input/Output Behaviors

The input arguments are passed through the stack:

REFUND_RECEIVER : GAS_TOKEN : GAS_PRICE : DATA_GAS : START_GAS : RETURN_LOC : WS

The function has no return value, and thus the output stack, if succeeds, is as follows:

RETURN_LOC : WS

The payment amount is:

((START_GAS - GAS_LEFT) + DATA_GAS) * GAS_PRICE

where GAS_LEFT is the result of gasleft() at line 115.

If the arithmetic overflow occurs when evaluating the above expression, the function reverts.

If no overflow occurs, receiver is set to tx.origin if refundReceiver is zero, otherwise it is set to refundReceiver. Thus receiver is non-zero.

Finally, the amount of Ether is sent to receiver. If send succeeds, then the function returns. Otherwise it reverts.

Here, we have little concern about the reentrancy, since there is no critical statement after send, and also the function is private.

Other Behaviors

The function cannot be directly called from outside, since it is a private function. An external transaction to this function will silently terminates with no effect (and no exception).

Pre-condition

We assume that:

the value of the address arguments are within the range of addresses.

`checkSignatures`

checkSignatures is an internal function that checks validity of the given signatures.

Inout/Output Behaviors

The input arguments are passed through the stack:

CONSUME_HASH : SIGS_LOC : DATA_LOC : DATA_HASH : RETURN_LOC : WS

where data and signatures are stored in the memory:

|<-  32  ->|<-    DATA_LEN    ->|     |<-  32  ->|<-    DATA_LEN    ->|
+----------+--------------------+     +----------+--------------------+
| DATA_LEN |      DATA_BUF      | ... | SIGS_LEN |      SIGS_BUF      |
+----------+--------------------+     +----------+--------------------+
^          ^                    ^     ^          ^                    ^
|          |                    |     |          |                    |
DATA_LOC   DATA_LOC + 32        |     SIGS_LOC   SIGS_LOC + 32        SIGS_LOC + 32 + SIGS_LEN
                                |
                                DATA_LOC + 32 + DATA_LEN

The function returns true if:

the number of signatures is more than equal to threshold, and
the first threshold number of signatures are valid, signed by owners, and sorted by their owner address

where a signature is valid if:

when v = 0: r's isValidSignature returns true
when v = 1: r == msg.sender or dataHash is already approved
otherwise: it is a valid ECDSA signature

Otherwise, the function returns false, unless isValidSignature throws (or reverts).

If isValidSignature throws or reverts, checkSignatures reverts, immediately terminating without returning to execTransaction.

Pre-condition

We assume that:

threshold is small enough to avoid overflow
the size of stack is small enough to avoid the stack overflow exception
the maximum memory location accessed is small enough to avoid the integer overflow exception.

Also, we made the following assumptions that are satisfied by its caller execTransaction:

the maximum size of data is 2^32. (this is practically reasonable bound considering the current block gas limit. see the size limit discussion.)
consumeHash = true
no overlap between the memory chunks of data and signatures, i.e., DATA_LOC + 32 + DATA_LEN <= SIGS_LOC

The following assumptions should be satisfied by the clients:

every signature is well-formed, which may not be satisfied, see our recommendation below.

Contract invariant:

every owner (i.e., some o such that owners[o] =/= 0) is within the range of address.

`execTransaction`

execTransaction is an external function that executes the given transaction.

Input/Output Behaviors

Since it is an external function, it starts with a fresh VM (i.e., both the stack and the memory are empty, the PC is 0, etc.)

we assume that

nonce is small enough to avoid overflow
all address argument values are within the range of address
operation is zero, since we consider only the Enum.Call case.
the size of data and signatures is small enough to avoid overflow (see the signatures size discussion)

execTransaction has the following non-trivial behaviors:

checkSignatures may revert, which immediately terminates VM, without returning to execTransaction.
execute never revert, even if the given transaction throws or reverts. the return value of the given transaction is ignored.
handlePayment may throw or revert, and in that case, execTransaction reverts (i.e., the given transaction is reverted as well).

contract invariants:

threshold is greater than or equal to 1, and small enough to avoid overflow.

when we abstract the external call, we assume that it does not change the current (i.e., proxy) storage, which allows the modular reasoning.

a conservative abstraction would be to assume that an external call may update all accounts (i.e., balance, storage, nonce, and even code!) and also create one or more new accounts, but never delete an existing account (since the SELFDESTRUCT opcode effect is applied only after the current transaction finishes.) however, this kind of crude abstraction does not necessarily provide meaningful reasoning either.

OwnerManager

contract invariant (after setup):

threshold >= 1
ownerCount >= threshold
ownerCount is small enough to avoid overflow

circular linked list invariant (after setup):

owners denotes a (non-empty) list without duplicates (o_0, o_1, ... o_N) where N >= 0, o_i is non-zero, o_0 = 1, and all o_i's are distinct, iff: owners[o_i] = o_{i+1 mod N+1} for 0 <= i <= N and owners[x] = 0 for any x \not\in the list (o_0, ..., o_N)

addOwnerWithThreshold is a public authorized function that takes as input a new owner and a new threshold value, and adds the new owner and updates threshold.

it can be called by only the proxy account. otherwise, it reverts.

it also reverts if one of the following is not satisfied:

the argument owner is not 0 nor 1 (sentinel).
the argument owner is not an owner (before calling this function).
the argument _threshold should be within the range of [1, ownerCount + 1], inclusive.

it preserves the circular linked list invariant:

the post-state owners' denotes (o_0, owner, o_1, ..., o_N) if the pre-state owners denotes (o_0, o_1, ... o_N).

informative: the check require(owner != SENTINEL_OWNERS) is logically redundant in the presence of require(owners[owner] == address(0)), but it can save the gas cost when owner = SENTINEL_OWNERS.

removeOwner is a public authorized function that removes the given owner and updates threshold.

it can be called by only the proxy account. otherwise, it reverts.

it also reverts if one of the following is not satisfied:

the current threshold should be less than the current ownerCount
owner is not 0 nor 1
owners[prevOwner] = owner

this pre-condition implies N > 0, and thus prevOwner =/= owner.

it preserves the circular linked list invariant:

the post-state owners' denotes (..., prevOwner, owner, o_i, ...) if the pre-state owners denotes (..., prevOwner, o_i, ...).

recommendation: it may be considered to check that _threshold <= threshold

swapOwner is a public authorized function that replaces oldOwner with newOwner.

it can be called by only the proxy account. otherwise, it reverts.

it also reverts if one of the following is not satisfied:

oldOwner is not 0 nor 1
newOwner is not 0 nor 1
owners[newOwner] = 0
owners[prevOwner] = oldOwner

this pre-condition implies N > 0, and all prevOwner, oldOwner, and newOwner are distinct.

(..., prevOwner, oldOwner, ...) => (..., prevOwner, newOwner, ...)

informative: the check require(newOwner != SENTINEL_OWNERS) is logically redundant in the presence of require(owners[newOwner] == address(0)), but it can save the gas cost when newOwner = SENTINEL_OWNERS.

transaction reordering issue.

this function allows to update threshold, which introduces an usability issue similar to the ERC20 approve function issue.

the common usage scenario of this function is to add a new owner with increasing the threshold value (or keeping the value as is). it is very unlikely the case of decreasing the threshold value while adding a new owner. if there still exists such a use case, one can split the task into two transactions: adding a new owner, and decreasing threshold. that is, we have not found a reason for such a task, if any, to be executed atomically.

exploit scenario:

suppose there are five owners with threshold of three. suppose alice proposes a transaction of addOwnerWithThreshold(o1,4) and immediately bob proposes a transaction of addOwnerWithThreshold(o2,5). if the bob's transaction is approved before the alice's transaction, the final threshold will be 4, while it should be 5.

recommendation:

reject addOwnerWithThreshold if it tries to decrease threshold
have two more functions: increaseThreshold and decreaseThreshold

changeMasterCopy misses the contract account existence check for the new master copy address. if the non-contract address is set to the master copy, then the proxy fall back function will silently returns.

recommend: implement the existence check, e.g., using EXTCODESIZE.

backup:

for any active address x,

both x and owners[x] are either an owner or the sentinel (0x1), iff owners[x] =/= 0.
- i.e., both x and owners[x] are not an owner nor the sentinel, iff owners[x] = 0.
x is not an owner, if x is either 0 and 1

x is an owner or the sentinel, iff owners[x] =/= 0 and there exists y such that owners[y] = x

we assume that data is well-formed. it is a reasonable assumption from the fact that the solidity generated bytecode has the proper checks.

in general, when a bytes-type argument is provided, the following checks are performed:

CALLDATASIZE >= 4 ? // checks if the function signature is provided
CALLDATASIZE >= 4 + 32 * NUM_OF_ARGS // checks if the headers of all parameters are provided
.... // load static type args and checks range
startLOC := CALLDATALOAD(4 + 32 * IDX)
startLOC <= 2^32 ?
startLOC + 4 + 32 <= CALLDATASIZE ? // checks if the length is provided
dataLen := CALLDATALOAD(startLoc + 4)
startLoc + 4 + 32 + dataLen <= CALLDATASIZE ? // checks if the actual data is provided
dataLen <= 2^32 ?

Contract-wide Assumption

We first assume that there are at least five accounts deployed on-chain: the master copy account, the proxy account, the transaction sender (tx.origin) account, the transaction target (to) account, and the payment receiver (refundReceiver) account. Note that the master copy, the proxy, and the transaction sender accounts must be distinct, while the transaction target and the payment receiver accounts may be the same with others. We do not assume anything about their balances except that their values are within the range of uint256 (i.e., 0 to 2^256 - 1, inclusive).

We also assume that the call depth at the point of executing execTransaction is less than 1023, since the nested depth of external contract calls is at least 1.

Statistics

Number of formal specifications: 64
Total LOC of the specifications: >2,000
Verification time: 29,103s (~ 8h) @ Intel i7-4960X CPU 3.60GHz
Average number of (semantics) steps: 5,050 (max: 11,635)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

GnosisSafe Formal Verification

Goal and Scope

Assessment

Formal Specification

`signatureSplit`

Input/Output Behaviors

Other Behaviors

Pre-condition

`encodeTransactionData`

Input/Output Behaviors

Other Behaviors

Pre-condition

`handlePayment`

Input/Output Behaviors

Other Behaviors

Pre-condition

`checkSignatures`

Inout/Output Behaviors

Pre-condition

`execTransaction`

Input/Output Behaviors

Contract-wide Assumption

Statistics

Clone this wiki locally