Delving Into a Common FA2 Contract With Factori

Blockchain Tezos Michelson Factori dApps Static Analysis Safety Security
Published on 2023/04/19
Delving Into a Common FA2 Contract With Factori

A few days ago, we introduced Factori's new static analysis capabilities and promised a more detailed real world smart contract analysis. We showcase in this article how factori analyze can be used to unveil the permissions / failing conditions of the most deployed FA2/NFT contract on Tezos blockchain. Of course, we don't have the contract's high-level source code. We picked its address on the blockchain. In such circumstances, it can be quite a hassle to get information on how the contract works. You can re-run this analysis in the following way:

$ factori analyze kt1 YOUR-KT1

General information about the storage

The analysis of the contract has found several issues/warnings that may cause problems in the future.

Found unbounded data structures with non-lazy deserialization in the storage
  - map is used once in the storage,
    * token_info field is a map in the storage

There is a CALL_CONTRACT in this contract, check for reentrancy

The following fields of the storage may be unused:
  var_19 -> (big_map%total_supply(nat) (nat))

The analysis reveals an unbounded data structure with non-lazy deserialization in the storage, potentially causing performance issues and out-of-gas errors. This correspond to the token_info field, which is a map in the storage.

The next one indicates that there is a CALL_CONTRACT in the contract, which may lead to potential reentrancy attacks. Ensuring proper protection against these attacks can be crucial.

Finally, it seems that the total_supply storage field is unused. It indicates a potential storage inefficiency.

Without having the specification or the high level code, we can't say at this moment if this map could be problematic. A manual review or the specification would have allowed us to eliminate all lingering doubt.

Now we can look at the output of Factori on the entry points. In the next section, we will look at the set_administrator and balance_of entrypoints.

Permission Analysis

Let's take a closer look at the output of our permissions analysis on the set_administrator entrypoint.

# Entrypoint: set_administrator
Parameter: (address%set_administrator)

Fail with "FA2_NOT_ADMIN" if ((SENDER <> storage.administrator))

In this case, it is quite normal that the failure case occurs when the sender is not the administrator (defined in the storage, storage.administrator). Only the administrator of the contract can change the administrator address stored in the contract's storage.

set_metadata and set_pause have similar outputs. Only the administrator can call those entrypoints as well.

Unreachable Code Detection

If we look at the result of the analysis on the balance_of entrypoint, in addition to permissions, another interesting piece of information is displayed. Let's take a closer look.

# Entrypoint: balance_of
Parameter: (pair%balance_of(list%requests(pair(address%owner) (nat%token_id))) (contract%callback(list(pair(pair%request(address%owner) (nat%token_id)) (nat%balance)))))

Fail with "FA2_PAUSED" if (storage.paused)
Else
Fail with "FA2_TOKEN_UNDEFINED" if (not ((nat%token_id) in storage.token_metadata))
Else
Fail with "425" if ((GET ((nat%token_id), (address%owner), storage.ledger) is None) /\ (MEM ((nat%token_id), (address%owner), storage.ledger)))

When the entrypoint balance_of of the contract is called, the analysis concludes that there are three possible error messages that can be returned if certain conditions are met.

The analysis highlights three error messages: FA2_PAUSED occurs when the contract's 'paused' flag is set to true; FA2_TOKEN_UNDEFINED appears when the specified token ID isn't defined in the metadata.

The third and last error 425 is very interesting because it is unreachable due to a logical contradiction between the MEM and GET instructions, making the condition unsatisfiable. Indeed, translated into high level code, this is equivalent to:

if Big_map.mem token_id owner storage.ledger then (* Result of `Big_map.mem` is true *)
  match Big_map.find_opt token_id owner storage.ledger with
    | None -> (* Unreachable code since the `Big_map.mem` returns true *)
       Tezos.failwith 425
    | Some _ ->
       DO_SOMETHING
else (* Result of `Big_map.mem` is false *)
  DO_SOMETHING_ELSE

We can easily see that in the case where Big_map.mem returns true, then the None case of Big_map.find_opt can never happen. It could be a compilation issue from a high-level language to Michelson.

Conclusion

From this smart contract pulled from the blockchain, we've gained significant insights utilizing the factori analyze function. Keep in mind, however, that it may not be effective in every situation or with every contract, partly due to the halting problem. Additionally, it's crucial to conduct thorough research and not depend solely on the generated formulas. Nevertheless, this tool can serve as a valuable diagnostic instrument for examining smart contracts.

Factori can also be employed to troubleshoot software issues. In the following Stackexchange post, a user encountered difficulties when their contract call repeatedly failed. By conducting an automatic analysis, it becomes apparent that the error resulting in the contract's failure stems from the user's lack of authorization to execute the transfer.

And once again, please let us know if you enjoy this new feature! Also remember that Functori does meticulous smart contract audits based on years of experience in smart contract development and review, Tezos core development, by our engineers with PhDs in formal methods.

Appendix

Full output of the permission and storage analysis on the FA2 smart contract

Found unbounded data structure with non-lazy deserialization in the storage
map is used once in the storage
token_info field is a map in the storage
There is a CALL_CONTRACT in this contract, check for reentrancy
The following fields of the storage may be unused:
var_19 -> (big_map%total_supply(nat) (nat))


Result of permission analysis

# Entrypoint: balance_of
Parameter: (pair%balance_of(list%requests(pair(address%owner) (nat%token_id))) (contract%callback(list(pair(pair%request(address%owner) (nat%token_id)) (nat%balance)))))

  Case Fail with "FA2_PAUSED" if (storage.paused)
  Else Fail with "FA2_TOKEN_UNDEFINED" if (not ((nat%token_id) in storage.token_metadata))
  Else Fail with 425 if ((GET ((nat%token_id), (address%owner), storage.ledger) is None) AND (MEM ((nat%token_id), (address%owner), storage.ledger)))

# Entrypoint: mint
Parameter: (pair%mint(pair(address%address) (nat%amount)) (pair(map%metadata(string) (bytes)) (nat%token_id)))

  Case Fail with "FA2_NOT_ADMIN" if ((SENDER <> storage.administrator))
  Else Fail with 535 if ((GET (param.mint.token_id, param.mint.address, storage.ledger) is None) AND (MEM (param.mint.token_id, param.mint.address, storage.ledger)))
  Else Fail with "Token-IDs should be consecutive" if (((storage.all_tokens <> param.mint.token_id)) AND ((param.mint.token_id >= storage.all_tokens)) AND ((not (MEM (param.mint.token_id, param.mint.address, storage.ledger))) OR ((MEM (param.mint.token_id, param.mint.address, storage.ledger)) AND (GET (param.mint.token_id, param.mint.address, storage.ledger) is Some))))

# Entrypoint: set_administrator
Parameter: (address%set_administrator)

  Case Fail with "FA2_NOT_ADMIN" if ((SENDER <> storage.administrator))

# Entrypoint: set_metadata
Parameter: (pair%set_metadata(string%k) (bytes%v))

  Case Fail with "FA2_NOT_ADMIN" if ((SENDER <> storage.administrator))

# Entrypoint: set_pause
Parameter: (bool%set_pause)

  Case Fail with "FA2_NOT_ADMIN" if ((SENDER <> storage.administrator))

# Entrypoint: transfer
Parameter: (list%transfer(pair(address%from_) (list%txs(pair(address%to_) (pair(nat%token_id) (nat%amount))))))

  Case Fail with "FA2_PAUSED" if (storage.paused)
  Else Fail with "FA2_NOT_OPERATOR" if (not (var_1))

   Where var_1 := if (var_2) then (True)
                  else MEM ((nat%token_id), SENDER, (address%from_), operators)

         var_2 := if ((SENDER = (address%administrator))) then (True)
                  else ((address%from_) = SENDER)
  Else Fail with "FA2_TOKEN_UNDEFINED" if (not ((nat%token_id) in token_metadata))
  Else Fail with 404 if ((GET ((nat%token_id), (address%from_), ledger) is None) AND ((0 < (nat%amount))))
  Else Fail with "FA2_INSUFFICIENT_BALANCE" if (((ledger[((address%from_),(nat%token_id))] < (nat%amount))) AND (GET ((nat%token_id), (address%from_), ledger) is Some) AND ((0 < (nat%amount))))
  Else Fail with 407 if false
  Else Fail with 408 if false
  Else Fail with 407 if ((ISNAT ((ledger[((address%from_),(nat%token_id))] - (nat%amount))) is None) AND ((ledger[((address%from_),(nat%token_id))] >= (nat%amount))) AND (GET ((nat%token_id), (address%from_), ledger) is Some) AND ((0 < (nat%amount))))
  Else Fail with 410 if ((GET ((nat%token_id), (address%to_), UPDATE ((nat%token_id), (address%from_), [GET_OPT] (ISNAT ((ledger[((address%from_),(nat%token_id))] - (nat%amount)))), ledger)) is None) AND (MEM ((nat%token_id), (address%to_), UPDATE ((nat%token_id), (address%from_), [GET_OPT] (ISNAT ((ledger[((address%from_),(nat%token_id))] - (nat%amount)))), ledger))) AND (ISNAT ((ledger[((address%from_),(nat%token_id))] - (nat%amount))) is Some) AND ((ledger[((address%from_),(nat%token_id))] >= (nat%amount))) AND (GET ((nat%token_id), (address%from_), ledger) is Some) AND ((0 < (nat%amount))))

# Entrypoint: update_operators
Parameter: (list%update_operators(or_(pair%add_operator(address%owner) (pair(address%operator) (nat%token_id))) (pair%remove_operator(address%owner) (pair(address%operator) (nat%token_id)))))

  Case Fail with "FA2_NOT_ADMIN_OR_OPERATOR" if ((not (var_3)) AND ((or_(pair%add_operator(address%owner) (pair(address%operator) (nat%token_id))) (pair%remove_operator(address%owner) (pair(address%operator) (nat%token_id)))) is Left))

   Where var_3 := if (((SENDER = (address%owner))) AND ((or_(pair%add_operator(address%owner) (pair(address%operator) (nat%token_id))) (pair%remove_operator(address%owner) (pair(address%operator) (nat%token_id)))) is Left)) then (True)
                  else if (((SENDER <> (address%owner))) AND ((or_(pair%add_operator(address%owner) (pair(address%operator) (nat%token_id))) (pair%remove_operator(address%owner) (pair(address%operator) (nat%token_id)))) is Left)) then (SENDER = (address%administrator))
  Else Fail with "FA2_NOT_ADMIN_OR_OPERATOR" if ((not (var_4)) AND ((or_(pair%add_operator(address%owner) (pair(address%operator) (nat%token_id))) (pair%remove_operator(address%owner) (pair(address%operator) (nat%token_id)))) is Right))

   Where var_4 := if (((SENDER = (address%owner))) AND ((or_(pair%add_operator(address%owner) (pair(address%operator) (nat%token_id))) (pair%remove_operator(address%owner) (pair(address%operator) (nat%token_id)))) is Right)) then (True)
                  else if (((SENDER <> (address%owner))) AND ((or_(pair%add_operator(address%owner) (pair(address%operator) (nat%token_id))) (pair%remove_operator(address%owner) (pair(address%operator) (nat%token_id)))) is Right)) then (SENDER = (address%administrator))
|