diff --git a/README.md b/README.md index dbf9213..52e81b4 100644 --- a/README.md +++ b/README.md @@ -222,12 +222,16 @@ PRNG wrapper (typically not used directly). ## Dogfooding -daml-props has been validated against two production codebases: +daml-props has been validated against three production codebases: ### canton-network-token-standard (simple-token) Pure state-machine model of the CIP-056 transfer engine. 4 parties, 6 action types (self-transfer, direct transfer, two-step initiate/accept/reject/withdraw). 5 property tests, all passing. See `Examples/`. +### canton-token-template admin layer (AccessControl / Pausable / supply) + +Pure state-machine model of the OpenZeppelin [canton-token-template](https://github.com/OpenZeppelin/canton-token-template) minting-control path — `Rules_Mint`, `consumeMintAllowance`, and `assertNotPaused`. Models three admin-layer semantics as invariants over random action sequences (mint / pause / unpause): **pause** (no mint may increase supply while paused), **authorization** (only a party holding a minter capability can mint), and **conservation** (cumulative capped minting never exceeds the issued allowance — CIP supply invariant D3). Following the Amulet pattern, each semantic has a fixed executor that satisfies every invariant and a buggy executor that drops exactly one guard; the negative tests `test_adminAllowanceBypassDetected`, `test_adminPauseBypassDetected`, and `test_adminAuthBypassDetected` each catch the corresponding bypass with a minimal sequence. 5 property tests, all passing. See `DamlProps/Examples/AdminLayer/`. These rows mirror the admin-layer proofs A1–A8 in the companion [daml-verify](https://github.com/OpenZeppelin/daml-verify) project. + ### Splice (amulet) Pure model of `AmuletRules.daml` transfer engine with buggy and fixed executor variants. daml-props detected the H2 vulnerability through property-based testing: zero-input featured-app transfers mint reward coupons without burning any amulet. The `test_amuletH2Buggy` negative test catches this with a minimal 1-step sequence. See [SPLICE_FINDINGS.md](SPLICE_FINDINGS.md) and `DamlProps/Examples/Amulet/`. diff --git a/daml/DamlProps/Examples/AdminLayer/Model.daml b/daml/DamlProps/Examples/AdminLayer/Model.daml new file mode 100644 index 0000000..76fbe00 --- /dev/null +++ b/daml/DamlProps/Examples/AdminLayer/Model.daml @@ -0,0 +1,218 @@ +-- | Pure state-machine model of the OpenZeppelin canton-token-template admin layer. +-- Models the minting control path of `SimpleToken/Rules.daml` (`Rules_Mint`), +-- `SimpleToken/Admin/Capability.daml` (`consumeMintAllowance`, `requireRole`) +-- and the Pausable gate (`assertNotPaused`). +-- +-- Three admin-layer semantics are modeled as state-machine invariants: +-- * Pause — while paused, no mint may increase supply (origination control). +-- * Authorization — only a party holding a minter capability can mint. +-- * Conservation — cumulative minted by a capped minter never exceeds its +-- initial allowance (CIP supply invariant D3). +-- +-- Following the Amulet example's design, each semantic has a FIXED executor +-- (mirroring the real contract logic) and a BUGGY executor that drops exactly +-- one guard. The fixed executor satisfies every invariant for all action +-- sequences; each buggy executor is caught by the invariant whose guard it +-- dropped — demonstrating the properties have teeth. +-- +-- Design: invalid actions (paused, unauthorized, over-allowance, non-positive) +-- are no-ops (Right state unchanged), exactly as the real choices reject with +-- `assertMsg`/`ensure` without mutating the ledger. +module DamlProps.Examples.AdminLayer.Model where + +import DamlProps.Gen + +-- | A capped minter: party id, the allowance it was issued, and what remains. +-- Mirrors `RoleCapability` with `role = Minter` and `mintAllowance = Some _`. +data Minter = Minter with + mId : Int + initialAllowance : Decimal + remaining : Decimal + deriving (Show, Eq) + +-- | Admin-layer ledger state. +data AdminState = AdminState with + paused : Bool + minters : [Minter] + totalMinted : Decimal + -- ^ Cumulative amount minted across all minters. + mintedWhilePaused : Decimal + -- ^ Amount minted while paused. The real layer blocks this entirely, so a + -- correct model keeps it at 0.0; the pause invariant asserts exactly that. + unauthorizedMinted : Decimal + -- ^ Amount minted by parties holding no minter capability. A correct model + -- keeps it at 0.0; the authorization invariant asserts exactly that. + deriving (Show, Eq) + +-- | Build the initial state from a set of capped minters (unpaused, nothing minted). +mkInitialAdminState : [Minter] -> AdminState +mkInitialAdminState ms = AdminState with + paused = False + minters = ms + totalMinted = 0.0 + mintedWhilePaused = 0.0 + unauthorizedMinted = 0.0 + +-- | The admin-layer actions a caller may attempt. +data AdminAction + = Mint with maId : Int; maAmount : Decimal + | Pause + | Unpause + deriving (Show, Eq) + +-- | Sum of every minter's initial allowance — the global conservation bound. +initialAllowanceSum : AdminState -> Decimal +initialAllowanceSum state = + foldl (\acc m -> acc + m.initialAllowance) 0.0 state.minters + +-- | Total allowance consumed so far (initial minus remaining, summed). +consumedAllowance : AdminState -> Decimal +consumedAllowance state = + foldl (\acc m -> acc + (m.initialAllowance - m.remaining)) 0.0 state.minters + +-- | Look up a minter by party id. +findMinter : Int -> [Minter] -> Optional Minter +findMinter _ [] = None +findMinter mid (m :: rest) = if m.mId == mid then Some m else findMinter mid rest + +-- | Decrement a minter's remaining allowance by `amt`. +decrementMinter : Int -> Decimal -> [Minter] -> [Minter] +decrementMinter mid amt = map adjust + where adjust m = if m.mId == mid then m with remaining = m.remaining - amt else m + +-- | FIXED executor: mirrors `Rules_Mint` + `consumeMintAllowance` + `assertNotPaused`. +-- Enforces all three guards: pause, authorization, and the allowance cap. +executeAdminFixed : AdminState -> AdminAction -> Either Text AdminState +executeAdminFixed state Pause = Right state with paused = True +executeAdminFixed state Unpause = Right state with paused = False +executeAdminFixed state (Mint mid amt) + | state.paused = Right state -- assertNotPaused: blocked + | amt <= 0.0 = Right state -- eMintAmountNotPositive + | otherwise = case findMinter mid state.minters of + None -> Right state -- not a minter: requireRole fails + Some m -> + if amt > m.remaining + then Right state -- eMintAllowanceExceeded + else Right state with + minters = decrementMinter mid amt state.minters + totalMinted = state.totalMinted + amt + +-- | BUGGY executor — drops the pause guard. Mints succeed while paused and the +-- minted amount is recorded in `mintedWhilePaused`. Caught by `invNoMintWhilePaused`. +executeAdminNoPause : AdminState -> AdminAction -> Either Text AdminState +executeAdminNoPause state Pause = Right state with paused = True +executeAdminNoPause state Unpause = Right state with paused = False +executeAdminNoPause state (Mint mid amt) + | amt <= 0.0 = Right state + | otherwise = case findMinter mid state.minters of + None -> Right state + Some m -> + if amt > m.remaining + then Right state + else Right state with + minters = decrementMinter mid amt state.minters + totalMinted = state.totalMinted + amt + mintedWhilePaused = + state.mintedWhilePaused + (if state.paused then amt else 0.0) + +-- | BUGGY executor — drops the allowance cap. A capped minter can mint beyond +-- its allowance, driving `remaining` negative and `totalMinted` past the bound. +-- Caught by `invConservation` / `invNonNegativeAllowance`. +executeAdminNoAllowance : AdminState -> AdminAction -> Either Text AdminState +executeAdminNoAllowance state Pause = Right state with paused = True +executeAdminNoAllowance state Unpause = Right state with paused = False +executeAdminNoAllowance state (Mint mid amt) + | state.paused = Right state + | amt <= 0.0 = Right state + | otherwise = case findMinter mid state.minters of + None -> Right state + Some _ -> Right state with -- no cap check + minters = decrementMinter mid amt state.minters + totalMinted = state.totalMinted + amt + +-- | BUGGY executor — drops the authorization guard. A party with no minter +-- capability can mint, recorded in `unauthorizedMinted`. Caught by `invAuthorized`. +executeAdminNoAuth : AdminState -> AdminAction -> Either Text AdminState +executeAdminNoAuth state Pause = Right state with paused = True +executeAdminNoAuth state Unpause = Right state with paused = False +executeAdminNoAuth state (Mint mid amt) + | state.paused = Right state + | amt <= 0.0 = Right state + | otherwise = case findMinter mid state.minters of + Some m -> + if amt > m.remaining + then Right state + else Right state with + minters = decrementMinter mid amt state.minters + totalMinted = state.totalMinted + amt + None -> Right state with -- unauthorized mint admitted + totalMinted = state.totalMinted + amt + unauthorizedMinted = state.unauthorizedMinted + amt + +-- | INVARIANT (conservation, D3): cumulative minted never exceeds the sum of +-- initial allowances. +invConservation : AdminState -> Either Text () +invConservation state = + if state.totalMinted > initialAllowanceSum state + then Left ("totalMinted (" <> show state.totalMinted + <> ") exceeds initial allowance sum (" <> show (initialAllowanceSum state) <> ")") + else Right () + +-- | INVARIANT: no minter's remaining allowance is ever negative. +invNonNegativeAllowance : AdminState -> Either Text () +invNonNegativeAllowance state = + let negs = filter (\m -> m.remaining < 0.0) state.minters + in if null negs then Right () + else Left ("Negative remaining allowance: " <> show negs) + +-- | INVARIANT: minted supply is exactly the allowance consumed from minters +-- (no supply appears from outside the capped minter set). +invConsistency : AdminState -> Either Text () +invConsistency state = + if state.totalMinted == consumedAllowance state + then Right () + else Left ("totalMinted (" <> show state.totalMinted + <> ") /= consumed allowance (" <> show (consumedAllowance state) <> ")") + +-- | INVARIANT (pause): nothing was ever minted while paused. +invNoMintWhilePaused : AdminState -> Either Text () +invNoMintWhilePaused state = + if state.mintedWhilePaused > 0.0 + then Left ("Minted " <> show state.mintedWhilePaused <> " while paused") + else Right () + +-- | INVARIANT (authorization): nothing was ever minted by a non-minter party. +invAuthorized : AdminState -> Either Text () +invAuthorized state = + if state.unauthorizedMinted > 0.0 + then Left ("Unauthorized parties minted " <> show state.unauthorizedMinted) + else Right () + +-- | Combined invariant for the fixed model: all five hold simultaneously. +checkAdminInvariants : AdminState -> Either Text () +checkAdminInvariants state = + case invConservation state of + Left e -> Left e + Right () -> case invNonNegativeAllowance state of + Left e -> Left e + Right () -> case invConsistency state of + Left e -> Left e + Right () -> case invNoMintWhilePaused state of + Left e -> Left e + Right () -> invAuthorized state + +-- | Generate admin-layer actions. Party ids 1-4: some are minters, some are +-- not (stressing authorization); amounts span 0 and values above per-minter +-- allowance (stressing the cap); pause/unpause interleave (stressing the gate). +genAdminAction : Gen AdminAction +genAdminAction = genFrequency + [ (5, genMintAction) + , (2, genPure Pause) + , (2, genPure Unpause) + ] + +genMintAction : Gen AdminAction +genMintAction = + genBind (genInt 1 4) $ \mid -> + genBind (genDecimal 0.0 60.0) $ \amt -> + genPure (Mint mid amt) diff --git a/daml/DamlProps/Examples/AdminLayer/Properties.daml b/daml/DamlProps/Examples/AdminLayer/Properties.daml new file mode 100644 index 0000000..c743ff2 --- /dev/null +++ b/daml/DamlProps/Examples/AdminLayer/Properties.daml @@ -0,0 +1,90 @@ +-- | Property-based tests for the admin-layer model. +-- Demonstrates that the OpenZeppelin canton-token-template admin layer's three +-- minting-control semantics — pause, authorization, and allowance conservation — +-- hold for all action sequences, and that dropping any one guard is detected. +module DamlProps.Examples.AdminLayer.Properties where + +import Daml.Script +import DamlProps.Runner +import DamlProps.Examples.AdminLayer.Model + +-- | Initial state: two capped minters (parties 1 and 2) with allowances 100 and +-- 50. Parties 3 and 4 hold no capability — the action generator emits mints from +-- all four, so authorization and the allowance cap are both exercised. +testInitialState : AdminState +testInitialState = mkInitialAdminState + [ Minter 1 100.0 100.0 + , Minter 2 50.0 50.0 + ] + +-- | Runner config for admin-layer properties. +adConfig : Text -> RunnerConfig +adConfig name = (defaultRunnerConfig name) with + numTests = 100 + maxSequenceLength = 12 + +-- | Property A: the fixed model satisfies every admin-layer invariant. +-- For all action sequences, supply is conserved, allowances stay non-negative, +-- minted supply matches consumed allowance, and nothing is minted while paused +-- or by an unauthorized party. +test_adminInvariantsFixed : Script () +test_adminInvariantsFixed = script do + let result = runProp (adConfig "admin-invariants-fixed") genAdminAction + executeAdminFixed checkAdminInvariants testInitialState + case result of + AllPassed _ n -> debug ("admin-invariants-fixed: PASSED (" <> show n <> " tests)") + FoundFailure d -> error (formatDetail d) + +-- | Property B: conservation (D3) detects an allowance-cap bypass. +-- The no-allowance executor lets a capped minter mint past its allowance. +-- EXPECTS FoundFailure — a negative test demonstrating the property has teeth. +test_adminAllowanceBypassDetected : Script () +test_adminAllowanceBypassDetected = script do + let result = runProp (adConfig "admin-allowance-bypass") genAdminAction + executeAdminNoAllowance invConservation testInitialState + case result of + FoundFailure d -> do + debug "Allowance-cap bypass DETECTED by daml-props:" + debug (" Minimal sequence: " <> show (length d.fdMinimalSequence) <> " steps") + debug (" Invariant: " <> d.fdFailure.invariantError) + AllPassed _ _ -> + error "UNEXPECTED: allowance-cap bypass should have been detected" + +-- | Property C: the pause invariant detects a dropped pause guard. +-- The no-pause executor mints while paused. EXPECTS FoundFailure. +test_adminPauseBypassDetected : Script () +test_adminPauseBypassDetected = script do + let result = runProp (adConfig "admin-pause-bypass") genAdminAction + executeAdminNoPause invNoMintWhilePaused testInitialState + case result of + FoundFailure d -> do + debug "Pause bypass DETECTED by daml-props:" + debug (" Minimal sequence: " <> show (length d.fdMinimalSequence) <> " steps") + debug (" Invariant: " <> d.fdFailure.invariantError) + AllPassed _ _ -> + error "UNEXPECTED: pause bypass should have been detected" + +-- | Property D: the authorization invariant detects a dropped role guard. +-- The no-auth executor lets a party with no capability mint. EXPECTS FoundFailure. +test_adminAuthBypassDetected : Script () +test_adminAuthBypassDetected = script do + let result = runProp (adConfig "admin-auth-bypass") genAdminAction + executeAdminNoAuth invAuthorized testInitialState + case result of + FoundFailure d -> do + debug "Authorization bypass DETECTED by daml-props:" + debug (" Minimal sequence: " <> show (length d.fdMinimalSequence) <> " steps") + debug (" Invariant: " <> d.fdFailure.invariantError) + AllPassed _ _ -> + error "UNEXPECTED: authorization bypass should have been detected" + +-- | Property E: supply/allowance consistency holds under the fixed model. +-- Minted supply always equals the allowance consumed from the minter set — +-- there is no path that increases supply without drawing down an allowance. +test_adminConsistencyFixed : Script () +test_adminConsistencyFixed = script do + let result = runProp (adConfig "admin-consistency-fixed") genAdminAction + executeAdminFixed invConsistency testInitialState + case result of + AllPassed _ n -> debug ("admin-consistency-fixed: PASSED (" <> show n <> " tests)") + FoundFailure d -> error (formatDetail d)