Rob Behnke
June 15th, 2023
When it comes to security audits and analysis of smart contracts, checking for correctness in the smart contract code is an important first step. Typical traditional testing methodologies like unit tests, integration tests, and end-to-end tests play a crucial role in smart contract auditing. Still, there are even more advanced techniques that auditors and security teams can employ to provide a higher level of assurance.
One of the most adopted techniques for smart contract auditing is formal verification, and in this article, we will dive deeper into it, exploring how this technique can significantly enhance the security audit process and provide intermediate to advanced security experts with powerful tools for ensuring the correctness and reliability of smart contract implementations. From formal specification to model checking and formal proofs, we’ll examine each approach's patterns, limitations, and practical applications. Additionally, we’ll discuss the challenges and some considerations for using formal verification in the smart contract auditing landscape.
Before we dissect what formal verification is and the techniques that apply to blockchain technology, let’s first understand the foundational concepts.
Formal methods in cybersecurity refer to a set of techniques employed to model software systems as mathematical entities or objects. They involve writing specifications in formal logic, utilizing model checking, performing verification, and constructing formal proofs to ensure the correctness and reliability of the systems that would rely on them.
Formal methods are categorized into two disciplines:
Formal specifications: writing comprehensive specifications
Formal verification: creating proofs that justify the correctness of a formal specification.
A formal specification in smart contract development refers to technical requirements that a contract must satisfy. Writing a formal specification for a smart contract means documenting what the contract does, how it does it, and how it will behave in different environments. If a smart contract violates the formal specifications for it, even in the slightest way possible, then it is considered insecure.
Formal verification of a smart contract is a process that involves writing proofs that prove or check whether the smart contract follows its provided specification.
The formal method joins these two categories to achieve the goal of checking smart contract correctness, following these steps:
Creating a formal model for the target smart contract
Writing a formal specification of the required properties that satisfies the model
Checking the model against the specification
The check can be done in two ways:
Using the state exploration approach that checks all possible states in an automatic manner. This approach is difficult to scale and often leads to state explosion, where the number of states grows exponentially until it no longer fits the computer’s memory.
Using the proof-based approach that involves writing theorems manually by a human. This method is more precise but requires the assistance of a proof assistant (such as Coq or Isabelle), resulting in time and effort consumption for its implementation.
The formal verification process typically involves the following steps:
The first step in the formal verification process is to define the system's specifications and properties that need to be verified. This involves precisely capturing the desired behavior, safety requirements, and invariants of the system or smart contract. To ensure clarity and precision, the specifications can be expressed using formal languages, such as temporal logic or functional specifications.
Once the specifications and properties are defined, a mathematical model of the system or smart contract is constructed. The model serves as an abstract representation of the system, capturing its essential components, states, and transitions. Depending on the verification technique used, the model can take various forms, such as finite-state machines, Petri nets, or transition systems.
In this stage, the constructed model is subjected to formal analysis techniques to verify the desired properties. The analysis process may involve techniques like model checking, theorem proving, or abstract interpretation. Model checking explores all possible system states and transitions to validate whether the properties hold or identify potential violations. Theorem proving employs logical reasoning to construct formal proofs of the desired properties. Abstract interpretation provides a static analysis framework to approximate the system's behavior and infer properties.
During the formal analysis, a counterexample is generated if a property is violated or not proven. A counterexample represents a specific scenario or execution path that demonstrates the violation of the property. Analyzing counterexamples helps identify the root cause of the violation and provides insights into potential fixes or improvements to the system or smart contract design.
Based on the insights gained from the formal analysis and counterexample analysis, the system or smart contract design can be refined and iterated upon. This may involve modifying the specifications, adjusting the model, or revisiting the implementation code. The refinement and iteration process aims to address identified vulnerabilities, strengthen the system's properties, and enhance its overall correctness.
Formal verification often relies on specialized tools and software frameworks to automate and assist in the verification process. These tools provide functionalities for modeling the system, expressing properties, performing formal analysis, and generating diagnostic information. Examples of such tools include model checkers, theorem provers and assistants, and static analyzers specifically designed for formal verification.
For Solidity, formal verification is done with the use of Satisfiability Modulo Theories (SMT) and Horn solving.
Satisfiability Modulo Theories (SMT) is an automated reasoning technique that helps Solidity contract auditors verify complex logical formulas and constraints in their smart contracts. It combines the ability to check if a formula is satisfiable (can be true) with reasoning about theories specific to Solidity, such as arithmetic and arrays. SMT enables auditors to identify bugs, vulnerabilities, and logical inconsistencies early in the development process, improving the reliability of smart contracts.
On the other hand, Horn solving is an automated reasoning technique that auditors can use to verify properties and logic in their smart contracts. In simple terms, Horn solving focuses on solving logical formulas expressed in Horn clauses, which consist of a head (conclusion) and a body (premise). It is particularly useful for verifying properties like code correctness and contract safety. By applying Horn-solving techniques, Solidity contract auditors can automatically reason about the behavior of their smart contracts and verify if certain conditions always hold or if they may lead to undesirable outcomes. This helps identify potential issues, such as security vulnerabilities or unintended behavior, in the contract code.
The practical applications of formal verification include the following:
Smart contract code correctness and invariant verification
Bug detection and vulnerability analysis
Smart contract upgrades and migration impacts
System integration and interoperability consistencies and vulnerabilities
Compliance and regulatory requirements
The following are some of the key challenges associated with adopting formal verification of Solidity smart contracts:
Complexity and scalability: It is computationally intensive and time-consuming. As the size and complexity of the smart contract increase, the scalability becomes even more challenging. Smart contract auditors need to carefully select appropriate verification tools, techniques, and optimizations to efficiently handle the complexity and ensure timely verification.
Cost and time investment: It requires time and dedicated efforts from skilled professionals to model the system, specify properties, conduct the verification, and analyze the results. Auditors need to consider the trade-offs between the potential benefits of formal verification and the associated costs in terms of time, expertise, and computational resources.
Limited language support: There is limited tooling support for formal verification of contracts in the development programming languages, including the advanced features of Solidity. It is essential to consider the tooling landscape and choose the most suitable tools that align with the specific requirements and features of the smart contract being verified.
Specification challenges: Specifying complex behavior, handling edge cases, and capturing all relevant properties can be non-trivial. Ambiguities or gaps in specifications can lead to false positives or negatives. Auditors need to invest time and effort in formulating clear and unambiguous formal specifications that accurately represent the intended behavior of the smart contract.
False positives and false negatives: False positives occur when the tool flags a potential issue that is not actually a vulnerability, resulting in unnecessary investigation or code modifications. False negatives occur when the tool fails to detect an actual vulnerability, potentially leading to security risks. Developers need to carefully analyze and interpret the verification results, distinguishing genuine issues from false alarms to ensure effective verification outcomes.
Addressing the challenges and considerations in formal verification is crucial for mitigating risks and protecting your smart contracts from vulnerabilities. That's where Halborn comes in. As a leading blockchain security firm, Halborn offers comprehensive smart contract auditing and formal verification services. With our team of experienced Web2 and Web3 security experts and cutting-edge tools, Halborn can help you navigate the complexities of formal verification, identify potential vulnerabilities, and fortify your smart contracts against attacks. Get in touch with Halborn to take your smart contract security to the next level.