What is Formal Verification?
For most blockchain newcomers, formal verification may be the first time they have heard of it; even some blockchain practitioners who are not technology-oriented may just “just hear the name, but don’t know its meaning”.
According to Wikipedia’s definition of formal verification, we know that in the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.
From the definition point of view, it seems that formal verification is not as difficult as imagined. In short, it is mathematically proven that the development program is correct. Of course, ‘correct’ here means that the implementation of the program is consistent with the programmer’s development intention. Although formal verification does not seem complicated, it is actually very difficult in practice. This is why formal verification is always shrouded in a layer of ‘’mystery’.
In fact, before formal verification began to be applied in the field of blockchain, its application scenarios revolved around military, aviation, aerospace and other fields; coupled with the scarcity of talents proficient in this technology, it has long been associated with small public, unpopular and other adjectives linked.
Introduce formal methods
Benefits from the relevant theories of the formal method as the basic support, the formal verification technology can achieve further development and application. In simple terms, formal methods refer to the use of mathematical tools, concepts, and methods to define, develop, and verify. Its most obvious feature is that it is based on mathematical foundation, including various logics, set theory, algebra theory, graph theory and so on.
Formal specification: It refers to the application of a formal language with precise syntax and semantics to describe the nature and behavior of the system, and is the basis for designing system constraints and verifying whether the system is correct.
Formal verification: It establishes the relationship between the behavior of the system and its properties on the basis of the formal specification, and then verifies whether the system requires the key properties.
There is a close connection between formal specification and formal verification, which together form the core framework of formal methods. Formal verification is to verify whether an existing program can meet the requirements of its specification, and this is also the core problem that formal methods need to solve.
The main method of formal verification
At present, the more common formal verification methods can be divided into two categories:
Deductive verification: It is based on the basic idea of theorem proving. It uses logical formulas to describe the system and its properties, and proves that the system has certain properties through some axioms or inference rules.
Model Verification: It is a technique based on a finite model and examining the desired properties of the model, which can be used to confirm whether a contract has certain properties through a state space search.
Among them, model verification technology can be regarded as one of the most successful automatic verification technologies in the past 30 years. It has been widely used in the verification of finite state systems, including the analysis and verification of circuit design and communication protocols.
According to the specifications and characteristics of the model to be verified, it can be divided into: composite detector, temporal logic model detector and behavior consistent detector.
According to the different techniques used, it can be divided into: state-oriented model checking and symbolic model checking.
Usually, the model needs to go through an iterative verification process to finally meet the verification conditions.
Formal Verification and Smart Contracts
After ten years of exploration and precipitation, blockchain technology has become a trend leading a new round of technological change, especially the blockchain + application model that empowers real economic industries such as finance, payment, and logistics. An epoch-making long-term mission.
However, the natural characteristics of blockchain technology, such as open source, non-tampering, and anonymity, have put forward extremely high requirements for the security construction of the blockchain ecosystem. In particular, the iconic application of blockchain 2.0, smart contracts, bears huge security pressure at the application level. Since the capital of a smart contract is actually a piece of code running in the blockchain network; as long as it is code, there will inevitably be bugs in the design and development process. Coupled with the exposure of smart contracts to open-source blockchain networks, it becomes very easy to be hacked, resulting in irreparable economic losses.
How to ensure the security of blockchain and smart contracts has become a key issue that restricts the development of blockchain. Among them, strengthening smart contract auditing and improving the prior review mechanism are important guarantees for improving the security protection of blockchain and smart contracts; and formal verification is one of the efficient ways to break the situation.
Apply formal verification to strengthen the security audit of smart contracts, which can impose normative constraints on the generation and execution of smart contracts to ensure the controllability, schedulability, and credibility of smart contracts during execution. sex.
Improving the prior review mechanism through formal verification will eliminate the ambiguity and incompatibility of natural language, eliminate logic loopholes and security loopholes, and then use formal tools to model, analyze and verify smart contracts.
About DeHacker
DeHacker is a team of auditors and white hat hackers who perform security audits and assessments. With decades of experience in security and distributed systems, our experts focus on the ins and outs of system security. Our services follow clear and prudent industry standards. Whether it’s reviewing the smallest modifications or a new platform, we’ll provide an in-depth security survey at every stage of your company’s project. We provide comprehensive vulnerability reports and identify structural inefficiencies in smart contract code, combining high-end security research with a real-world attacker mindset to reduce risk and harden code.
