Our great sponsors
-
As an example, taken from Certora's tutorials (most examples in this article will be copied or adapted from it), let's say we have a Bank contract that receives and stores deposits from users. We want to verify that, after every deposit, the total funds deposited are greater than every individual user balance.
-
The main challenge is dealing with non-view functions. The default behavior of the prover is to assume that an external call can alter all state on every contract but the caller, noted as HAVOC_ECF. This can lead to state changes in external contracts that are unreachable, making verification more difficult. Furthermore, it assumes that the call is non-reentrant, which in reality is a frequent source of attacks. This last issue can be avoided by indicating that calls can re-enter, noted as HAVOC_ALL, but this means that an external call can mutate any state in any contract, caller included. This leaves the contract being verified in a state where we don't know anything about it after an external call is made. This severely limits what we can prove.
-
SonarQube
Static code analysis for 29 languages.. Your projects are multi-language. So is SonarQube analysis. Find Bugs, Vulnerabilities, Security Hotspots, and Code Smells so you can release quality code every time. Get started analyzing your projects today for free.
-
Understanding a smart contract as a finite-state machine (obligatory mention to Yoichi's bamboo, my favorite smart contract programming language that never happened) allows us to define clear rules on:
-
Let's grab some examples from OpenZeppelin's TimelockController spec. In a Timelock, operations can have different states. We can write a rule that checks, for instance, that calling execute is the only way for moving an operation from ready to done state.
-
Certora's tutorial on github is also a great starting point for the basic concepts, though the lessons for more advanced ones are still under development. The documentation provides a good overview and reference for many concepts, though it's also a work in progress, and redirects to an older set of docs for the more advanced ones. A multi-contract example repo is a good complement to see the documented concepts in action.
-
InfluxDB
Build time-series-based applications quickly and at scale.. InfluxDB is the Time Series Platform where developers build real-time applications for analytics, IoT and cloud-native services. Easy to start, it is available in the cloud or on-premises.
Related posts
- Fork mainnet using hardhat to test and build on DeFi protocols and more
- Generating Decentralized identifier using ERC725 and ERC735
- “Every company will have an nft strategy” - Gary Vee Gary V explains why every company will implement in nft strategy in the next decade. Not every nft will be the next big then but they will still be very useful because the technology is so great. Do you agree with Gary?
- Implementing a Token Contract using Solidity
- Question about implementing a UUPS proxy