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 summary of our review process
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 the abs
' parameter
is negative. For such conversions, is_nat: int -> nat option
should be
preferred. This function returns None
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.