Protocol - Audit

[Renegatto]

SNet Protocol

Definitions

Owners agree with the tx - means that the transaction is signed by at least the threshold number of pubkeys associated with the list recorded in the state thread datum

Incorrect protocol state - a state in which some protocol requirements can be violated.

Well-formed state thread UTxO for protocol instance $p$ - a UTxO thread $p$ that contains a small amount of Lovelace, (close to min Ada per UTxO) and an always unique single NFT state thread token $nft\ p$, such that:

• the UpgradeableOwners validator $uoValidator\ p$ is able to distinct $nft\ p$ from any other token $nft\ p’$ of another protocol instance $p’$
• UTxO $thread\ p$ has datum Constr 0 [owners,minOwnersThreshold], where
  • $\text{owners} : \text{BuiltinList PubKeyHash}$, contains no duplicates and has length no less than $minOwnersThreshold$
  • $(\text{minOwnersThreshold} : \text{Integer}) \in [2; \text{length owners} - 1]$

protocol instance $p$ is properly initialized iff the well-formed state thread UTxO $thread\ p$ is locked on UpgradeableOwners validator $uoValidator\ p$ address.

Prerequisites

All the requirements listed are only applicable to a properly initialized protocol instance.

Requirements

Legend:

• ✅ Confirmed

• ⏹ Dependency violated

  Means that some other requirement is violated, and only this leads to this requirement being violated too.

• ❌ Directly violated

⏹ EC0: Protocol must not stale

Staling is incorrect state, so given the precondition,

Require:

• ⏹ EC1

  ⏹ EC1: Protocol can not be put from correct into incorrect state

  Require:

• ✅ According to EUO6 all protocol state is contained in a state thread, therefore
• ⏹ EUO2

R0: After creation, there is always single NFT token in existence.

This is ambiguous and partially follows from ⏹EUO0.

⏹ R1: The token is held at UpgradeableOwners script.

Require:

• ⏹ EUO0

  R2: Initialization creates a correct datum.

  This is unrelated to onchain and can be considered a prerequsite.

❌ UO0. The minimum threshold is no greater than the number of owners and greater than 1.

Require either:

• ❌ Correct validator checks
• ❌ UO4

✅ UO1. Owners can set a new threshold number and change the set of owners in a single transaction.

IF they can do it, they can do it in a single Tx as well.

Follows from the code.

⏹ UO2. It is impossible to stall the protocol by creating an unspendable output.

The only UTxO required for the protocol functioning is the state thread UTxO. So Require:

• ❌ EUO4

⏹ UO3. As a token holder I can freely burn my tokens.

Require:

• ⏹ EC0
• ✅ It indeed allows free burning tokens of the same asset. The MP restrictions do not forbid burning any amount of its tokens of any token name.

  ❌ UO4. List of owners must not have duplicates

  Directly falsified by #9

  ✅ UO5. Token minting transactions do not change owners and threshold.

  It is indeed checked. The implementation is ineffective though.

  ⏹ UO7. Can mint if agreed

  Require:

• ⏹ EC0
• ❌ EUO3
• ✅ It follows from the codebase, that can mint as long as doesn’t violate other requirements

  ⏹ UO8. Can change params if agreed

  Require:

• ⏹ EC0
• ❌ EUO3
• It follows from the codebase, that can change as long as doesn’t violate other requirements

⏹ EUO0: State thread UTxO is always well-formed

Require:

• ⏹ EUO1.

  ⏹ EUO1: If input state thread UTxO is well-formed, output state thread UTxO is also well-formed

  According to the codebase it holds up to ❌UO4

  ⏹ EUO2: No Tx spending well-formed state thread UTxO can put protocol into incorrect state

  Require:

• ⏹ EUO1

Reasoning:

According to EUO6, put protocol into incorrect state means to produce state thread UTxO on which protocol violate some requirements. Therefore EUO1.

❌ EUO3: Tx that spend state thread UTxO require owners agreement

Require either:

• ❌ UO4
• ❌ Correct validator checks

❔EUO4: Well-formed state thread UTxO is always spendable

According to the well-formed state thread UTxO it can be made unspendable only by exceeding limits on its datum size.

Require:

• ❌ UO0
• ❌ EUO5
• ❔Positive benchmark result

Reasoning:

• According to UO0 minOwnersThreshold is bound to the length of the owners, so it is only unsafe if owners field is unsafe.
• According to EUO5 owners list can become of size $n$ for at least $n$ owner additions, i.e. $n$ transactions.
• It can be considered safe if the number of Txs that allows owners to grow up to the point to make state thread UTxO unspendable can be considered too big to be achieved accidentally, and too big to be feasible as an intentional attack on the protocol.

• Is it that big?

  To answer this benchmarking must be done.

  ❌ EUO5: Can add or remove at most one owner per Tx

  Require:

• ✅ Can add at most one owner per Tx

  It is implemented in a way that owner addition Cons the new owner to the list, so it is True.

• ❌ Can remove at most one owner per Tx

  Owner removal filter the list of owners for inequality against the removing owner, so

  Require either:

  • ❌ UO4
  • ❌ Correct validator checks

    ✅ EUO6: Protocol state is only its state thread UTxO state

    The only validated onchain protocol entities are State thread UTxO and protocol tokens. This is why only them could carry the protocol state.

So require:

• ✅ Protocol tokens are not the part of the protocol state
  • Protocol tokens are not tracked at all by the validator, so they can not be considered state.
  • Token MP do not make any decisions based on the input or output tokens rather than forbidding their burning or minting. So this can not be considered a decision based on a state.

• ✅ State thread UTxO is a part of the protocol state

  State Thread UTxO indeed affects validator decision making, and indeed carries changes from one validator Tx to another.

✅ EUO7: No Tx spending non-protocol UO UTxO can put protocol into incorrect state

Require:

• ✅ Holds for spending against MultiSigRedeemer

  This redeemer cause check that the UTxO being spent is indeed state thread token.

  So it is not possible to spend non-protocol UTxO using this redeemer.

• ✅ Holds for spending against any other redeemer

  Currently there is no wildcard redeemer, so another redeemer would cause validation failure. So state change this way is impossible.

  ❌ EUO8: Can freely spend non-protocol UTxO

  Require either:

• ❌ Can spend against redeemer Constr n _, $n \in [0;2]$

  No, validator enforces UTxO being spent to be state thread UTxO, when this redeemer is used.

• ❌ Can spend against another redeemer

  No, validator is implemented in a way it always case split by the redeemer. So using another redeemer causes evaluation failure.

  However, implementing this is trivial and may lead to almost no overhead.