Dev multisig wallet properties #89
Open
Conversation
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
added 3 commits
November 28, 2025 08:19
Implements 30+ property tests for Uniswap V2 constant product (x*y=k) automated
market makers. These properties cover liquidity provision, removal, swaps, and
critical security invariants.
Properties Implemented:
Basic Properties (8 properties):
- Adding liquidity increases K, total supply, reserves, and user LP balance
- First mint locks MINIMUM_LIQUIDITY (1000 tokens) to prevent first depositor attack
- Total supply maintained above MINIMUM_LIQUIDITY after initialization
Remove Liquidity Properties (7 properties):
- Removing liquidity decreases K, total supply, reserves, and user LP balance
- Burn returns proportional amounts of both tokens
- Total supply never falls below MINIMUM_LIQUIDITY
Swap Properties (8 properties):
- Swapping does not decrease K (increases due to 0.3% fees)
- Price moves in correct direction based on swap
- LP token balances unaffected by swaps
- Zero amount swaps have no effect
- Insufficient liquidity and invalid swaps fail
Invariant Properties (10 properties):
- K never decreases except through liquidity removal (core invariant)
- Reserves never zero after initialization
- Total supply equals sum of balances
- MINIMUM_LIQUIDITY locked prevents first depositor attacks
- Donation attack resistance: direct transfers don't inflate LP value
- No free money: mint then immediate burn not profitable
- Price accumulator monotonically increasing (TWAP oracle)
- LP tokens represent proportional ownership
- Flash swaps must restore K (plus fees)
Files Added:
Property Contracts:
- contracts/UniswapV2/internal/properties/UniswapV2BasicProperties.sol
- contracts/UniswapV2/internal/properties/UniswapV2RemoveLiquidityProperties.sol
- contracts/UniswapV2/internal/properties/UniswapV2SwapProperties.sol
- contracts/UniswapV2/internal/properties/UniswapV2InvariantProperties.sol
Utilities:
- contracts/UniswapV2/util/IUniswapV2Pair.sol (minimal interface)
- contracts/UniswapV2/internal/util/UniswapV2TestBase.sol (base contract)
Test Harness:
- tests/UniswapV2/foundry/src/SimplePair.sol (example implementation)
- tests/UniswapV2/foundry/src/MockERC20.sol (test token)
- tests/UniswapV2/foundry/test/CryticUniswapV2Test.sol (complete harness)
Updated:
- CLAUDE.md (added UniswapV2 to project overview)
Security Properties Coverage:
First Depositor Attack Protection:
The MINIMUM_LIQUIDITY mechanism prevents share price manipulation on first
deposit by burning 1000 LP tokens. Properties verify this protection is
maintained throughout the pool lifecycle.
Donation Attack Resistance:
Properties verify that direct token transfers (donations) to the pair do not
inflate LP token value. Similar to ERC4626 inflation attacks and Euler donation
attack pattern.
Constant Product Invariant (x*y=k):
Core properties ensure K never decreases except through liquidity removal. Swaps
must increase K due to 0.3% fees. Violations indicate value leakage or fee bypass.
No Free Money:
Properties verify mint-burn cycles cannot be profitable, catching rounding errors
and integer overflow/underflow issues.
Flash Swap Safety:
Properties ensure flash swaps (borrow-repay in single transaction) restore K
plus fees, preventing free token extraction.
Testing Approach:
These properties support internal testing mode (test contract inherits from pair
implementation). External testing mode can be added following the same pattern
as ERC20/ERC721 properties.
Example Usage:
contract MyPairTest is
MyUniswapV2Pair,
CryticUniswapV2BasicProperties,
CryticUniswapV2InvariantProperties
{
// Run with: echidna . --contract MyPairTest --config echidna-config.yaml
}
Resolves crytic#4
- Removed custom MockERC20.sol (not following repo patterns) - Updated SimplePair to use minimal IERC20 interface - Moved TestToken into test harness (matches ERC20/ERC4626 test patterns) - SimplePair now works with any ERC20-compatible token
Implements comprehensive property tests for MultiSig wallet contracts following issue crytic#32. This PR adds 27 properties across 4 categories with support for both internal and external testing modes. **Added Files (13 files):** Internal Testing Mode: - contracts/MultiSig/internal/util/MultiSigTestBase.sol - contracts/MultiSig/internal/properties/MultiSigBasicProperties.sol (8 properties) - contracts/MultiSig/internal/properties/MultiSigThresholdProperties.sol (6 properties) - contracts/MultiSig/internal/properties/MultiSigSignatureProperties.sol (7 properties) - contracts/MultiSig/internal/properties/MultiSigNonceProperties.sol (6 properties) - contracts/MultiSig/internal/echidna.config.yaml External Testing Mode: - contracts/MultiSig/external/util/IMultiSigMock.sol - contracts/MultiSig/external/util/MultiSigExternalTestBase.sol - contracts/MultiSig/external/properties/MultiSigExternalBasicProperties.sol (8 properties) - contracts/MultiSig/external/properties/MultiSigExternalThresholdProperties.sol (6 properties) - contracts/MultiSig/external/properties/MultiSigExternalSignatureProperties.sol (7 properties) - contracts/MultiSig/external/properties/MultiSigExternalNonceProperties.sol (6 properties) - contracts/MultiSig/external/echidna.config.yaml **Property Coverage (27 total):** Basic Properties (MULTISIG-BASIC-001 to 008): - Owner authorization validation - Threshold bounds (0 < threshold ≤ owner count) - Zero address protection - Owner list consistency - Duplicate owner prevention - Executed transaction immutability Threshold Properties (MULTISIG-THRESHOLD-001 to 006): - Execution requires threshold approvals (addresses crytic#32) - Threshold validation and bounds checking - Approval count constraints Signature/Approval Properties (MULTISIG-SIGNATURE-001 to 007): - Signature reuse prevention (addresses crytic#32) - Owner-only approval validation - Approval counting accuracy - Zero address protection Nonce Properties (MULTISIG-NONCE-001 to 006): - Strictly monotonic nonce increase (addresses crytic#32) - Single-use nonce enforcement (addresses crytic#32) - Sequential execution validation - Replay protection **Key Features:** - Flexible design works with both ECDSA signatures and approval mappings - Full NatSpec documentation for all properties - Follows repository patterns (PropertiesAsserts, PropertiesConstants, etc.) - Both internal (inheritance) and external (interface) testing modes - Compatible with Echidna and Medusa fuzzers Closes crytic#32
omarinuwa
requested review from
bsamuels453 and
glarregay-tob
as code owners
|
Omar Inuwa seems not to be a GitHub user. You need a GitHub account to be able to sign the CLA. If you have already a GitHub account, please add the email address used for this commit to your account. You have signed the CLA already but the status is still pending? Let us recheck it. |
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.