feat: threat model#4
Open
bogdan-manole wants to merge 27 commits intochore-testing-interface-pingpongfrom
Open
feat: threat model#4bogdan-manole wants to merge 27 commits intochore-testing-interface-pingpongfrom
bogdan-manole wants to merge 27 commits intochore-testing-interface-pingpongfrom
Conversation
bogdan-manole
force-pushed
the
feat/threat-model
branch
2 times, most recently
from
da672c2 to
75ba31c
Compare
bogdan-manole
force-pushed
the
feat/coverage
branch
from
c80ec6c to
d992b35
Compare
bogdan-manole
force-pushed
the
feat/threat-model
branch
from
028900d to
d7b37d2
Compare
Base automatically changed from
feat/coverage
to
chore-testing-interface-pingpong
January 19, 2026 15:40
bogdan-manole
force-pushed
the
feat/threat-model
branch
from
843ea05 to
f7495be
Compare
- Change Era type from BabbageEra to ConwayEra - change TxBody patterns: BabbageTxBody -> ConwayTxBody - change field names: btbInputs -> ctbSpendInputs, btbOutputs -> ctbOutputs, etc. - change script witnesses: PlutusScriptV2InBabbage -> PlutusScriptV2InConway - change Plutus purposes: AlonzoSpending -> ConwaySpending (+ Voting, Proposing) - Fix BuiltinByteString conversion in DoubleSatisfaction
…terface - Move ThreatModel modules from convex-mockchain to new namespace Convex.ThreatModel in testing-interface - Update convex-testing-interface.cabal with new modules and dependencies - Update test imports to use new namespace
…nerable/secure PingPong demo - Add UnprotectedScriptOutput threat model that detects scripts not validating output addresses - Split PingPong into secure (validates output address) and vulnerable (only checks datum) variants - Add property tests: vulnerable version fails threat model, secure version passes - Demonstrates how threat models detect vulnerabilities and validate fixes
…le/secure Bounty demo - Add Bounty contract: secure version requires unique TxOutRef datum per output - Add vulnerable Bounty: only checks 'output to beneficiary exists' (double satisfaction) - Fix DoubleSatisfaction threat model to use removeOutput instead of changeValueOf (fixes handling of Ada-only outputs that would become invalid 0-value outputs) - Add property tests demonstrating vulnerable script fails, secure script passes
- Add threatModels method to TestingInterface class with default empty list - Capture UTxO before each action and get last transaction for threat model evaluation - Run threat models against the last transaction after all actions complete - Add unprotectedScriptOutput threat model to PingPongModel as demonstration - Add lens dependency for optics
- for this we run the threatModel inside the MockchainT modan - add ThreatModel.Cardano.Api utils - modify the TestingInterface to use this
- Fix inline datum handling: TxOutDatumInline should not add datums to witness set (fixes NotAllowedSupplementalDatums error) - Add recalculateScriptIntegrityHash to recompute PPViewHash after transaction modifications (fixes PPViewHashesDontMatch error) - All 4 threat model tests now pass correctly
bogdan-manole
force-pushed
the
feat/threat-model
branch
from
f7495be to
a54afc2
Compare
… testing-interface - Move PingPong, Bounty, Sample validators and specs to testing-interface - Keep MatchingIndex in coin-selection (tests coin-selection specific functionality) - Add test suite configuration to testing-interface cabal file - Clean up unused imports and fix compilation warnings - Remove convex-testing-interface dependency from coin-selection tests
bogdan-manole
force-pushed
the
feat/threat-model
branch
from
a54afc2 to
86fd753
Compare
- Add largeDataAttack threat model detecting permissive FromData/UnsafeFromData parsers - Make PingPong.hs secure with strict UnsafeFromData (rejects extra fields) - Make Vulnerable.hs self-contained with unstableMakeIsData (vulnerable to both attacks) - Rename pingPongVulnerable* to vulnerablePingPong* - Move test groups to PingPongSpec.hs and BountySpec.hs
bogdan-manole
force-pushed
the
feat/threat-model
branch
from
5916cf4 to
2e24436
Compare
- Add LargeValue.hs module with largeValueAttack and largeValueAttackWith
- Add minting infrastructure to TxModifier (AddPlutusScriptMint, alwaysSucceedsMintingPolicy)
- Add Value validation to secure PingPong script (prevents junk token injection)
- Add propPingPongVulnerableToLargeValue test
- Increase maxTxSize limit to 30000 for larger secure script
- Update documentation for both secure and vulnerable PingPong scripts
… validations - Extract coverage from validation errors using CovLoc format parser - Accumulate coverage in runThreatModelM via modifyMockChainState - Add PingPongCoverageSpec with tests for uncovered code paths: - Line 141: invalid datum index - Line 205: invalid script purpose - Line 217: findOwnInput empty list (ledger-guarded) - Line 220: findOwnInput recursive case - Line 247: NoOutputDatum error - Lines 248-250: OutputDatumHash paths - Fix typo: tryExtractCovverageData -> tryExtractCoverageData
…tput - Add withCoverage helper to encapsulate IORef/catch boilerplate for coverage collection - Add CoverageConfig type with coverageIndices and coverageReport fields - Add printCoverageReport, writeCoverageReport, silentCoverageReport for Pretty output - Add printCoverageJSON, writeCoverageJSON and pretty variants for compact JSON output
…stead of Property - Change propRunActionsWithOptions to return TestTree with a 'Positive tests' sub-test - Add tasty and tasty-quickcheck as library dependencies - Re-export TestTree for consumer convenience - Update PingPongSpec call site to use new signature - Prepares test group structure for future counterexample tests
…n detection - Add InvalidActions type (valid prefix + one invalid action) - Add Arbitrary instance that generates actions violating preconditions - Add negativeTest property: runs valid prefix, attempts invalid action, expects failure - Collect coverage data from both success and failure paths - Extract suchThatMaybe to top-level helper for reuse
…ostic testing - Add aiken-contracts-example/ with two Aiken validators: check_answer (datum+redeemer==43) and ping_pong (secure stateful validator with continuation output + value equality checks) - Add AikenSpec.hs: 4 unit tests for check_answer using Aiken blueprint loading - Add AikenPingPongSpec.hs: TestingInterface property test, and threat model test proving the Aiken validator resists output redirect attacks - Demonstrates that BuildTx, MockChain, and TestingInterface work identically with Aiken-compiled Plutus scripts as with PlutusTx/Plinth scripts - Aiken enum types (Constr 0/1/2) are wire-compatible with PlutusTx ToData instances
…datum bloat threat model - Port Cardano CTF tipjar validator to Aiken stdlib v3.0.0 (preserves datum bloat DoS vulnerability) - Add Convex.ThreatModel.DatumBloat module with datumListBloatAttack and datumByteBloatAttack - Add AikenTipJarSpec with TestingInterface instance, unit tests, and standalone threat model tests - Threat model results: unprotectedScriptOutput and largeDataAttack pass (tipjar resists), largeValueAttack and datumByteBloat detect vulnerabilities (expectFailure) - Add griefing attack test proving huge message prevents future tips but owner can still claim
- Add 15 CTF validators from cardano-ctf repo (original series + bank series) - Original series: hello_world, sell_nft, vesting, tipjar_v2, multisig_treasury, purchase_offer, king_of_cardano, lending, multisig_treasury_v2/v3 - Bank series: bank_00 through bank_03 (bank + account validators each) - Add shared bank types library (lib/ctf/bank_types.ak) - Update compiled blueprint with all 44 validator entries - All contracts preserve intentional CTF vulnerabilities for testing
- Add TestingInterface specs for sell_nft (double satisfaction), vesting (time bound manipulation), tipjar_v2 (datum bloat), and hello_world - Add new TimeBoundManipulation threat model for detecting wrong validity range checks (upper_bound vs lower_bound) - sell_nft proven vulnerable to doubleSatisfaction - vesting proven vulnerable to timeBoundManipulation - tipjar_v2 proven still vulnerable to datumByteBloat and largeValue despite partial value-preservation patch
…vulnerabilities - Add TestingInterface specs for multisig_treasury, multisig_v2, multisig_v3, purchase_offer, king_of_cardano, lending, and bank_00 through bank_03 - Each spec includes manual exploit tests proving the vulnerability exists plus property-based threat model tests for automated detection - Register all new test suites in Spec.hs (77+ tests total) - Update blueprint with all compiled validators
- Add signatoryRemoval, negativeIntegerAttack, duplicateListEntryAttack, valueUnderpaymentAttack, tokenForgeryAttack, inputDuplication, selfReferenceInjection, redeemerAssetSubstitution, mutualExclusionAttack - Extend TxModifier with removeRequiredSigner and AddPlutusScriptMintV3 - Add updateExecutionUnits for auto-recalculating script execution budgets - Add getTxRequiredSigners to ThreatModel monad - Wire all threat models into CTF test specs with expectFailure tests - Replace fail with new failPrecondition function across all threat models
…ativeTesting option
- Add disableNegativeTesting
- Broaden arbitraryAction in 12 Aiken specs to enable negative testing (PingPong pattern)
- Keep init-like actions tight (guard matches precondition exactly), broaden only spending actions
- Fix witness handling in MultisigTreasury V1/V2 perform functions
- Fix MintValidationToken precondition in MultisigV3 (independent of script state)
- Add tasty-expected-failure dependency to convex-testing-interface
- Mark 4 CTF contracts with known vulnerabilities as IGNORED for negative testing :
- bank_00 (negative balance)
- king_of_cardano (re-close)
- multisig_v2 (forgery)
- multisig_v3 (replay)
…parate test nodes - Add Named GADT constructor to ThreatModel for intrinsic naming - Add ThreatModelOutcome (TMPassed/TMFailed/TMSkipped/TMError) and runThreatModelCheck - Restructure test tree: IORef two-phase with sequentialTestGroup, each threat model as separate Tasty node - Add expectedVulnerabilities typeclass field with inverted pass/fail semantics - Add runThreatModelMQuiet for suppressed standalone vulnerability tests - Add updateRedeemer to avoid orphaned supplemental datums for inline-datum inputs - Fix ChangeScriptInput to not add inline datums to TxDats (NotAllowedSupplementalDatums fix) - Fix TxModifier fromJust crash with safe datum extraction fallback - Early-stop threat models on first TMFailed (threatModels only, not expectedVulnerabilities) - Limit assertFailure output to first failure message - Separate positiveTest params for threatModels vs expectedVulnerabilities - Rewrite redeemerAssetSubstitution with Phase 1-valid swappable-pair approach - Add Named wrappers to all 16 built-in threat models - Migrate 10 Aiken CTF specs from standalone expectFailure to expectedVulnerabilities - Restore 3 PingPong standalone vulnerable-script tests with runThreatModelMQuiet
- Fix inputDuplication to extract script from tx witness set and use addPlutusScriptInput instead of addReferenceScriptInput, which created UTxOs with ReferenceScriptNone causing false-negative validation failures - Add attacker output to inputDuplication for value conservation - Add AddPlutusScriptInputV3 constructor to TxModifier for PlutusV3 script support - Widen LendingModel preconditions to match actual contract domain: LendAction accepts any existing loan, RepayAction accepts any funded loan - Update nextState/perform to handle re-funding and double-repay cases - Add mixed-state arbitraryAction branch so LendAction can be the last tx
…nventions - merge runThreatModelMQuiet & runThreatModelM common functionalities - Rename rebalanceAndSign/tryRebalanceAndSign to rebalanceAndSignM/rebalanceAndSign (same for adjustChangeOutput) - Remove unused imports, pragmas, and redundant constraints - Fix incomplete pattern match in extractData, add ype signatures to local bindings
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.