Where can one locate a formally verified ERC20/ERC721 solidity code/template that adheres to security design patterns such as check effects interaction patterns?


Here is the relevant code in the 0xcert reference implementation:

 * @dev Actually perform the safeTransferFrom.
 * @param _from The current owner of the NFT.
 * @param _to The new owner.
 * @param _tokenId The NFT to transfer.
 * @param _data Additional data with no specified format, sent in call to `_to`.
function _safeTransferFrom(
  address _from,
  address _to,
  uint256 _tokenId,
  bytes _data
  address tokenOwner = idToOwner[_tokenId];
  require(tokenOwner == _from);
  require(_to != address(0));
    _transfer(_to, _tokenId);
    if (_to.isContract()) {
    bytes4 retval = ERC721TokenReceiver(_to).onERC721Received(msg.sender, _from, _tokenId, _data);
    require(retval == MAGIC_ON_ERC721_RECEIVED);

Source: https://github.com/0xcert/ethereum-erc721/blob/master/contracts/tokens/NFToken.sol#L310-L337

This is not formally verified, to a rigorous definition of the word. Actually very few things are formally verified, please see the Vyper project if you are interested in that -- people interested in formality are using that language.

But informally, you can see that onERC721Received, the recursion step is applied at the tail of this function. That is the important part.

Here is the standard text -- https://eips.ethereum.org/EIPS/eip-721 -- and it states:

When transfer is complete, this function checks if _to is a smart contract (code size > 0). If so, it calls onERC721Received on _to ...

Therefore this is a tail-end recursion, which follows the check effects interaction pattern.

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.