crytic / properties Goto Github PK
View Code? Open in Web Editor NEWPre-built security properties for common Ethereum operations
License: GNU Affero General Public License v3.0
Pre-built security properties for common Ethereum operations
License: GNU Affero General Public License v3.0
Ex: maybe making a lib version?
See https://twitter.com/agfviggiano/status/1732328333105418326
I am reviewing a smart contract that contains a very complex logic to mint NFTs with random rarities using Chainlink VRF. Just by reading the code it is hard to understand if it correctly implements the specification. It would be nice to have pre-built echidna properties to test invariants.
In my particular example, the invariants are rather commonplace to other NFT projects, which is why I believe these are generic enough to be applied to other smart contracts:
If you think this is useful I can work on these properties and submit a PR.
PropertiesHelper.clampBetween
do not emit a LogString
event with the value is clamped, which makes debugging harder. This is missing in both uint256
and int256
versions.
ERC721 might be a good target
The formatting of the codebase is inconsistent:
https://github.com/crytic/properties/blob/main/contracts/util/PropertiesHelper.sol#L184
if ( !(a < b)) {
https://github.com/crytic/properties/blob/main/contracts/util/PropertiesHelper.sol#L197
if(!(a <= b)) {
add invariants like https://twitter.com/CertoraInc/status/1727791536933323201
This is a bit subjective, but I find it confusing:
import {PropertiesAsserts} from "@crytic/properties/contracts/util/PropertiesHelper.sol";
I propose a refactor so that the contract name matches the contract filename:
import {PropertiesAsserts} from "@crytic/properties/contracts/util/PropertiesAsserts.sol";
We can re-use some of the work done for ABDK to support https://github.com/PaulRBerg/prb-math
CryticERC721ExternalBurnableProperties contains 5 tests while CryticERC721BurnableProperties contains 6 tests. This means that the list of 19 property tests for ERC721 is actually only 18 property tests for the external tests. Either a test is forgotten in the external tests or the list of property tests should differ for external vs internal.
The external tests only have one test test_ERC721_external_burnRevertOnTransfer
while the internal tests have test_ERC721_burnRevertOnTransferFromPreviousOwner
and test_ERC721_burnRevertOnTransferFromZeroAddress
.
No response
2.2.3
No response
The PropertiesConstants
contracts contain some hardcoded parameters that are related to Echidna's default setup, such as USER1
, USER2
, and USER3
.
The issue is that it also contains INITIAL_BALANCE
, which has nothing to do with balanceAddr
or balanceContract
. This can be confusing to users.
Maybe it is better to migrate this value to another contract and create the related BALANCE_ADDR
or BALANCE_CONTRACT
variables.
N/A
N/A
N/A
N/A
Which would cover everything in https://github.com/crytic/building-secure-contracts/blob/master/development-guidelines/token_integration.md#erc20-tokens, plus other edge cases we are aware of
The idea would be to have helpers to ease the integration of erc20 edge case, like
import "@crytic/properties/contracts/util/erc20/erc20.sol";
Which would include :
all_erc20_standard() returns ( IERC20[] memory)
- returns all standards token deployed, and converted to IERC20
object (or a similar name)all_erc20_non_standard() returns ( IERC20[] memory)
- returns all non-standard token deployed, and converted to IERC20
object (or a similar name)all_erc20() returns ( IERC20[] memory)
- returns all tokens deployed, and converted to IERC20
object (or a similar name)In the IERC721Internal
interface you define the following function usedId
:
function usedId(uint256 tokenId) external view returns (bool);
I'm having a hard time to understand what is the reason behind using this as part of the interface. In your ERC721Compliant
contract, you declare it but not use it:
If someone adds something like usedId[id] = true
to the _customMint
function, the following property always fails obviously:
If you want to track the used ids, you should update it after the above test assertion to make sense.
Furthermore, the README
section on the ERC721
is outdated. There is no ITokenMock
in the ERC721
case for example, but IERC721Internal
. I would recommend making it consistent with the ERC20
example tho & updating the docs about the latest status quo.
I would consider it as a big value-add, if you could add the common property assertions for any EIP-1155-based contracts.
There's a set of functions in contracts/util/PropertiesHelper.sol
named clamp...
for making numbers fit in a fixed range by performing modulo. For example using such function to put numbers 0-10 in the range 4-6 will result in:
in: 0 1 2 3 4 5 6 7 8 9 10
out: 6 4 5 6 4 5 6 4 5 6 4
In the programming nomenclature the term "clamp" usually refers to putting number in a fixed range by assigning it the value of the boundary, if that boundary is exceeded. For example clamping numbers 0-10 in the range 4-6 would result in:
in: 0 1 2 3 4 5 6 7 8 9 10
out: 4 4 4 4 4 5 6 6 6 6 6
I'm writing this based on my experience, I got really confused when I saw PropertyHelper
's clamp...
functions in use for the first time. I checked my expectations by searching on the internet for "clamp a number", and all the resources were referring to "clamping" as assigning the exceeded boundary, not calculating the modulo. I think that many developers using PropertiesHelper
for the first time will be confused or misled.
I think that the clamp...
functions should be renamed to something less confusing. For example the name wrap...
could be good, it would reflect how numbers exceeding the limit are returning into the range on the other end.
Write code using PropertiesHelper
.
No response
All of them.
No response
https://github.com/d-xo/weird-erc20#tokens provides a good list of non-standard ERC20 tokens, along with nice example contracts. I think we should aim to integrate these tokens as test-cases and be able to detect a good number of these.
For example, we can use a low level call, or try/catch, and verify that it actually reverts
Since a lot of MultiSigs work in a relatively similar way (e.g., using signatures, some threshold of votes/signatures is required, only approved signers can execute, etc.) we could probably build a set of general properties to test MultiSigs.
For example:
Uniswap v2 might be a good first one
When integrating https://github.com/crytic/properties with an existing foundry codebase, many assertion helpers collide with forge-std/Test.sol
, which makes it harder to use both helpers on the same set of contracts.
For example, this repo's assertWithMsg
from this repo serves the same purpose as foundry's assertTrue
, so they could have the same name. Also, one uses assertGte
while the other uses assertGe
, etc.
It would be nice if this repo was fully compatible with foundry for an easier integration.
These 2 tests:
contract CryticABDKMath64x64Properties {
...
function add_test_range(int128 x, int128 y) public view {
int128 result;
try this.add(x, y) {
result = this.add(x, y);
assert(result <= MAX_64x64 && result >= MIN_64x64);
} catch {
// If it reverts, just ignore
}
}
function sub_test_range(int128 x, int128 y) public view {
int128 result;
try this.sub(x, y) {
result = this.sub(x, y);
assert(result <= MAX_64x64 && result >= MIN_64x64);
} catch {
// If it reverts, just ignore
}
}
}
They are not actually showing failure in case this.add
/this.sub
overflow or underflow.
It looks like result
being int128 makes it always conforming with the assert statement despite the failure in this.add
/this.sub
.
pragma solidity ^0.8.0;
import "@crytic/properties/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol";
contract CryticABDKMath64x64Harness is CryticABDKMath64x64Properties {
/* Any additional test can be added here */
}
Working directory: tests/ABDKMath64x64PropertyTests/hardhat
Force ABDKMath64x64
to overflow/underflow by commenting out the require statement on the tested methods.
library ABDKMath64x64 {
....
function add (int128 x, int128 y) internal pure returns (int128) {
unchecked {
int256 result = int256(x) + y;
// COMMENTED THIS TO FORCE IT TO FAIL
// require (result >= MIN_64x64 && result <= MAX_64x64);
return int128 (result);
}
}
function sub (int128 x, int128 y) internal pure returns (int128) {
unchecked {
int256 result = int256(x) - y;
// COMMENTED THIS TO FORCE IT TO FAIL
// require (result >= MIN_64x64 && result <= MAX_64x64);
return int128 (result);
}
}
}
Run echidna-test . --contract CryticABDKMath64x64Harness --test-mode assertion
Output:
sub_test_range(int128,int128): passed! ๐
abs(int128): passed! ๐
add_test_maximum_value(): passed! ๐
mulu(int128,uint256): passed! ๐
add_test_range(int128,int128): passed! ๐
add_test_range
and sub_test_range
did not fail as expected.No response
Echidna 2.0.1
No response
We need to standardize the properties in this repo, for example:
We should also agree on a structure to group the properties in the file, and how to document the sections (ex
properties/contracts/Math/ABDKMath64x64/ABDKMath64x64PropertyTests.sol
Lines 379 to 384 in c25de70
Once we have defined the rules, we should apply them on the repo, and integrate them in the contribution guidelines
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.