At Functori, we believe that smart contracts reviews and audits are crucial to building secure and reliable digital Web3-based services and applications. Thanks to our combined expertise in blockchains, formal methods, and programming languages, we set up a solid methodology for reviewing smart contracts and finding as many bugs and flaws as possible. This blog post provides some insights about our activity in this domain.
What Are Smart Contracts?
Smart contracts are computer programs intended to be deployed and stored on decentralized, digital, transparent, traceable, and irreversible ledgers; at least for public blockchains. A smart contract instance has a state and a set of entrypoints, a sort of public functions, that allow users and other smart contracts to interact with it. Think of a smart contract instance as a RESTful API server where the backend database is the contract's state, and the API's endpoints are the exposed entrypoints.
A deployed smart contract's code is public, meaning anyone can audit it. It is generally immutable, unless some upgrade policy is implemented. Anyone can call its entrypoints, unless explicit restrictions are pre-defined on some of these entrypoints based, e.g., on the caller's cryptographic address.
Smart contracts simplify the exchange of digital goods and services without the need for intermediaries such as banks, notaries, or centralized systems. They have the potential to revolutionize various industries by streamlining processes, reducing costs, and increasing efficiency.
Why Review/Audit Smart Contracts?
Depending on what they are used for, software quality may or may not be an essential matter. For instance, we put a different level of requirements and rigor for a video game compared to banking, airplane, or space rocket software. In fact, an integer overflow in the former would simply lead to a lousy user experience, while it could imply significant human and financial losses in the second. A smart contract that manages a large amount of valuable assets should clearly be classified in the second category.
Let's consider the REST API server example again. When designing or deploying a server, we generally start from a situation where no one can access the services. We then define an access policy (e.g., logical roles and/or machine configuration). Once the rules are written, we can analyze them to see if they are too permissive or restrictive.
On the contrary, smart contracts are primarily designed to be executed in an open environment: both the code and the access policy are public and replicated on several machines. Even if the developer strives to define a consistent access policy, a minor approximation — that would be hurtless for a Web2 centralized architecture — potentially leads to a disaster in the decentralized world of Web3. The DAO's reentrancy bug and the Parity's library self-destruct flaw are typical examples of this claim.
To conclude this section, because smart contracts evolve in an open environment, they don't benefit from a defense-in-depth strategy usually used to secure Web2 infrastructures. Hence, auditing the code is all the more critical.
Our Auditing Process
Regardless of the targeted blockchain, virtual machine, or language, our process for reviewing smart contracts is the same: first, if some documentation or specification is provided, we read it carefully to understand the smart contracts' expected logic and capabilities. Then, we walk through the code to get familiar with it. Generally, it's the phase where we identify the contracts' storage and entrypoints. Depending on the complexity of the logic underlying the smart contracts, we also infer our own specification.
The actual code review phase can then start. We explore the contracts' call graph and carefully read each expression of each function. This phase, which is repeated many times, aims to find flaws in the contracts' logic (compared to the reference specification) or potential bugs due to misusing some language features (e.g., use of Michelson's maps instead of big maps, reentrancy, overflows).
During the phase above, we start a draft report and take notes about our findings. This allows providing feedback to developers proactively so that they begin fixing the code. In some situations, we write tests to confirm a suspected bug. We also redo the calculations if the code involves some non-trivial mathematical formulas.
Our reviews are always conducted by a team of at least two or three engineers. Once we finish the review phase, we polish the draft report and send the final version to the Client. To give an idea, you may want to have a look at the FlameDeFi DEX Smart Contract Review report, which has been made public by FlameDeFi team.
A Feedback From our Conducted Reviews
The most critical bugs are often related to contract logic, and finding those bugs is hard to automate. However, as an example on the simpler side of things, let's provide two of the most frequent error patterns in the contracts we have reviewed so far, and which can be systematically checked for:
- The use of Tezos' sets or maps instead of big maps: tagged as a high or critical issue based on the context, this misuse of Michelson's storage collection could lead to blocking either a user's or the entire contract's assets in the worst case, or to a high gas fee incurring storage deserialized at each call. This is all the more dangerous as unit or small integration tests do not allow spotting this class of issues. As a takeaway, developers should know that Michelson's sets and maps, when they appear as fields of a contract's storage, are fully deserialized at each entrypoint of view invocation. This costs gas, which is bounded and raises the paid fees. On the opposite, big maps are lazy structures. Their values are dynamically fetched from the context on request.
- The use of the
abs: int -> nat
primitive to convert integers to natural numbers: also marked as critical; this misuse of conversion functions enables breaches that may lead to asset theft from the contract. In fact, developers in such situations don't always consider the consequences if theabs
' parameter is negative. For such conversions,is_nat: int -> nat option
should be preferred. This function returnsNone
if the argument is not positive, which obliges developers to handle this particular case and think about it.
Conclusion
To conclude this post, we really enjoy reviewing smart contracts and helping projects get more confidence in their dApps. If you have some application that you would like to get reviewed, don't hesitate to hand it over to our experts.