HackMD
  • Prime
    Prime  Full-text search on all paid plans
    Search anywhere and reach everything in a Workspace with Prime plan.
    Got it
    • Prime  Full-text search on all paid plans
      Prime  Full-text search on all paid plans
      Search anywhere and reach everything in a Workspace with Prime plan.
      Got it
      • Sharing Link copied
      • /edit
      • View mode
        • Edit mode
        • View mode
        • Book mode
        • Slide mode
        Edit mode View mode Book mode Slide mode
      • Note Permission
      • Read
        • Owners
        • Signed-in users
        • Everyone
        Owners Signed-in users Everyone
      • Write
        • Owners
        • Signed-in users
        • Everyone
        Owners Signed-in users Everyone
      • More (Comment, Invitee)
      • Publishing
        Everyone on the web can find and read all notes of this public team.
        After the note is published, everyone on the web can find and read this note.
        See all published notes on profile page.
      • Commenting Enable
        Disabled Forbidden Owners Signed-in users Everyone
      • Permission
        • Forbidden
        • Owners
        • Signed-in users
        • Everyone
      • Invitee
      • No invitee
      • Options
      • Versions and GitHub Sync
      • Transfer ownership
      • Delete this note
      • Template
      • Insert from template
      • Export
      • Dropbox
      • Google Drive
      • Gist
      • Import
      • Dropbox
      • Google Drive
      • Gist
      • Clipboard
      • Download
      • Markdown
      • HTML
      • Raw HTML
    Menu Sharing Help
    Menu
    Options
    Versions and GitHub Sync Transfer ownership Delete this note
    Export
    Dropbox Google Drive Gist
    Import
    Dropbox Google Drive Gist Clipboard
    Download
    Markdown HTML Raw HTML
    Back
    Sharing
    Sharing Link copied
    /edit
    View mode
    • Edit mode
    • View mode
    • Book mode
    • Slide mode
    Edit mode View mode Book mode Slide mode
    Note Permission
    Read
    Owners
    • Owners
    • Signed-in users
    • Everyone
    Owners Signed-in users Everyone
    Write
    Owners
    • Owners
    • Signed-in users
    • Everyone
    Owners Signed-in users Everyone
    More (Comment, Invitee)
    Publishing
    Everyone on the web can find and read all notes of this public team.
    After the note is published, everyone on the web can find and read this note.
    See all published notes on profile page.
    More (Comment, Invitee)
    Commenting Enable
    Disabled Forbidden Owners Signed-in users Everyone
    Permission
    Owners
    • Forbidden
    • Owners
    • Signed-in users
    • Everyone
    Invitee
    No invitee
       owned this note    owned this note      
    Published Linked with GitHub
    Like1 BookmarkBookmarked
    Subscribed
    • Any changes
      Be notified of any changes
    • Mention me
      Be notified of mention me
    • Unsubscribe
    Subscribe
    # Formal Verification of Zesty Smart Contracts ## Summary This document describes the specification and verification of Zesty Market using the Certora Prover. The work was undertaken from June 21, 2021 to July 4, 2021. All commits are run through the Certora Prover. The scope of our verification was the Zesty Markets logic. The Certora Prover proved the implementation of the Zesty Market is correct with respect to the formal rules written by the Zesty and the Certora teams. During the verification process, the Certora Prover discovered bugs in the code listed in the table below. All issues were promptly corrected, and the fixes were verified to satisfy the specifications up to the limitations of the Certora Prover. The Certora development team is currently handling these limitations. The next section formally defines high level specifications of Zesty. [All the rules are publically available](https://github.com/zestymarket/zesty-contracts-v2/tree/main/specs). Certora Prover run results: - [Zesty Market V1_1](https://vaas-stg.certora.com/output/43260/a03f1d5d9acc92de66e1?anonymousKey=28767ccc25cd5fec3d4108de7e13990cfd9ce1a2) - [Zesty Market V2](https://vaas-stg.certora.com/output/43260/5167604c74cafa114f69?anonymousKey=6ba5e3192e6b10e14b762c27313ca31a5c6605f6) - [Zesty NFT](https://vaas-stg.certora.com/output/43260/6c39a6b984e26acea5c3/?anonymousKey=895cd4f0d63d2ba65d34b35bace9797d257370ae) ## List of Main Issues Discovered **Severity: <span style="color:red">**High**</span>** | Issue: | Integrity of auction times can be violated | | -------- | -------- | | Rules Broken: | Time ranges validity | | Description: | Contract time start is not checked to be within `(auction time start, contract time end)`. Specifically, it is only checked to be greater than `auction time start`. | | Mitigation/Fix: | Add a require statement to auction creation function. | **Severity: <span style="color:red">**High**</span>** | Issue: | Auction cancel operation may fail unexpectedly | | -------- | -------- | | Rules Broken: | Revert conditions for auction cancellation | | Description: | An unexpected subtraction overflow caused by wrong ordering of storage writes. Found by the Zesty team. | | Mitigation/Fix: | Reorder storage updates so that we do not dereference deleted storage. | **Severity: <span style="color:blue">**Recommendation**</span>** | Issue: | No need to keep an extra variable for an address | | -------- | -------- | | Rules Broken: | N/A | | Description: | There is no need to keep an extra state variable of type address to mirror the value of a type such as `IERC20`. | | Mitigation/Fix: | Remove the address state variable. | ## Disclaimer The Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of the Certora Prover are scoped to the provided specification, and the Certora Prover does not check any cases not covered by the specification. We hope that this information is useful, but provide no warranty of any kind, explicit or implied. The contents of this report should not be construed as a complete guarantee that the contract is secure in all dimensions. In no event shall Certora or any of its employees be liable for any claim, damages or other liability, whether in an action of contract, tort or otherwise, arising from, out of or in connection with the results reported here. ## Notations ✔️ indicates the rule is formally verified on the latest reviewed commit. We write ✔️* when the rule was verified on a simplified version of the code (or under some assumptions). ![](https://i.imgur.com/rDhiM7e.png =20x20) indicates the rule was violated under one of the tested versions of the code. ✍ indicates the rule is not yet formally specified. 🔁 indicates the rule is postponed. We use Hoare triples of the form {p} C {q}, which means that if the execution of program C starts in any state satisfying p, it will end in a state satisfying q. In Solidity, p is similar to require, and q is similar to assert. The syntax {p} (C1 ~ C2) {q} is a generalization of Hoare rules, called relational properties. {p} is a requirement on the states before C1 and C2, and {q} describes the states after their executions. Notice that C1 and C2 result in different states. As a special case, C1~op C2, where op is a getter, indicating that C1 and C2 result in states with the same value for op. ## Verification of ZestyNFT Implementation of ERC721 for Zesty NFT tokens. ### Functions 1. `balanceOf(address owner): uint256` Returns the number of NFTs held by the given owner. 2. `ownerOf(uint256 tokenId): address` Returns the owner of the NFT with the given token ID. 3. `tokenOfOwnerByIndex(address owner, uint256 index): uint256` Returns the token ID held by the given owner in the provided index. (exposes internal state.) 4. `totalSupply(): uint256` Returns the number of NFTs in circulation. 5. `tokenByIndex(uint256 index): uint256` Returns the token ID in the given global index. (exposes internal state.) 6. `mint(string uri)` Mints a new NFT. 7. `burn(uint256)` Burns an NFT. 8. `transferFrom(address from, address to, uint256 tokenId)` Transfer the NFT with the given token ID from the provided from address to the desired recipient. 9. `safeTransferFrom(address from, address to, uint256 tokenId, bytes data)` Similar to `transferFrom` but with additional guarantees about the recipient being compatible with the NFT. ### Properties 1. Transfer functions only changes the ownership of the token ID to be transferred and no other token ID ✔️ 2. Consistency of `tokenOfOwnerByIndex` - unless the holder transfers their NFT, and the token is having the same index for the owner, then it cannot be assigned a different owner ✔️ ## Verification of Zesty Vault Store of Zesty NFTs. The vault is abstract and is used by both versions of Zesty Market. ### Functions 1. `authorizeOperator(address _operator)` 2. `revokeOperator(address _operator)` 3. `depositZestyNFT(uint256)` (internal) 4. `withdrawZestyNFT(uint256)` (internal) 5. `getDepositor(uint256 tokenID): address` Getter for NFT deposits, mapping a token ID to its depositor. 6. `getOperator(address depositor): address` Getter for NFT deposit operators, mapping a depositor to its operator. 7. `getZestyNFTAddress(): address` Return the address of the underlying NFT. ### Properties 1. Cannot transfer NFTs that do not belong to the sender 🔁 ## Zesty Market V1.1 ### Functions Some of the functions are allowing for batching several operations of the same type, by treating each of the arguments as an array, and enforcing all arguments arrays have the same length. We mark such functions below, but present them as if they were a single operation. 1. `buyerCampaignCreate(string uri)` Creates a new campaign identified by the given URI. 2. `sellerNFTDeposit(uint256 tokenId, uint8 autoApprove)` A seller deposits an NFT representing an ad space, and whether bids will be autoapproved or not. 3. `sellerNFTWithdraw(uint256 tokenId)` A seller withdraws an NFT representing an ad space, assuming all auctions have been closed. 4. `sellerNFTUpdate(uint256 tokenId, uint8 autoApprove)` A seller updates auto approval for the NFT with the given token ID. 5. `sellerBan(address a)` A seller bans a potential buyer with the given address a. 6. `sellerUnban(address a)` A seller unbans a potential buyer with the given address a. 7. `sellerAuctionCreate(uint256 tokenId, uint256 auctionTimeStart, uint256 auctionTimeEnd, uint256 contractTimeStart, uint256 contractTimeEnd, uint256 priceStart)` A seller creates a single auction. (In code: Batched version.) 8. `sellerAuctionCancel(uint256 sellerAuctionId)` A seller cancels a single auction (assuming no bids). (In code: Batched version.) 9. `sellerAuctionBid(uint256 sellerAuctionId, uint256 buyerCampaignId)` A buyer bids in a single auction. (In code: Batched version.) 10. `sellerAuctionBidCancel(uint256 sellerAuctionId)` A buyer cancels a bid in a single auction. (In code: Batched version.) 11. `sellerAuctionApprove(uint256 sellerAuctionId)` A seller approves a buyer's bid. (In code: Batched version.) 12. `sellerAuctionReject(uint256 sellerAuctionId)` A seller rejects a buyer's bid, returning bid sum to buyer. (In code: Batched version.) 12. `contractWithdraw(uint256 contractId)` A seller withdraws a fulfilled contract, receiving bid sum. (In code: Batched version.) 13. `getSellerNFTSetting(uint256 tokenId): (uint256 tokenId, address seller, uint8 autoApprove, uint256 inProgressCount)` Getter for the NFT settings (auto approval flag) of the given token ID. 14. `getSellerAuctionPrice(uint256 sellerAuctionId): uint256` Computes the relative price taking into account the elapsed time. (Math: decreases monotonically until contract time end, beginning from the start price.) 15. `getSellerAuction(uint256 id): (address seller, uint256 tokenId, uint256 auctionTimeStart, uint256 auctionTimeEnd, uint256 contractTimeStart, uint256 contractTimeEnd, uint256 priceStart, uint256 pricePending, uint256 priceEnd, uint256 buyerCampaign, uint8 buyerCampaignApproved)` Getter for the seller auction for the given ID. 16. `getBuyerCampaign(uint256 id): (address buyer, string uri)` Getter for the buyer campaign for the given ID. 17. `getContract(uint256 id): (uint256 sellerAuctionId, uint256 buyerCampaignId, uint256 contractTimeStart, uint256 contractTimeEnd, uint256 contractValue, uint8 withdrawn)` Getter for the contract with the given ID. ### Properties 1. For a token that is mapped to a seller, auto approve can be either 1 ("FALSE") or 2 ("TRUE"), and if the token is not mapped to a seller, then auto approve is 0. ✔️ 2. Seller auction price rules: a. Price decreases monotonically in time ✔️ b. Price may only decrease in transitions ✔️ c. Price at auction time start is equal to the specified start price ✔️ 3. Batchable operations are additive: we get the same erc20 effect for the sender and the market contract for each batchable operation (e.g. bid) when running on [a1, a2] and on ([a1], [a2]). a. Additivity of bid ✔️ b. Additivity of approve ✔️ c. Additivity of bid cancel ✔️ d. Additivity of reject ✔️ e. Additivity of withdraw ✔️ 4. Either `priceEnd` or `pricePending` should be zero. Both cannot be non-zero. ✔️ 5. Before bidding and setting the winning campaign, there cannot be a `priceEnd` or `pricePending` setting ✔️ 6. Once `priceEnd` is set, `pricePending` must be zero and the campaign must be approved ✔️ 7. Auctions above the seller auction count must be uninitialized ✔️ 8. Campaigns above the buyer campaign count must be uninitialized, and campaign ID 0 is never initialized ✔️ 9. Contracts above the contract count must be uninitialized ✔️ 10. NFT depositor is the same as the seller set in NFT settings ✔️ 11. An auction's token ID must have the same seller in both auctions struct and settings struct ✔️ 12. Once a contract is marked as withdrawn this cannot be changed ✔️ 13. Solvency. The token balance of the market must be greater than the sum of all pending auction bids, plus all ended auction bids, minus the sum of all withdrawn contract valus. ✔️ 14. Monotonicity of counters a. Buyer campaign count should monotincally increase and start at 1 ✔️ b. Seller auction count should monotonically increase and start at 1 ✔️ 15. Time ranges validity: For a created auction, auction time end must be greater than auction time start, contract time end must be greater than contract time start and auction time end ![](https://i.imgur.com/rDhiM7e.png =20x20) 16. All calls that have potential external calls protect against reentrancy ✔️ 17. When an NFT is deposited in the contract, owner shouldn't be able to withdraw it unless the in progress count is set to 0 🔁 18. An auction can have a price if and only if it has a buyer campaign ✔️ 19. If an NFT has a seller, then it must be owned by the contract 🔁 20. The variables for `txToken` and `txTokenAddress` hold the same value. ✔️ 21. The difference in price pending + price delta is equal to the difference in the balance of the buyer and/or market, where every batchable operation is assumed to take just one element. ✔️ ``` let price(auctionId) = getAuctionPricePending(auctionId) + getAuctionPriceEnd(auctionId) let delta_price(auctionId) = p' - p in { p = price(auctionId) } op(); { p' = price(auctionId) } let delta_balance(u) = b' - b in { b = token.balanceOf(u) } op(); { b' = token.balanceOf(u) } { buyerBalance = token.balanceOf(buyer) ∧ buyer ≠ market ∧ hasBuyer = getAuctionBuyerCampaign(auctionId) ≠ 0 ∧ buyer = getBuyer(getAuctionBuyerCampaign(auctionId)) } op() where op is sellerAuctionApproveBatch([auctionId]) v op is sellerAuctionBidCancelBatch([auctionId]) v op is sellerAuctionRejectBatch([auctionId]) { hasBuyer ⇒ delta_price(auctionId) = delta_balance(buyer) ∧ delta_price(auctionId) = delta_balance(market) } { buyerBalance = token.balanceOf(buyer) ∧ buyer ≠ market ∧ buyer = getBuyer(c) } op() where op is sellerAuctionBidBatch([auctionId], c) { delta_price(auctionId) = delta_balance(buyer) ∧ delta_price(auctionId) = delta_balance(market) } ``` 22. Revert conditions for bid cancellation ✔️ 23. Revert conditions for auction cancellation ✔️![](https://i.imgur.com/rDhiM7e.png =20x20) ## Zesty Market V2 The Zesty Market V2 is very similar in structure and functionality to V1, but includes better checking of actual contract fulfillment by the seller. Most of the rules for V1 can be applied to V2 as well, and no new violations were found.

    Import from clipboard

    Advanced permission required

    Your current role can only read. Ask the system administrator to acquire write and comment permission.

    This team is disabled

    Sorry, this team is disabled. You can't edit this note.

    This note is locked

    Sorry, only owner can edit this note.

    Reach the limit

    Sorry, you've reached the max length this note can be.
    Please reduce the content or divide it to more notes, thank you!

    Import from Gist

    Import from Snippet

    or

    Export to Snippet

    Are you sure?

    Do you really want to delete this note?
    All users will lost their connection.

    Create a note from template

    Create a note from template

    Oops...
    This template is not available.


    Upgrade

    All
    • All
    • Team
    No template found.

    Create custom template


    Upgrade

    Delete template

    Do you really want to delete this template?

    This page need refresh

    You have an incompatible client version.
    Refresh to update.
    New version available!
    See releases notes here
    Refresh to enjoy new features.
    Your user state has changed.
    Refresh to load new user state.

    Sign in

    Forgot password

    or

    By clicking below, you agree to our terms of service.

    Sign in via Facebook Sign in via Twitter Sign in via GitHub Sign in via Dropbox

    New to HackMD? Sign up

    Help

    • English
    • 中文
    • Français
    • Deutsch
    • 日本語
    • Español
    • Català
    • Ελληνικά
    • Português
    • italiano
    • Türkçe
    • Русский
    • Nederlands
    • hrvatski jezik
    • język polski
    • Українська
    • हिन्दी
    • svenska
    • Esperanto
    • dansk

    Documents

    Tutorials

    Book Mode Tutorial

    Slide Mode Tutorial

    YAML Metadata

    Contacts

    Facebook

    Twitter

    Feedback

    Send us email

    Resources

    Releases

    Pricing

    Blog

    Policy

    Terms

    Privacy

    Cheatsheet

    Syntax Example Reference
    # Header Header 基本排版
    - Unordered List
    • Unordered List
    1. Ordered List
    1. Ordered List
    - [ ] Todo List
    • Todo List
    > Blockquote
    Blockquote
    **Bold font** Bold font
    *Italics font* Italics font
    ~~Strikethrough~~ Strikethrough
    19^th^ 19th
    H~2~O H2O
    ++Inserted text++ Inserted text
    ==Marked text== Marked text
    [link text](https:// "title") Link
    ![image alt](https:// "title") Image
    `Code` Code 在筆記中貼入程式碼
    ```javascript
    var i = 0;
    ```
    var i = 0;
    :smile: :smile: Emoji list
    {%youtube youtube_id %} Externals
    $L^aT_eX$ LaTeX
    :::info
    This is a alert area.
    :::

    This is a alert area.

    Versions

    Versions and GitHub Sync

    Sign in to link this note to GitHub Learn more
    This note is not linked with GitHub Learn more
     
    Add badge Pull Push GitHub Link Settings
    Upgrade now

    Version named by    

    More Less
    • Edit
    • Delete

    Note content is identical to the latest version.
    Compare with
      Choose a version
      No search result
      Version not found

    Feedback

    Submission failed, please try again

    Thanks for your support.

    On a scale of 0-10, how likely is it that you would recommend HackMD to your friends, family or business associates?

    Please give us some advice and help us improve HackMD.

     

    Thanks for your feedback

    Remove version name

    Do you want to remove this version name and description?

    Transfer ownership

    Transfer to
      Warning: is a public team. If you transfer note to this team, everyone on the web can find and read this note.

        Link with GitHub

        Please authorize HackMD on GitHub

        Please sign in to GitHub and install the HackMD app on your GitHub repo. Learn more

         Sign in to GitHub

        HackMD links with GitHub through a GitHub App. You can choose which repo to install our App.

        Push the note to GitHub Push to GitHub Pull a file from GitHub

          Authorize again
         

        Choose which file to push to

        Select repo
        Refresh Authorize more repos
        Select branch
        Select file
        Select branch
        Choose version(s) to push
        • Save a new version and push
        • Choose from existing versions
        Available push count

        Upgrade

        Pull from GitHub

         
        File from GitHub
        File from HackMD

        GitHub Link Settings

        File linked

        Linked by
        File path
        Last synced branch
        Available push count

        Upgrade

        Danger Zone

        Unlink
        You will no longer receive notification when GitHub file changes after unlink.

        Syncing

        Push failed

        Push successfully