Recently, ChatGPT has become popular, and its active users have exceeded 100 million in just two months since its launch. Using it to write articles, code codes, fall in love, find a job and reply to emails has become a routine operation. There are many ways to teach you to use this software to make money on the Internet. Even a professor from the Wharton School of Business at the University of Pennsylvania claimed that student ChatGPT passed the business management exam.
As a result, the topic of artificial intelligence replacing certain jobs or even human beings being replaced by artificial intelligence has become a hot topic. In the era when everyone is imprisoned, everyones heart is gradually beating.
So can artificial intelligence, or computer products such as formal verification, replace humans? In the world of Web3.0, can formal verification replace manual review?
formal verification
Formal verification is a mathematical proof method for verifying that a computer program works as expected. It expresses the properties and expected behavior of programs as mathematical formulas, and then uses automated tools to check whether these formulas hold. This process helps to ensure that its programs meet expectations.
Application of Formal Verification
Formal verification is a tool that can be widely used in different systems, including:
Computer hardware design: Ensuring that integrated circuits and digital systems meet the specifications they need and behave correctly.
Software Engineering: Validating the correctness and reliability of software systems, especially in mission-critical applications/domains such as aviation, medical devices, and financial systems.
Network Security: Assess the security of cryptographic algorithms and protocols, and identify security gaps in security-sensitive systems.
AI and Machine Learning: Validate the properties and behavior of AI and ML models to ensure they perform as expected and make accurate predictions.
Automatic theorem proving: verifying mathematical theorems and proving mathematical conjectures, applied in the fields of mathematics, physics and computer science.
Blockchain and smart contracts: Ensure the correctness, security and reliability of blockchain systems and smart contracts.
Formal Verification of Smart Contracts
The formal verification of smart contracts is to express the logic and expected behavior of smart contracts with mathematical expressions, and then use automated tools to check whether these mathematical expressions are correct.
This process includes:
The specification and properties of the contract are defined in a formal language.
Translate the code of the contract"” into a formal representation, such as mathematical logic or a model.
Use an automated theorem prover or model checker to verify that the contracts specification and properties hold.
Repeat the verification process to find and fix any errors or deviations from expectations.
Sometimes an automated theorem prover or model checker cannot prove or disprove a property. In this case, it may be necessary to refine the specification and desired properties and repeat the verification process.
Breaking down the specification into smaller pieces of code or providing more specification information can refine the specification and its expected properties. This can make it easier for theorem provers and model checkers to verify that specifications and properties hold.
Formal verification can be applied to one contract or to many contracts at the same time. Web3.0 projects often use multiple contracts, and it is important to ensure that these contracts work together and correctly implement the desired project functionality.
In formal verification, the use of this mathematical method helps to ensure that smart contracts are free from bugs, bugs, and other unexpected behaviors, since their properties have been rigorously proven to be correct mathematically.
formalize the code
Code snippet example one
The following code shows a simplified token transfer function program: There are two users, each of whom has some tokens (balance and balance 2). The function transferFromUser 1 transfers tokens from User 1 to User 2 . The program has an invariant that the total supply of tokens is always equal to the sum of balances.
Code snippet 1: Token transfer program
We express the invariants with mathematical formulas and number the formulas. In mathematical formulas, = means equal to, not assignment.
Code snippet example 2
The following code shows how to add logical formulas (integer overflow is ignored for the sake of simplicity and clarity of the example).
Code snippet 2: Logical formula function that expresses the meaning of the code
If one wanted to check that transferFromUser 1 held an invariant in the program, then we could check Equation 7 (at the end of the function) for the invariant (Equation 1). Below is a proof using high school algebra methods.
Collaboration of Formal Verification and Manual Audit
In terms of ensuring the security of smart contracts, formal verification and manual auditing can be said to complement each other.
Formal verification:
Formal verification provides a systematic and automated way to check the logic and behavior of a contract and its expected properties, making it easier to identify and fix potential bugs or vulnerabilities. It is very effective for finding complex or subtle problems that may be difficult to detect through manual inspection.
When dealing with complex or multiple contracts, it is difficult for humans to reason about all the combinations and possibilities that need to be checked, while machines are no pressure.
Manual Audit:
Human auditing provides expert review of contract code, design, and deployment. Audit experts can use their experience and expertise to identify potential security risks and evaluate the overall security situation of the contract.
In addition to this, humans can also verify that the formal verification process was performed correctly and check for issues that cannot be detected with automated tools. Therefore, human expert audit is more helpful to ensure the correctness of specifications and required properties used in formal verification.
To sum up, only by combining the two methods of formal verification and manual audit can a comprehensive and thorough evaluation of the security of smart contracts be conducted, and the chances of discovery and bug fixes be increased. It’s also an approach to security that combines the strengths of humans and machines and is called “defense in depth.”
Security Expert Online AMA
The power of formal verification cannot be underestimated, but the importance of manual auditing cannot be ignored. On the ChatGPT official website, it has admitted its own shortcomings, and the clichéd discussion that artificial intelligence cannot replace human thinking and creation can also omit 10,000 words here... No, Bard made a mistake and Googles stock price plummeted.
Similarly, formal verification cannot replace manual auditing, and the two complement each other to conduct a complete inspection of smart contracts.
Have any questions after reading the article? Why not be a guest at [CertiK Twitter AMA] on [Friday, February 10 Japan], and have an online one-on-one QA with experts! Friends who are unable to attend due to jet lag can leave a message in the background, and we will convey it to the guests for you and release the content of the AMA replay!
