Skip to content

Formalising Hydra

Jump to bottom
Arnaud Bailly edited this page May 14, 2022 · 3 revisions

Auditing & Formalising Hydra Protocol

Problem Statement

We want to:

  • Have a common language between researchers and engineers, in order to ensure the safety guarantees stated in the paper are actually provided by the implementation,
  • Help with the auditing and certification process from third-party,
  • Validate changes to the protocol introduced by the implementation or by new feature w.r.t. to the specification,
  • Provide strong evidence to users Hydra is actually safe and can be entrusted with their funds.

To this end, we are looking for a way to formalise the Hydra Head Protocol

Current Situation

Specification

In the original Head paper, Various desired properties are stated (in section 6.1) within an "experiment" setting describing the behaviour of the system in the presence of an adversary with some variations in the degree of corruption possible:

  • Consistency
  • (Conflict-Free) Liveness
  • Soundness
  • Completeness

Those properties link all three specifications presented above and in essence state the requirements the Head protocol needs to meet. Note that only the Close, Contest and Final transitions of the on-chain state are considered in the security "game".

The (Simple) Hydra Head protocol is specified in pseudocode, defining both:

  1. The Off-chain protocol producing consensus about the Snapshots (eg. UTxO) when the Head is open, Off-Chain Protocol Example
  2. The Client-to-Head Interaction protocol defining the effect external inputs have on the system, Client-to-Head Interaction Example
  3. The On-Chain Validation "smart contracts" mixing both validation of inputs (eg. redeemers) and production of new state (eg. datums). On-Chain Validation Example

The properties are then proven in subsection 6.4.

Implementation

The actual implementation of the Hydra Head protocol in this repository departs from the specification in the following:

  • The On-Chain validators are implemented in Plutus which requires validators to be boolean functions,
  • The on-chain state change is actually produced off-chain, by the entity crafting the transaction,
  • The implemented off-chain protocol is the so-called Coordinated Head Protocol which lets the leader be entirely responsible of which ones among the seen transactions shall be part of the produced snapshot,
    • This removes the need for confirming every single transaction hence removes the associated messages exchange in the protocol,
    • We implement an "optimisation" stated in a footnote on page 21 whereby all messages are broadcasted to all nodes and each node does the confirmation independently from all the individual messages, thus removing another message.

The code has an extensive test suite, comprising unit tests, integration and end-to-end tests, and property tests. For the on-chain validators we have implemented specific property tests that introduce Mutations to otherwise "healthy" transactions in order to test-drive and check each transaction's type behaviour. We are aware we are missing some intermediate property tests checking the state machine transition's logic, both for off-chain and on-chain protocol.

How?

We have been investigating various solutions, and discussed with other teams what promising avenues there could be to solve our problem.

Pseudo-code in Documentation

Quviq

  • Quviq develops the quickcheck-dynamic framework whose usage is detailed in the Plutus documentation. This framework leverages the Emulator infrastructure from plutus-apps and thus tailored to DApps that are based on the PAB and Contract monad which is not the case for Hydra (we talk directly to the chain)
  • Quviq has partnered with us to adapt the Contract monad to how we create and observe transactions

Ledger

We had a discussion with Jared and Tim from Ledger team, about the way they approached this problem

  • In the ledger, the specifications are defined in LaTeX then translated to Haskell as predicates and transition rules.
  • Those rules are then exercised with property tests that generate a complete chain trace (eg. sequence of transactions) and ensure the invariants are preserved
  • This process has its shortcomings as the researchers have no direct way to relate specifications to actual code

We discussed various other options to avoid the desynchronisation between formal specification and code problem:

  • OTT is a formalism that allows one to write a single specification and then generate various artefacts from it, including LaTeX and executable code (OCaml for example)
  • Tim shared a Haskell-centric approach he practiced on some example code whereby:
    1. The specification is written as a Haskell typeclass defining an interface,
    2. The typeclass embeds Property-returning functions like: 
      propZero:: (Show t,Eq t) => t -> Property
propZero x = (applyDiff @t) x (zero @t) === x
    3. Those properties can be tested against actual implementation by instantiating types: 
      testProperty "propZero Map" (propZero @(Map Int Int))

Djed

From a discussion with Jean-Frédéric Étienne and James Chapman

The Djed algorithmic stablecoin

Djed paper

Djed example property

Djed property

{-| Check stablecoin test objective #18 (https://input-output.atlassian.net/browse/DS-124)
(use after an unsuccessful buying reservecoin order with insufficient Ada for buying RC response)
-}
checkSTO18 ::
  (MonadError StableCoinTestError m, MonadWriter OrderTestLog m, MonadReader DeployedStablecoin m)
  => OrderSummary -- ^ Summary of the order that was executed
  -> SCBankState -- ^ Bank state before executing the order
  -> SCBankState -- ^ Bank state after executing the order
  -> m ()
checkSTO18
  OrderSummary{boPeggedCurrencyExchangeRate, boOrderTxOuts}
  oldState
  _newState
  = do
    StableCoinParams{scBaseFee, scDefaultReserveCoinPrice} <- asks (sqsStableCoinParams . dsQueryState)
    let
      buyRCPrice = max scDefaultReserveCoinPrice equityPrice
      equity              = R.fromInteger (scReserve oldState) P.- min (R.fromInteger (scReserve oldState)) (boPeggedCurrencyExchangeRate P.* R.fromInteger (scN_SC oldState))
      equityPrice         =
        if (scN_RC oldState > 0)
          then equity P.* R.recip (R.fromInteger (scN_RC oldState))
          else P.zero
      adaFromOrderUtxo (SCOrder{scAction=BuyRC _ totalBuyingPrice}, _, _, _) = Just totalBuyingPrice
      adaFromOrderUtxo _ = Nothing

    case boOrderTxOuts of
      [adaFromOrderUtxo -> Just a] | R.fromInteger a P.* (R.recip $ buyRCPrice P.* (P.one P.+ scBaseFee)) < P.one -> pure ()
                                   | otherwise -> throwError (PropertyFailed "STO18: Deposited Ada for buying order / ( BuyRCPrice * (1 + baseFee) ) < 1 ")
      _ -> throwError $ TestFailed "Expected one BuyRC order txout"

    logTestObjective STO18
Clone this wiki locally