diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 75a222d..19d02f1 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -49,4 +49,4 @@ jobs: with: name: ${{ github.ref_name }} tag_name: ${{ github.ref_name }} - files: "src/*.pdf" \ No newline at end of file + files: "outputs/*.pdf" \ No newline at end of file diff --git a/butane-sale/butane-sale.typ b/butane-sale/butane-sale.typ new file mode 100644 index 0000000..ae3424c --- /dev/null +++ b/butane-sale/butane-sale.typ @@ -0,0 +1,879 @@ +#import "../template/audit.typ": * +#import "@preview/finite:0.3.0": automaton + +#show: report.with( + client: "Butane", + title: "Pro-rata Sale", + repo: "https://github.com/SundaeSwap-finance/sundae-audits", + date: "2023-02-21", + authors: ( + ( + name: "Pi Lanningham", + display: text(1.3em, $pi$) + " Lanningham", + ), + ), +) + += Audit Manifest + +Please find below the list of pinned software dependencies and files that were covered by the audit. + +#software_versions( + items: ( + ( + name: "Pro-rata Sale", + version: "0.0.0", + commit: "580bba7c85603cd87f6b1e037d30915ca0cf543f", + ), + ) +) + +#files_audited( + items: ( + ( + file: "validators/sale.ak", + hash: "75780d0962a096b13176c9ac10664a94a6c38badfdb633a9f09be654685c6568", + ), + ( + file: "validators/nft.ak", + hash: "e50a6642c85499da9ccfa18204b4c63d9455a7edde86726746017eef98a4acbf", + ), + ( + file: "lib/launchpad/prorata.ak", + hash: "b141707194119480c4ab4df48acfc941534e6b52d6ba1718a57834ddef0fc37e", + ), + ( + file: "lib/launchpad/types.ak", + hash: "9c322668b8e8c034ede0ecaca95df242c5de66b9b0bef1046fc6bfd695c77496", + ), + ( + file: "lib/launchpad/utils.ak", + hash: "512c6c801f07d6b8ae5d200fc48326b45b36f1161f7e25b278401cc695e6b8ae", + ), + ) +) + +#artifacts( + ( + ( + validator: "sale", + method: "deposit", + hash: "", + ), + ( + validator: "sale", + method: "collect", + hash: "", + ), + ( + validator: "sale", + method: "machine", + hash: "", + ), + ( + validator: "nft", + method: "nft", + hash: "", + ) + ) +) + +#pagebreak() + +#set par( + leading: 1em, + first-line-indent: 1em, + justify: true, +) + += Context + +The Butane token is a new cardano native token with utility in the upcoming "Butane" synthetics protocol. The scripts under audit are a set of smart contracts that govern a so-called "pro-rata" sale of these tokens. The butane team intends to offer 43% of the total supply (10,750,000 Butane) to the public in this sale, at a rate of 0.9 ADA per Butane. + +If less than 9,675,000 ADA is raised, the remaining tokens will be burned, reducing the total supply. If more than 9,675,000 ADA is raised, then each user will use the same percentage of their deposit to buy the token at that rate, and the remaining ADA will be returned to them. + +For example, if 10,000,000 ADA is raised, then only 96.75% of the raised ADA can actually purchase tokens. Thus, a user who deposited 1,000 ADA would use 967.5 ADA to purchase 1075 Butane, and 32.5 ADA would be returned. + +#v(1em) +#set par(first-line-indent: 0em) +This audit was performed by Sundae Labs, with the following understanding: + - There would be an "admin" user that should be acknowledged as a point of centralization, and should be treated as a largely trusted actor. + - That is, this actor should never have direct access to the user funds, but can be trusted to progress the protocol, and provide accurate off-chain global state. + - Performance of the contracts is not a factor. + - To limit scope and complexity, we are only auditing the Sale portion, not the Butane minting policy. + - The duration in which the sale should be active is limited, minimizing the window of time in which an attacker has to find a vulnerability. + - The contracts will remain closed source during the sale, minimizing the information available to an attacker during that vulnerable window. + +#pagebreak() + += Specification + +The butane prorata sale protocol is intended to facilitate the initial public sale of the Butane token. + +The high level objectives of this sale are: + - A trusted admin begins the sale + - While the sale is active, users can deposit funds in a bid to purchase Butane tokens + - This deposit must be a minimum amount of ADA + - At the end of the sale, the admin can close the sale, preventing further deposits + - The admin can then calculate the total subscription of the sale, and lock in a "pro-rata" percentage + - Users, or the admin in large batches, can then claim their portion of the sold tokens, paying a fixed rate for those they mint, and receiving the remaining amount of ADA in return. + - When rounding, values should be rounded in favor of the protocol. That is, a user may receive up to 1 diminutive unit less of Butane than they paid for, resulting in a slightly smaller total supply of Butane. + - The admin can exercise discretion over the timing of the raise + - The admin should not be able to change the terms of the sale + - Users should be able to reclaim their ADA after an expiration if the sale doesn't terminate for some reason. + +In particular, what we mean by pro-rata distribution is: + - Let the butane price be the quantity of butane per 1 ADA raised + - Let the total purchased butane amount be the total deposited ADA multiplied by the butane price + - If the total purchased butane amount is less than the amount allocated to the sale + - Let each deposit be spent if the deposited ADA is paid to the admin, and `deposit_amount * butane_price` is minted and paid to the depositer + - If the total purchased butane amount is greater than the amount allocated to the sale + - Let the pro-rata percentage be `sale_allocation / total_purchased_butane_amount` + - Let the pro-rata payment be `deposited_ada * pro_rata_percentage` + - Let the rebate amount be `deposited_ada - pro_rata_payment` + - Let each deposit be spent if `pro_rata_payment` ADA is paid to the admin, and `pro_rata_payment * butane_price` Butane plus `rebate_amount` ADA is paid to the depositer + +#pagebreak() + +The full protocol should adhere to the following state transition diagram: +#v(3em) +#scale(x: 150%, y: 150%, origin: top+left)[ + #automaton( + ( + Pending: (Live:("Begin Sale")), + Live: (Counting:("End Sale")), + Counting: (Closed:("Close Sale")), + Closed: (nil: ("Burn")), + nil: (), + ), + layout: ( + Pending: (0,0), + Live: (2.5,0), + Counting: (5, 0), + Closed: (7.5, 0), + nil: (7.5, -2) + ), + style: ( + Closed-nil: ( + label: ( + angle: 90deg, + ) + ), + Pending: (stroke: red), + Live: (stroke: blue), + Counting: (stroke: purple), + Closed: (stroke: green), + ) + ) +] +#v(8em) +Each depositing user should adhere to the following state transition diagram. The highlighted transitions are only valid when the sale is in the appropriately colored state above. + +#v(3em) +#scale(x: 150%, y: 150%, origin: top+left)[ + #automaton( + ( + Abstain: (Deposit: ("Deposit")), + Deposit: (Claimed: ("Claim"), Reclaimed: ("Expired")), + Claimed: (), + Reclaimed: (), + ), + final: ("Abstain", "Claimed", "Reclaimed"), + layout: ( + Abstain: (0,0), + Deposit: (2.5, 0), + Claimed: (5, 0), + Reclaimed: (2.5, -2), + ), + style: ( + Abstain-Deposit: (stroke: blue), + Deposit-Claimed: (stroke: green), + ) + ) +] + +#pagebreak() + +== Detailed Specification + +=== Definitions + +#defn("Butane Token", "The native token of the butane protocol being sold as part of these contracts") +#defn("Public Sale", [ + A specific offering of the #ref("Butane Token") available to all users through the decentralized protocol covered by this audit +]) +#defn("Admin UTXO", [ + A trusted UTXO, authenticated by a unique NFT, used as a reference input to describe the global state of the #ref("Public Sale") +]) +#defn("Admin NFT", [ + The NFT authenticating the #ref("Admin UTXO") +]) +#defn("State Machine", [ + A smart contract implementing a simple state machine through which the #ref("Admin UTXO") is advanced by the #ref("Admin"). +]) +#defn("Admin", [ + A user trusted to advance the #ref("Admin UTXO") through the stages of the sale correctly. +]) +#defn("Deposit", [ + Either: + - The act of depositing ADA to participate in the sale + - A specific UTXO holding the ADA of a user participating in the sale +]) +#defn("Counting Token", [ + A temporary token minted to authenticate participation in the #ref("Public Sale"). +]) +#defn("Sale Allocation", [ + The total amount of #ref("Butane Token") allocated to the #ref("Public Sale") +]) +#defn("Sale Price", [ + The price of the #ref("Butane Token") for the purposes of the #ref("Public Sale"), either in ADA per Butane or Butane per ADA, depending on context. +]) +#defn("Target Raise", [ + The total amount of ADA being sought as part of the #ref("Public Sale"). Calculated as the #ref("Sale Allocation") times the #ref("Sale Price") in ADA per Butane. +]) +#defn("Subscription", [ + The total amount of ADA deposited in the #ref("Public Sale") + + Related: + - A #ref("Public Sale") is under-subscribed when the total amount of ADA raised is less than the #ref("Target Raise") + - A #ref("Public Sale") is over-subscribed when the total amount of ADA raised is greater than the #ref("Target Raise") +]) +#defn("Pro-rata Percentage", [ + The percentage of the #ref("Sale Allocation") that each user is entitled to, based on their deposit amount. + This is calculated as follows: + - If under-subscribed, it is 100% + - If over-subscribed, it is the #ref("Sale Allocation") divided by the #ref("Subscription"). +]) +#defn("Rebate", [Some amount of ADA returned returned to the user when the #ref("Public Sale") is over-subscribed.]) +#defn("Target Recipient", [The cardano address that will receive ADA raised from the #ref("Public Sale")]) +#defn("Recipient", [The address attached to a specific deposit which will receive the #ref("Butane Token") and possibly a #ref("Rebate").]) + +#pagebreak() + +=== Transactions + +There are 7 transaction archetypes in this protocol. We present each in detail below. + +- Initialization + - A new #ref("Public Sale") is initialized by the #ref("Admin") creating the #ref("Admin UTXO") + - An NFT must be minted and paid into a UTXO with the correct `Pending` datum. + - This represents the initial `Start` transition in the state diagram above. + +#v(5em) +#transaction( + "Initialization", + inputs: ( + ( + name: "Admin Wallet", + value: ( + ada: "minUTXO", + ) + ), + ), + outputs: ( + ( + name: "Admin UTXO", + address: "State Machine", + value: ( + ada: "minUTXO", + NFT: 1, + ), + datum: ( + "Pending": "" + ) + ), + ) +) + +#pagebreak() + +- Begin Sale + - The #ref("Admin") opens the sale to the public by spending the #ref("Admin UTXO") and updating the state to `Live`. + - Represents the transition from "Pending" to "Live" in the diagram above. + - Involves a commitment to sale details. + +#v(5em) +#transaction( + "Begin Sale", + inputs: ( + ( + name: "Admin UTXO", + address: "State Machine", + value: ( + ada: "minUTXO", + NFT: 1, + ) + ), + ), + outputs: ( + ( + name: "Admin UTXO", + address: "State Machine", + value: ( + ada: "minUTXO", + NFT: 1, + ), + datum: ( + "Live": ( + total_expected_ada: [A#sub[e]], + price_n: [P#sub[n]], + price_d: [P#sub[d]], + mint_token_pol: "policy", + mint_token_tn: "token name", + expiry_time: [`K`], + ) + ) + ), + ) +) + +#pagebreak() + +- Deposit + - A user deposits ADA, securing their position in the #ref("Public Sale"). + - An equal amount of #ref("Counting Token") is minted to verify that the deposit was made while the #ref("Public Sale") was still ongoing, rather than after the fact. + - The #ref("Public Sale") must be live, as proven through a reference input. + - The user must commit to the details of the sale. + - Represents the users transition from "Abstain" to "Deposit" in the diagram above. + +#v(5em) +#transaction( + "Deposit", + inputs: ( + ( + name: "User Wallet", + value: ( + ada: "X+Y", + ) + ), + ( + name: "Admin UTXO", + address: "State Machine", + reference: true, + value: ( + ada: "minUTXO", + NFT: 1, + ), + datum: ( + "Live": ( + total_expected_ada: [A#sub[e]], + price_n: [P#sub[n]], + price_d: [P#sub[d]], + mint_token_pol: "policy", + mint_token_tn: "token name", + expiry_time: [`K`], + ) + ) + ) + ), + outputs: ( + ( + name: "Deposit UTXO", + address: "sale.collect", + value: ( + ada: "X", + counting: "X", + ), + datum: ( + recipient: "User Address", + locked_lovelace: "X", + details_hash: [`H`], + expiry_time: [`K`], + ) + ), + ( + name: "Change UTXO", + address: "User Address", + value: ( + ada: "Y", + ) + ), + ), + notes: [ + `H` is the hash of the admin Datum launch details. + ] +) + +#pagebreak() + +- End Sale + - End the #ref("Public Sale"), preventing further deposits + - Also allows time for the #ref("Admin") to calculate the #ref("Subscription") and #ref("Pro-rata Percentage") before closing the sale. + - Represents the transition from "Live" to "Counting" in the diagram above. + +#v(5em) +#transaction( + "End Sale", + inputs: ( + ( + name: "Admin UTXO", + address: "State Machine", + value: ( + ada: "minUTXO", + NFT: 1, + ), + datum: ( + "Live": ( + total_expected_ada: [A#sub[e]], + price_n: [P#sub[n]], + price_d: [P#sub[d]], + mint_token_pol: "policy", + mint_token_tn: "token name", + expiry_time: [`K`], + ) + ) + ), + ), + outputs: ( + ( + name: "Admin UTXO", + address: "State Machine", + value: ( + ada: "minUTXO", + NFT: 1, + ), + datum: ( + "Counting": "" + ) + ), + ) +) + +#pagebreak() + +- Close Sale + - The #ref("Admin") closes the sale after calculating the #ref("Subscription") and #ref("Pro-rata Percentage"). + - Locks in a price and a #ref("Subscription") amount, so that claims can begin claiming. + - Represents the transition from "Pending" to "Closed" in the diagram above. + +#v(5em) +#transaction( + "Close Sale", + inputs: ( + ( + name: "Admin UTXO", + address: "Admin Address", + value: ( + ada: "minUTXO", + NFT: 1, + ), + datum: ( + "Counting": "" + ) + ), + ), + outputs: ( + ( + name: "Admin UTXO", + address: "Admin Address", + value: ( + ada: "minUTXO", + NFT: 1, + ), + datum: ( + "Closed": ( + "total_deposited_ada": [A#sub[d]], + ) + ) + ), + ) +) + +#pagebreak() + +- Claim + - Someone (either the user, or someone on their behalf) spends a deposit, burning the #ref("Counting Token"), paying the appropriate ADA to the #ref("Target Recipient"), and minting the appropriate amount of #ref("Butane Token"), paid along with any #ref("Rebate") to the #ref("Recipient"). + - $P_n / P_d$ is the #ref("Sale Price") denominated in ADA per Butane + - $A_e$ refers to the #ref("Sale Allocation") + - $A_d$ refers to the #ref("Subscription") + +#v(2em) +#transaction( + "Claim", + inputs: ( + ( + name: "Deposit UTXO", + address: "sale.collect", + value: ( + ada: "X", + counting: "X", + ), + datum: ( + recipient: [`recipient1`], + locked_lovelace: "X", + details_hash: [`H`], + expiry_time: [`K`], + ) + ), + ( + name: "Deposit UTXO", + value: ( + ada: "Y", + counting: "Y", + ), + datum: ( + "...": "" + ) + ), + ( + name: "...", + ), + ( + name: "Admin UTXO", + reference: true, + value: ( + ada: "minUTXO", + NFT: 1, + ), + datum: ( + "Closed": ( + "total_deposited_ada": [A#sub[d]], + ) + ) + ), + ), + outputs: ( + ( + name: "User Output", + address: [`recipient1`], + value: ( + ada: "X - Pa", + butane: "Ba", + ), + ), + ( + name: "User Output 2", + address: [`recipient2`], + value: ( + ada: "Y - Pb", + butane: "Bb", + ) + ), + ( + name: "Payment UTXO", + address: "Target Recipient", + value: ( + ada: "Pa + Pb", + ) + ), + ), + notes: [ + #linebreak() + `H` must match hash of details in each deposits redeemer + $ P_i = cases( + X_i "if" A_d <= A_e, + floor(frac(X_i * A_e, A_d)) "if" A_d > A_e, + ) $ + $ B_i = floor(frac(P_i * P_d, P_n)) $ + ] +) + +#pagebreak() + +- Reclaim + - Someone reclaims their ADA after the expiration. + - Only used in disaster recovery, if the sale datum is burned too soon. + +#v(2em) +#transaction( + "Reclaim", + inputs: ( + ( + name: "Deposit UTXO", + address: "sale.collect", + value: ( + ada: "X", + counting: "X", + ), + datum: ( + recipient: [`recipient1`], + locked_lovelace: "X", + details_hash: [`H`], + expiry_time: [`K`], + ) + ), + ( + name: "Deposit UTXO", + value: ( + ada: "Y", + counting: "Y", + ), + datum: ( + "...": "" + ) + ), + ( + name: "...", + ), + ), + outputs: ( + ( + name: "User Output", + address: [`recipient1`], + value: ( + ada: "X", + ), + ), + ( + name: "User Output 2", + address: [`recipient2`], + value: ( + ada: "Y", + ) + ), + ), + notes: [ + #linebreak() + `K` must be before the transaction lower bound. + ] +) +#pagebreak() + +=== Core Invariants + +We use the following labels for the terms defined above: + - $P_n / P_d$ is the #ref("Sale Price") denominated in ADA per Butane + - $A_e$ refers to the #ref("Sale Allocation") + - $A_d$ refers to the #ref("Subscription") + +#set enum(numbering: "1.a)") +#v(1em) +The protocol is considered correctly executed if: + + The #ref("Admin NFT") is minted and paid with a `Pending` datum to the state machine script. + + The #ref("State Machine") is advanced to `Live` with sale details matching those published publicly. + + The #ref("State Machine") is advanced by the #ref("Admin") according to a reasonable schedule. + + At least 1 hour without rollbacks passes between advancing the #ref("State Machine") to `Counting`, and advancing it to `Closed`. + + The #ref("Subscription") amount provided to the state machine represents the total supply of the #ref("Counting Token"), and thereby the total amount of ADA locked in the script. + +#v(1em) +The following core invariants should hold: + + The #ref("Admin") can be trusted to progress the protocol, and provide accurate off-chain global state. + + A user can only mint an amount #ref("Counting Token") by paying the same amount of Lovelace into the `sale.collect` script + + A user must lock at least 300 ADA to participate in the sale. + + A user can only mint Butane by burning the full amount of #ref("Counting Token") on their UTXO + + A user can only mint #ref("Counting Token") while the #ref("Admin UTXO") is `Live` + + A user can only claim the results of the #ref("Public Sale") after the #ref("Admin UTXO") has progressed to the `Closed` state. + + The #ref("Admin") cannot change the details of the sale after it is in the `Live` state. + + The total minted butane minted must not exceed $A_e * P_d / P_n$ + + A user can only mint Butane by paying $P_n / P_d$ ADA per #ref("Butane Token") paid to the #ref("Target Recipient") + + The #ref("Butane Token") minted from a deposit must be paid to the #ref("Deposit") #ref("Recipient") + + If $A_d <= A_e$, a user must pay the full amount of `locked_lovelace` to the #ref("Target Recipient") and mint $floor(frac("locked_lovelace" * P_d, P_n))$ Butane to the #ref("Recipient") + + We use `floor` because we cannot mint a fractional diminutive unit, and rounding down favors the protocol: the user may receive 1 diminutive unit less Butane than they paid for + + This helps maintain Invariant 5 + + If $A_d > A_e$, a user must pay $"paid_lovelace" = floor(frac("locked_lovelace" * A_e, A_d))$ ADA to the #ref("Target Recipient") and mint $floor(frac("paid_lovelace" * P_d, P_n))$ Butane to the #ref("Recipient") + + We take the floor when calculating the `paid_lovelace` to maintain Invariant 5. If we took the ceiling, `paid_lovelace` might be 1 lovelace more than the correct pro-rata amount, which could result in higher minted Butane than the #ref("Sale Allocation") + + Similarly, we take the floor when calculating the minted Butane to maintain Invariant 5 + + Any difference between `locked_lovelace` and `paid_lovelace` must be returned to the #ref("Recipient") along with the minted Butane. + + After some minimum time delay, if the #ref("Deposit") hasn't been claimed yet, a user can reclaim their `locked_lovelace` from the `sale.collect` script +#pagebreak() + += Findings Summary + +#findings(prefix: "BTN", items: ( + ( + title: [No commitment to price or allocation by Admin], + severity: "Critical", + description: [ + The protocol has an Admin role, that has the following two trust assumptions: + - They will progress the protocol through the state machine + - In the Close sale transaction, they will provide an accurate value for $A_d$, such that $A_d$ is the sum of all `locked_lovelace` in valid #ref("Deposit")s. + + However, the admin has much more control and requires much more trust than this. In particular, there is no commitment to the total expected ADA, the sale price, or the butane token policy ID. + + This makes the following attacks possible, which we deem outside of a reasonable trust assumption for such a sale: + - Users lock up ADA in expectation of receiving Butane at a price of 0.9 ADA per Butane, and instead the price is set to 1000 ADA per Butane. + - Users lock up ADA in expectation of collectively receiving 43% of the supply, and instead only 0.1% of the supply is distributed, with the rest retained by the team. + - Users lock up ADA in expectation of receiving Butane, but are given some other worthless token instead. + ], + recommendation: [ + Add `total_expected_ada`, `price_n`, `price_d`, `mint_token_pol` and `mint_token_tn` to the `Pending` and `Live` datums. + + Lock the Admin UTXO in a script that allows the #ref("Admin") to adhere to the state changes, and enforces that these values remain the same during each state transition. + + This way, users can confirm the details of the sale before making the decision about whether to participate. + ], + resolution: ( + commit: "53cb47dc77da6a9c053d2ab9c8baf416ea1e7409" + ) + ), + ( + title: [Not commitment to sale schedule], + severity: "Major", + description: [ + The protocol assumes that the admin will be responsible for eventually progressing the protocol, but does not assume they are trusted to progress the protocol in accordance with a schedule. + + One design goal is to allow reasonable flexibility in the timing. This is to allow an *almost* subscribed sale to wait for it's full sale before closing, without prescribing a set time. + + However, in the current protocol, the admin must be trusted to adhere to that reasonable schedule. For example, the admin could drag out the sale for months if the sale is under-subscribed, trying to eke out more and more ADA, while participants are locked in and have no way to cancel. + + Similarly, the admin could close the sale at any time, limiting the participants and impacting the amount of Butane burned. + + Finally, the admin could reopen the sale after some tokens have been claimed, allowing further deposits to raise more ADA. + ], + recommendation: [ + Simplify the sale state machine to just include `Sale` and `Closed` states. + Lock the #ref("Admin UTXO") in a script that allows the admin to progress the protocol. + Add a `start_time`, `minimum_length` and `maximum_length` fields to the `Sale` and `Closed` datums. + Use the `start_time` to prevent deposits before the sale starts, and `start_time + maximum_length` to automatically close the sale and prevent further deposits. + Then, only a single transition from `Sale` to `Closed` is needed from the admin to report the #ref("Subscription"). Enforce that this happens after `start_time + minimum_length` to ensure the sale stays open for a minimum length of time. + Add the ability to reclaim ADA if they wish after some delay. This way, if the protocol never progresses for some reason, at the very least the ADA isn't locked forever. + + In this way, the #ref("Admin") has flexibility over the timing of the sale, but users also know ahead of time the reasonable bounds on the schedule of the protocol. The trust placed in the #ref("Admin") is minimized, as they are only trusted to progress the protocol and provide an accurate #ref("Subscription") amount. + ], + resolution: ( + comment: "Flexibility in the timing of the sale is a design goal, and combined with the state machine and expiration we implemented for other findings, we believe the timing issue is safely within trust assumptions we are comfortable with" + ) + ), + ( + title: [Admin can change terms during partial claim or deadlock unclaimed funds], + severity: "Critical", + description: [ + The admin is trusted to progress the protocol, and provide accurate information. + + However, in the current implementation, because the #ref("Admin UTXO") is just held in a wallet, after the sale is closed, the admin can spend the UTXO before all participants have claimed. + + First, this could be used to change the terms of the sale part way through claims. For example, the admin could immediately claim funds for any insiders immediately when the sale is closed, and then change the price or allocation for the remaining claimants. + + Second, the admin could spend the UTXO to remove the datum completely. Because claiming depends on this UTXO as a reference input, this would permanently lock users ADA in the deposit. + ], + recommendation: [ + As with the other findings, lock the #ref("Admin UTXO") in a script. The script should enforce that after the sale is closed and the terms are provided, it is never spent again. + + This ensures that no user funds become deadlocked, and the terms of the sale don't change after some users have claimed. + + Alternatively, allow users to reclaim their ADA after some timeout, to ensure that even if the Admin behaves badly, at the very least they get their ADA back. + ], + resolution: ( + commit: "bcddbd7a2a590404db8e6abbf0599b20b9b608eb" + ) + ), + ( + title: [Attach staking addresses to deposits], + severity: "Info", + description: [ + Because the sale may span an epoch boundary, you should ensure the users stake address is attached to any deposits. This doesn't impact the correctness of the script, but ensures that users earn staking rewards for any ADA before the sale officially completes. + + You likely intended to do this anyway, but it's worth highlighting explicitly. + ], + resolution: ( + comment: "We address this by enforcing the recipient stake address equals the deposit utxo stake address" + ) + ), + ( + title: [Incomplete solutions to previous findings], + severity: "Major", + description: [ + The solutions to #ref("BTN-000") and #ref("BTN-001") provide some protection, reducing the severity to only "Major", but are not sufficient in our view. + + #ref("BTN-000") was resolved by adding sale details to the `Live` datum, storing the hash of the sale details in the deposit datum, and verifying the sale details provided through the redeemer match the hash. + + #ref("BTN-001") was addressed by implementing a simple state machine that transitions from `Pending`, to `Live`, to `Closed`. + + However, the implementation suffers from two issues: + - The state machine never no longer has a transition back to `Pending`, meaning deposits cannot be halted to count up the total subscription. A user may deposit in between the total being counted and the sale being closed, resulting in an excess of Butane being minted. + - The state machine can be burned, deleting the admin token. Any unclaimed ADA would be permanently locked at that point. + ], + recommendation: [ + - Add an intermediate state to allow for counting the total subscription in between the close of the sale and the opening of claims. + - Either disallow the evaporation of the state machine, or add an expiration, after which a user that was never calimed can reclaim their ADA, even if the admin UTXO has been burned. + ], + resolution: ( + commit: "c0f71e9952487cd491888bfb13ad2e78b11a89b0" + ) + ), + ( + title: [Issues with minUTXO protections], + severity: "Info", + description: [ + One stated goal was to allow the user to lock up an arbitrary amount of ADA, so long as the purchase amount in the datum is less than or equal to the amount in the datum. + + This is to allow the user to include the minUTXO amount, so that the Butane team doesn't need to cover the minUTXO amount when forcing claims for users. + + However, there are three issues. + + First, the user is not actually allowed to lock up an arbitrary amount of ADA. When executing a deposit, the following condition is checked: + ``` + assert( + locked_value == ( + value.from_lovelace(lovelace_sent) + |> value.add(own_pid, "", lovelace_sent) + ), + @"Recipient value must be equal to the lovelace_sent field in the redeemer!", + ), + ``` + + This means that `locked_lovelace` from the datum must always match the amount of ADA in the deposit. + + Second, when claiming, the exact amount of ADA is checked here: + ```rust + // previously was validating that the input was the rebated value. + // Now, we check it correctly corresponds to datum. + (( lovelace |> dict.to_list ) == [("", locked_lovelace)])?, + ``` + + If the lovelace on the UTXO differs from the amount in the datum, the sale will be un-claimable. + + Finally, when checking the result, the amount sent back to the user is compared via: + ```rust + lovelace_amt >= must_rebate, + ``` + + If the user had included an extra amount in their deposit to cover minUTXO, and received a rebate, then whoever executed their claim would be able to take the surplus. + + Coincidentally, these issues nullify eachother: because the user cannot lock up additional ADA, there is no concern about the additional ADA being taken, or the UTXO being unspendable. + ], + recommendation: [ + If you would like to preserve this property, we recommend switching the first check to comparing a greaterthan, like so: + ``` + assert( + and { + value.lovelace_of(locked_value) >= lovelace_sent, + value.without_lovelace(locked_value) == value.add(own_pid, "", lovelace_sent) + }, + @"Recipient value must be equal to the lovelace_sent field in the redeemer!", + ), + ``` + + Then, update the second check to compare the #ref("Counting Token")s instead, like so: + ``` + (( other_dict |> dict.to_list ) == [("", locked_lovelace)])?, + ``` + + This is equivalent to the intention, since the minting policy checks that #ref("Counting Token")s are minted equal to the amount in the datum, but avoids the surplus ADA issue. + + Finally, we recommend checking that the amount sent to the user is exactly: + ``` + lovelace_amt == this_value.lovelace - must_send + ``` + + Which ensures that the user receives the full amount of ADA they put in, minus the amount they paid in the sale. + + Alternatively, you can simply acknowledge the risk that Butane may need to cover the minUTXO costs to fully realize the claim. The upper-bound for this cost would be if the full amount was subscribed exactly (meaning no rebates were available to cover the minUTXO), and the most users possible claimed at the minimum amount available. + + That would be roughly 32,250 users, with a minUTXO requirement of around 1.2 ADA, or around 38,700 ADA in minUTXO costs. In any case, the minUTXO cost is capped at 0.4% of the total raise. + ], + resolution: ( + comment: "We will take the latter approach; If we raise 10,000,000 ADA, having to cover up to 38,700 ADA in minUTXO costs is an acceptable risk for us.", + ) + ), + ( + title: [Funds could get deadlocked if the recipient is a script], + severity: "Minor", + description: [ + If users construct their own transaction to participate in the sale, and direct the funds to a script address, they may become permanently locked. + + First, the ADA could never be reclaimed, because the contracts explicitly expect VerificationKeyCredentials. + Second, we enforce that the output when minting the butane has NoDatum. A script address with NoDatum on the UTXO cannot be spent. + + We don't expect users to build their own transactions given the short time window when this will be active, but if these scripts are reused, this could be more of a concern. + ], + recommendation: [ + One approach is to split the `Destination` and the `Owner` into two separate fields. The destination is an address and a datum, and the owner is a condition authorized to reclaim the ADA after some time. + + A simpler approach is just to enforce that the `recipient` is a VerificationKeyCredential during the initial deposit. + ], + resolution: ( + commit: "580bba7c85603cd87f6b1e037d30915ca0cf543f" + ) + ) +)) \ No newline at end of file diff --git a/example/example.typ b/example/example.typ index 2604db5..b74471f 100644 --- a/example/example.typ +++ b/example/example.typ @@ -11,15 +11,6 @@ display: text(1.3em, $pi$) + " Lanningham", ), ), - about: [ - Example Labs is a fake company used for this template report. - ], - disclaimer: [ - This is an example, what do you need disclaimed? - ], - links: [ - #link("https://google.com", "Google") - ] ) = Audit Manifest @@ -77,8 +68,8 @@ Please find below the list of pinned software dependencies and files that were c #artifacts( ( ( - name: "abc", - type: "minting", + validator: "abc", + method: "mint", hash: "41429696a31fccad078830c182fec39d0df34ec5526df3420fdb4ac132f81843", ), ) @@ -141,7 +132,7 @@ This is a protocol that seeks to do a thing. address: "Order Contract", value: ( ada: "N", - INDY: "M", + INDY: "M + Z", LQ: "P" ), datum: ( @@ -167,7 +158,7 @@ This is a protocol that seeks to do a thing. reference: true, value: ( ada: 1000000, - WMT: "X" + WMT: "X + Y" ), datum: ( a: 123, @@ -195,7 +186,7 @@ This is a protocol that seeks to do a thing. address: "Order Contract", value: ( ada: "N", - INDY: "M", + INDY: "M + Y", LQ: "P", ), datum: ( diff --git a/template/audit.typ b/template/audit.typ index cb18932..bfc9562 100644 --- a/template/audit.typ +++ b/template/audit.typ @@ -54,13 +54,9 @@ date: none, repo: "", body, - disclaimer: [], - about: [], - links: [], ) = { // Set the document's basic properties. - let title = client + " - " + title - set document(author: authors.map(a => a.name), title: title) + set document(author: authors.map(a => a.name), title: client + " - " + title) set text(font: "Linux Libertine", lang: "en") set heading(numbering: "1.a.i -") set underline(offset: 0.3em) @@ -68,15 +64,20 @@ // Title page. // The page can contain a logo if you pass one with `logo: "logo.png"`. - set page(fill: gradient.linear(rgb("#aa00de"), rgb("#0a93ec"), dir: ttb)) + set page( + background: [ + #image("img/bg.jpg", width: 100%, height: 100%) + ] + ) text(1.1em, date, fill: white) v(1.2em, weak: true) - text(2em, weight: 700, title, fill: white) + text(2em, weight: 500, client, fill: white) + v(0em) + text(3em, weight: 700, title, fill: white) v(9.6fr) - align(right, image("img/sundae.svg", width: 50%)) - v(0.6fr) + v(4.8fr) // Author information. if authors.len() > 0 { @@ -94,14 +95,15 @@ v(2.4fr) pagebreak() - set page(numbering: "1", number-align: center, fill: none) + set page(numbering: "1", number-align: center, fill: none, background: []) // Table of contents. outline(depth: 2, indent: true, ) pagebreak() // Main body. - set par(justify: true) + set par(justify: true, leading: 1.5em) + body @@ -113,7 +115,17 @@ == Disclaimer #v(1em) - #disclaimer + This Smart Contract Security Audit Report ("Report") is provided on an "as is" basis, for informational purposes only, and should not be construed as investment advice or any other kind of advice on legal, financial, or other matters. The entities and individuals involved in preparing this Report ("Auditors") do not guarantee the accuracy, completeness, or usefulness of the information provided herein and shall not be held liable for any contents, errors, omissions, or inaccuracies in this Report or for any actions taken in reliance thereon. + + The Auditors make no claims, promises, or guarantees about the absolute security of the smart contracts audited and the underlying code. The findings, interpretations, and conclusions presented in this Report are based on the best efforts of the Auditors and reflect their professional judgment at the time of the audit. The blockchain and cryptocurrency landscape is rapidly evolving, and new vulnerabilities may emerge that were not identified or considered at the time of the audit. As such, this Report should not be considered as a comprehensive guarantee of the audited smart contracts' security. + + The Auditors disclaim, to the fullest extent permitted by law, any and all warranties, whether express or implied, including without limitation, warranties of merchantability, fitness for a particular purpose, and non-infringement. The Auditors shall not be liable for any direct, indirect, incidental, special, exemplary, or consequential damages (including, but not limited to, procurement of substitute goods or services; loss of use, data, or profits; or business interruption) however caused and on any theory of liability, whether in contract, strict liability, or tort (including negligence or otherwise) arising in any way out of the use of this Report, even if advised of the possibility of such damage. + + This Report is not exhaustive and is subject to change without notice. The Auditors reserve the right to update, modify, or revise this Report based on new information, subsequent developments, or further analysis. The Auditors encourage all interested parties to conduct their own independent research and due diligence when evaluating the security of smart contracts. + + By using or relying on this Report, you agree to indemnify and hold harmless the Auditors from any claim, demand, action, damage, loss, cost, or expense, including attorney fees, arising out of or relating to your use of or reliance on this Report. + + If you have any questions or require further clarification regarding this Report, please contact the contact\@sundaeswap.finance. #pagebreak() @@ -133,53 +145,53 @@ #set align(horizon + center) *Description* ], - cell(fill: severity_colors.Critical)[ + cell(fill: severity_colors.Critical, height: 7em)[ #set align(horizon + center) #set text(fill: severity_text_colors.Critical) Critical ], - cell()[ + cell(height: 7em)[ #set align(horizon) Critical issues highlight exploits, bugs, loss of funds, or other vulnerabilities that prevent the dApp from working as intended. These issues have no workaround. ], - cell(fill: severity_colors.Major, height: 5.1em)[ + cell(fill: severity_colors.Major, height: 6.5em)[ #set align(horizon + center) #set text(fill: severity_text_colors.Major) Major ], - cell(height: 5.1em)[ + cell(height: 6.5em)[ #set align(horizon) Major issues highlight exploits, bugs, or other vulnerabilities that cause unexpected transaction failures or may be used to trick general users of the dApp. dApps with Major issues may still be functional. ], - cell(fill: severity_colors.Minor)[ + cell(fill: severity_colors.Minor, height: 6em)[ #set align(horizon + center) #set text(fill: severity_text_colors.Minor) Minor ], - cell()[ + cell(height: 6em)[ #set align(horizon) Minor issues highlight edge cases where a user can purposefully use the dApp in a non-incentivized way and often lead to a disadvantage for the user. ], - cell(fill: severity_colors.Info, height: 6.4em)[ + cell(fill: severity_colors.Info, height: 10.4em)[ #set align(horizon + center) #set text(fill: severity_text_colors.Info) Info ], - cell(height: 6.4em)[ + cell(height: 10.4em)[ #set align(horizon) Info are not issues. These are just pieces of information that are beneficial to the dApp creator, or should be kept in mind for the off-chain code or end user. These are not necessarily acted on or have a resolution, they are logged for the completeness of the audit. ], - cell(fill: severity_colors.Witness, height: 6.4em)[ + cell(fill: severity_colors.Witness, height: 9.4em)[ #set align(horizon + center) #set text(fill: severity_text_colors.Witness) Witness ], - cell(height: 6.4em)[ + cell(height: 9.4em)[ #set align(horizon) Witness findings are affirmative findings, which covers bizarre corner cases we considered and found to be safe. Not all such cases are covered, but when something is considered interesting, or might be a common question, we try to include it. ], @@ -255,22 +267,23 @@ == About Us #v(1em) - #about + Sundae Labs stands at the forefront of innovation within the Cardano ecosystem, distinguished by its pioneering development of the first Automated Market Maker (AMM) Decentralized Exchange (DEX) on Cardano. As a trusted leader in blockchain technology, we offer a comprehensive suite of products and services designed to enhance the Cardano network's functionality and security. Our offerings include Sundae Rewards, Sundae Governance, Sundae Exchange, and Sundae Taste Test—an automated price discovery platform—all available on a Software as a Service (SaaS) basis. These solutions empower other high-profile projects within the ecosystem by providing them with turnkey rewards and governance capabilities, thereby fostering a more robust and scalable blockchain infrastructure. + + Beyond our product offerings, Sundae Labs is deeply committed to the advancement of the Cardano community and its underlying technology. We contribute significantly to research and development efforts aimed at improving Cardano's security and scalability. Our engagement with Input Output Global (IOG) initiatives, such as Voltaire, and participation in core technological discussions underscore our dedication to the Cardano ecosystem's growth. Additionally, our expertise extends to software development consulting services, including product design and development, and conducting security audits. Sundae Labs is not just a contributor but a vital partner in Cardano's journey towards achieving its full potential. + #v(1em) === Links #v(1em) - - #links ] } #let software_versions(items: ()) = { grid( - columns: (2fr, 1fr, 4fr), + columns: (1.5fr, 1.6fr, 2fr), gutter: 1pt, cell(fill: rgb("#E5E5E5"), height: 2.4em)[*Software*], cell(fill: rgb("#E5E5E5"), height: 2.4em)[*Version*], @@ -278,8 +291,11 @@ ..items.map( row => ( cell(height: 2.4em)[*#row.name*], - cell(height: 2.4em)[*#row.version*], - cell(height: 2.4em)[*#row.commit*], + cell(height: 2.4em)[ + #align(horizon, text(0.7em, raw(row.version)))], + cell(height: 2.4em)[ + #align(horizon, text(0.7em, raw(row.commit))) + ], ) ).flatten() ) @@ -329,13 +345,13 @@ grid( columns: column_sizes, gutter: 1pt, - cell(fill: rgb("#E5E5E5"), height: 2.4em)[*Name*], - cell(fill: rgb("#E5E5E5"), height: 2.4em)[*Type*], + cell(fill: rgb("#E5E5E5"), height: 2.4em)[*Validator*], + cell(fill: rgb("#E5E5E5"), height: 2.4em)[*Method*], cell(fill: rgb("#E5E5E5"), height: 2.4em)[*Hash (Blake2b-224)*], ..artifacts.map( row => ( - cell(height: 2.4em)[#text(0.8em, row.name)], - cell(height: 2.4em)[#text(0.8em, row.type)], + cell(height: 2.4em)[#text(0.8em, row.validator)], + cell(height: 2.4em)[#text(0.8em, row.method)], cell(height: 2.4em)[#text(0.7em, raw(row.hash))], ) ).flatten() @@ -446,11 +462,13 @@ #let start = (x: -18em, y: 1em) #for input in inputs { // Track how much is on the inputs - if "value" in input { - for (k, v) in input.value { - let existing = mint.at(k, default: (qty: 0, variables: (:))) - let updated = collapse_values(existing, v, -1) - mint.insert(k, updated) + if not input.at("reference", default: false) { + if "value" in input { + for (k, v) in input.value { + let existing = mint.at(k, default: (qty: 0, variables: (:))) + let updated = collapse_values(existing, v, -1) + mint.insert(k, updated) + } } } @@ -461,12 +479,15 @@ // Now connect this output to the transaction place(dx: start.x + 10.5em, dy: start.y + 0.84em)[ #path( - stroke: if input.at("reference", default: false) { blue } else { black }, + stroke: if input.at("reference", default: false) { aqua } else { black }, ((0em, 0em), (0em, 0em), (8em, 0em)), ((7.44em, (inputHeightEstimate / 1.25) - (inputHeight / 1.25)), (-4em, 0em)) ) ] place(dx: start.x + 10.26em, dy: start.y + 0.59em)[#circle(radius: 0.25em, fill: black)] + if input.at("redeemer", default: none) != none { + place(dx: start.x + 12.26em, dy: start.y - 0.2em)[#input.at("redeemer")] + } start = (x: start.x, y: start.y + tx_out.height) inputHeight += tx_out.height @@ -531,13 +552,13 @@ #v \ ] ] else [#v(-1em)] - let signatures = if signatures.len() > 0 [ + let sigs = if signatures.len() > 0 [ *Signatures:* \ #for signature in signatures [ - #signature ] ] else [#v(-1em)] - let certificates = if certificates.len() > 0 [ + let certs = if certificates.len() > 0 [ *Certificates:* #for certificate in certificates [ - #certificate @@ -549,19 +570,22 @@ `slot` #if "upper" in validRange [$<=$ #validRange.upper] ] else [#v(-1em)] + + let boxHeight = 100pt + if certificates.len() > 0 { 32pt * certificates.len() } else { 0pt } + if signatures.len() > 0 { 32pt * signatures.len() } else { 0pt } + let transaction = [ #set align(center) #rect( radius: 4pt, - height: calc.max(100pt, inputHeight + 16pt, outputHeight + 16pt), + height: calc.max(boxHeight, inputHeight + 16pt, outputHeight + 16pt), [ #pad(top: 1em, name) #v(1em) #set align(left) #stack(dir: ttb, spacing: 1em, mints, - signatures, - certificates, + sigs, + certs, valid_range, ) ] @@ -587,7 +611,6 @@ #let anchor(title) = label("anchor_" + title) #let defn(title, ..definition) = block( - spacing: 11.5pt, inset: 8pt, radius: 4pt, { @@ -638,6 +661,9 @@ } else if finding.resolution.at("comment", default: "") != "" { "Acknowledged" } + if finding.severity == "Witness" { + status = "Resolved" + } let idx = "00" + str(counters.at(finding.severity)) let id = prefix + "-" + severity_num.at(finding.severity) + idx.slice(-2) @@ -705,16 +731,17 @@ #set align(horizon + center) *#t* ]), - cell(height: auto)[ + cell(height: 2.5em)[ #set align(horizon + center) #finding.at("category", default: "None") ], - cell(height: auto)[ + cell(height: 2.5em)[ #set align(horizon + center) + #set text(0.7em) #finding.at("resolution", default: (commit: " ")).at("commit", default: " ") ], cell( - height: auto, + height: 2.5em, fill: severity_colors.at(finding.severity) )[ #set align(horizon + center) @@ -722,11 +749,11 @@ #finding.severity ], cell( - height: auto, + height: 2.5em, fill: status_colors.at(finding.status) )[ #set align(horizon + center) - #set text(fill: status_text_colors.at(finding.status)) + #set text(0.9em, fill: status_text_colors.at(finding.status)) #finding.status ] ) @@ -758,7 +785,12 @@ #let status = finding.at("status", default: none) #if status == "Resolved" { - "This issue was resolved as of commit " + raw(finding.resolution.commit) + "." + "This issue was resolved as of commit " + raw(finding.resolution.commit) + if finding.resolution.at("comment", default: "") != "" { + ", with the comment: " + finding.resolution.comment + "." + } else { + "." + } } else if status == "Acknowledged" { "This issue was acknowledge by the project team with the comment: " + finding.resolution.comment + "." } else { diff --git a/template/img/bg.jpg b/template/img/bg.jpg new file mode 100644 index 0000000..85a1ac7 Binary files /dev/null and b/template/img/bg.jpg differ diff --git a/template/img/bg.png b/template/img/bg.png new file mode 100644 index 0000000..85a1ac7 Binary files /dev/null and b/template/img/bg.png differ