From 1c1cc0d0afd969e436fba31f4c9818cacdf4e1d6 Mon Sep 17 00:00:00 2001 From: Gregory Gerasev Date: Tue, 19 Mar 2024 00:38:54 +0700 Subject: [PATCH] WIP --- docs/goals_and_soa.md | 97 +++++++++++++++++++++++++++++++++---------- 1 file changed, 75 insertions(+), 22 deletions(-) diff --git a/docs/goals_and_soa.md b/docs/goals_and_soa.md index 320f4d3..f9f0499 100644 --- a/docs/goals_and_soa.md +++ b/docs/goals_and_soa.md @@ -48,7 +48,7 @@ what we use to demonstrate problems in following: * Fracada * JPG Vesting Contract * Indigo Protocol -* DApp project we participate, audited or otherwise know it codebase +* DApp projects we participated, audited or otherwise know their codebase * Hydra Auction * POCRE * CNS @@ -56,8 +56,6 @@ what we use to demonstrate problems in following: * Plutonomicon patterns * plutus-usecases -@todo #3: Add more links to specific bugs and code size blowups in existing DApps. - ## On-chain correctness ### Known common vulnerabilities @@ -77,27 +75,36 @@ taking that burden from developers and auditors. Those problems are similar to previous in that they tend to arise in naive Plutus implementations, -if developer was did not make measures to prevent them. +if developer was did not take measures to prevent them. + +Plutus forces developers to write TxIn/TxOut constraints from scratch, +leading by subtle bugs from copy-pasting logic or +trying to optimize them by hand. + +Examples: + +* Security bug in MinSwap audit - 2.2.1.3 Unauthorized Hijacking of Pools Funds +* Non-security bug in MinSwap audit - 2.2.2.2 Batcher Is Not Allowed to Apply Their Own Order + +Such constraints naturally lead to conditions +for which more performant implementation should +omit some constraints always following from others. +Such kind of manual SMT solving exercises are +known source for security bugs and complicated code. -Almost all transactions which require fungible tokens as input, +One of important cases is maintaining invariants of token value. +TODO - add explanation + +Most of transactions which require fungible tokens as input, should not depend from exact UTxO coin-change distribution. Failure to expect that leads to prohibition of correct transactions. -On other side too broad constraint might lead to -fund stealing. +On other side too broad constraint might lead to fund stealing. Example of bugs: * https://github.com/mlabs-haskell/hydra-auction/issues/146 -Another important case is maintaining invariants -of token value or immutable UTxOs. -Such kind of constraints naturally lead to script -for which more performant implementation should -eliminate some constraint following from others. -Such kind of manual SMT solving exercises are -known source for security bugs and complicated code. - Making Plutus contract invariant to `TxIn` ordering and participation in multi-script scenarios lead to similar kind of complications. @@ -106,6 +113,9 @@ Examples: * Non-security bug: https://github.com/mlabs-haskell/hydra-auction/issues/129 * Non-security bug: https://github.com/mlabs-haskell/hydra-auction/commit/8152720c43732f8fb74181b7509de503b8371997 +* Non-intentionally under-specified behavior in MinSwap audit: + * `2.2.2.1 Batchers Can Choose Batching Order` + * Triggered by `2.2.4.1 "Reliance on Indexes Into ScriptContexts' txInputs and txOutputs"` * Multiple kind of code complication was observed in CNS audit. ### Single script safety and liveliness @@ -169,6 +179,19 @@ Our script stages abstraction cover all those kind of problems. * @todo #3: document problems with slots in Plutus/Cardano API * https://github.com/mlabs-haskell/hydra-auction/issues/236 +## Matching off-chain logic + +Problem of duplicating logic between on- and off-chain is twofold. +Testing is essentially offchain, thus, you may miss that your onchain code +is not actually enforcing part of Tx provided in tests. + +CEM Script is constructing Tx for submission from same specification, +which is used for onchain script. Thus it is much harder to miss constraint +to be checked. + +Examples: + +* MinSwap audit - 2.2.1.2 LP Tokens Can Be Duplicated ## Logic duplication and spec subtleness @@ -195,15 +218,38 @@ is much less obvious to implement, and out of scope of current Catalyst project, but it is very much possible feature as well. -### On-/Off-chain and spec code duplication +Examples of diagrams in DApp specifications: + +* ... +* ... +* ... + +### On-/Off-chain and spec logic duplication + +Writing on-chain contracts manually encodes non-deterministic state machine, +which cannot be used for off-chain transaction construction. +Thus developer need to write them again in different style in off-chain code, +which is tedious and error prone. + +They should add checks for all errors possible, +like coins being available and correct script states being present, +to prevent cryptic errors and provide retrying strategies +for possible utxo changes. + +Our project encodes scripts in deterministic machine, +containing enough information to construct transaction automatically. +This also gives a way to check for potential on/off-chain logic differences +semi-automatically. + +Example: +* MinSwap Audit - 2.2.4.3 Large Refactoring Opportunities +* `availableVestings` - пример чего-то подобного для SimpleAuction @todo #3: Add more off-chain code duplication examples from existing PABs. Include problems with querying coin-selection, tests, retrying and errors. -### Correct off-chain Tx construction logic +Timing ... -A lot of on-chain problems, like timing and coin change issues -have their counterpart on Tx submission side. ### Common backend features @@ -274,12 +320,19 @@ and multiple commiters schemes (used in `hydra`). ### Atlas -Atlas provides (emulate-everything) and overall more humane DX -on top of cardano-api. But it has no feature related to goals +Atlas provides more humane DX on top of cardano-api. +But it has no features related to goals (synced-by-construction), (secure-by-construction) and (declarative-spec). +(emulate-everything) is planned, but is not implemented currently. + +Atlas includes connectors to Blockfrost and other backends, +which our project lacks. + +Also our project has slight differences in API design decisions. +Our monad interfaces is meant to be slightly more modular. +We use much less custom type wrappers, resorting to Plutus types where possible. -@todo #3: Add more specifics on Atlas to docs. ## Testing tools