Formal verification is a method of mathematically proving that a computer program functions as intended. It involves expressing the program's properties and expected behavior as mathematical formulas, and then using automated tools to check that these formulas hold true. This process helps ensure that the program meets its desired specifications.
Formal verification is a tool that can be applied to many systems, including:
- Computer hardware design: Ensuring that integrated circuits and digital systems meet their desired specifications and behave correctly.
- Software engineering: Verifying the correctness and reliability of software systems, especially in mission-critical applications such as aviation, medical devices, and financial systems.
- Cybersecurity: Evaluating the security of cryptographic algorithms and protocols, and identifying vulnerabilities in security-sensitive systems.
- Artificial intelligence and machine learning: Verifying the properties and behavior of AI and ML models, ensuring that they operate as intended and make accurate predictions.
- Automated theorem proving: Verifying mathematical theorems and proving mathematical conjectures, which has applications in fields such as mathematics, physics, and computer science.
- Blockchain and smart contracts: Ensuring the correctness, security, and reliability of blockchain systems and smart contracts.
Formal Verification of Smart Contracts
Formal verification of smart contracts works by representing the logic and desired behavior of smart contracts as mathematical statements, and then using automated tools to check if these statements are correct.
The process involves:
- Defining the specifications and desired properties of a contract in a formal language.
- Translating the code of the contract into a formal representation, such as mathematical logic or models.
- Using automated theorem provers or model checkers to validate that the specifications and properties of the contract hold true.
- Repeating the verification process to find and fix any errors or deviations from the desired properties.
Sometimes the automated theorem provers or model checkers cannot prove or disprove that a property holds true. In this case, the specifications and desired properties may need to be refined and the verification process repeated.
The specifications and desired properties can be refined by applying more specifications to smaller pieces of code or making the specifications more detailed. This can make it easier for the theorem provers and model checkers to validate that specifications and properties hold true.
Formal verification can be applied to one contract or to multiple contracts at a time. Web3 projects often use multiple contracts, and it is important to make sure that the contracts work together and implement the desired project functionality correctly.
This use of mathematical reasoning helps to ensure that smart contracts are free from bugs, vulnerabilities, and other unintended behavior. It also helps to increase trust and confidence in the contract, as its properties have been rigorously proven to be correct.
Translating Code into a Formal Representation
Code Snippet 1 shows a simplified program that implements a token transfer function. There are two users that each have a balance of tokens (balance
and balance2
). The function transferFromUser1
transfers tokens from User 1 to User 2. The program has an invariant that the total supply of tokens always equals the sum of the balances.
uint balance1;
uint balance2;
uint totalSupply;
// Transfer money from User 1 to User 2.
function transferFromUser1(uint amount) {
balance1 = balance1 - amount;
balance2 = balance2 + amount;
}
Code Snippet 1: A simple program illustrating a transfer
We represent the invariant as a mathematical formula. We number formulas to keep track of them. Because formulas are mathematical, = means “equals”, not assignment, in them:Formula 1: totalSupply = balance1 + balance2 // sum of balances
Code Snippet 2 shows how we can add logical formulas representing what is true at each point in the function (for simplicity, we ignore the possibility of integer overflow. Handling that would make the formulas much longer).function transferFromUser1(uint amount) {
// Formula 1: totalSupply = balance1 + balance2
balance1 = balance1 - amount;
// old(balance1) represents the value of balance1 when entering the function.
// Formula 2: totalSupply = old(balance1) + balance2
// Formula 3: balance1 = old(balance1) - amount // implied by the assignment
// Formula 4: Formula 2 ^ Formula 3
balance2 = balance2 + amount;
// old(balance2) represents the value of balance2 when entering the function.
// Substitute old(balance2) into Formula 4, replacing balance2.
// Formula 5: (totalSupply = old(balance1) + old(balance2)) ^
// (balance1 = old(balance1) - amount)
// Formula 6: balance2 = old(balance2) + amount // implied by the assignment
// Formula 7: Formula 5 ^ Formal 6.
// Formula 7 expands to:
// (totalSupply = old(balance1) + old(balance2)) ^
// (balance1 = old(balance1) - amount) ^
// (balance2 = old(balance2) + amount)
}
Code Snippet 2: Function with logical formulas representing the meaning of the code.
If we want to check that transferFromUser1
maintains the program invariant, we can check that Formula 7 (at the end of the function) implies the invariant (Formula 1). Here is the proof, using high-school algebra simplification rules.
Assume Formula 7 is true
Solve for old(balance1) and old(balance2) using the last 2 clauses of Formula 7:
old(balance1) = balance1 + amount
old(balance2) = balance2 - amount
Substitute that into the first clause of Formula 7:
totalSupply = (balance1 + amount) + (balance2 - amount)
Cancel addition and subtraction of amount:
totalSupply = balance1 + balance2
How formal verification and manual auditing work together
Formal verification and manual auditing complement each other in ensuring the security of smart contracts.
Formal verification provides a systematic and automated way to check the contract's logic and behavior against its desired properties, making it easier to identify and fix any potential errors or bugs. It is especially useful for finding complex and subtle issues that may be difficult to detect through manual inspection. When dealing with complex or multiple contracts, it can become difficult for a human to reason about all the possible combinations and cases that need to be checked. Machines, however, are well-suited to this task.
Manual auditing provides a human expert review of the contract's code, design, and deployment. The auditor can use their experience and expertise to identify potential security risks and evaluate the contract's overall security posture. They can also verify that the formal verification process was performed correctly, and check for issues that may not be detectable with automated tools. Their expert insight helps ensure that the specifications and desired properties used in formal verification are indeed the right ones.
Combining formal verification and manual auditing provides a comprehensive and thorough evaluation of a smart contract's security, increasing the chances of finding and fixing any vulnerabilities. The result is a defense-in-depth approach to security that leverages the unique capabilities of both humans and machines.
Conclusion
This is an overview of what formal verification is and how it can be applied to increase the security of smart contracts and decentralized applications. Stay tuned for a forthcoming technical deep dive into the formal verification of ERC-20 tokens.
This is a guest post from CertiK originally published here.
What is CertiK:
CertiK is a blockchain security firm that helps projects identify and eliminate security vulnerabilities in blockchains, smart contracts, and Web3 applications using its services, products, and cybersecurity techniques.
Where to find CertiK:
This is a paid press release, BSC.News does not endorse and is not responsible for or liable for any content, accuracy, quality, advertising, products, or other materials on this page. The project team has purchased this advertisement article for $1500. Readers should do their own research before taking any actions related to the company. BSC.News is not responsible, directly or indirectly, for any damage or loss caused or alleged to be caused by or in connection with the use of or reliance on any content, goods, or services mentioned in the press release.
This is a paid press release, BSC.News does not endorse and is not responsible for or liable for any content, accuracy, quality, advertising, products, or other materials on this page. The project team has purchased this advertisement article for $2500. Readers should do their own research before taking any actions related to the company. BSC.News is not responsible, directly or indirectly, for any damage or loss caused or alleged to be caused by or in connection with the use of or reliance on any content, goods, or services mentioned in the press release.
Author
Related News
Binance Executive Tigran Gambaryan Sues Nigeria's NSA and EFCC
The lawsuit reflects escalating tensions amidst allegations of innocence and regulatory scrutiny surrounding Binance Nigeria's alleged involvement in illicit financial activities.
The detained executive of Binance, Mr. Tigran Gambaryan, has taken legal action against Nigeria's National Security Adviser (NSA) Nuhu Ribadu, and the Economic and Financial Crimes Commission (EFCC).
Gambaryan, along with the firm's Africa Regional Manager, Mr. Nadeem Anjarwalla, filed a fundamental human rights violation suit amidst ongoing legal turmoil.
Gambaryan's legal challenge, initiated alongside his lawyer Mr. Olujoke Aliyu, aims to address his prolonged detention by the federal government. The suit, presented before Justice Inyang Ekwo of the Federal High Court in Abuja, challenges the legality of Gambaryan's continued confinement and the seizure of his international travel passport.
Gambaryan, a US citizen overseeing financial crime compliance at Binance, contends that his detention and passport seizure violates Section 35 (1) and (4) of Nigeria's 1999 Constitution. His legal team seeks various reliefs, including his release from custody, the return of his passport, a public apology from the NSA and EFCC, and an injunction against future investigations.
Allegations of Innocence Amidst Legal Turmoil
Gambaryan and his colleague's legal representatives maintain their innocence, claiming that the arrests occurred during discussions with Nigerian authorities regarding legal conflicts involving Binance.
In a dramatic turn of events, Binance's African regional manager, Nadeem Anjarwalla, recently fled Nigerian custody. Anjarwalla's escape follows mounting tensions surrounding the Nigerian authorities' investigation into alleged illicit financial activities involving Binance Nigeria, totaling a staggering $26 billion.
This is a paid press release, BSC.News does not endorse and is not responsible for or liable for any content, accuracy, quality, advertising, products, or other materials on this page. The project team has purchased this advertisement article for $1500. Readers should do their own research before taking any actions related to the company. BSC.News is not responsible, directly or indirectly, for any damage or loss caused or alleged to be caused by or in connection with the use of or reliance on any content, goods, or services mentioned in the press release.
This is a paid press release, BSC.News does not endorse and is not responsible for or liable for any content, accuracy, quality, advertising, products, or other materials on this page. The project team has purchased this advertisement article for $2500. Readers should do their own research before taking any actions related to the company. BSC.News is not responsible, directly or indirectly, for any damage or loss caused or alleged to be caused by or in connection with the use of or reliance on any content, goods, or services mentioned in the press release.
Follow us on Twitter and Instagram!
If you need tools and strategies regarding safety and crypto education, be sure to check out the Tutorials, cryptonomics explainers, and Trading Tool Kits from BSC News.
Looking for a job in crypto? Check out the CryptoJobsNow listings!
Author
Try Now!
Sign up Now
Coming Soon
WIN BIG
Coming Soon
Start Earning Today!
Earn Now
Coming Soon
Sign Up Now
Play & Mine!
Coming Soon
Editors Choice
Other Currencies
- nameLTBuyLitecoin
Sponsored
Buy Crypto with Fees as low as 0%
Buy Crypto with a bank transfer, credit or debit card, P2P exchange, and more. Not investment advice. All trading risk. Terms apply.
£0£0+0% - nameLTBuyEOS
Sponsored
Buy Crypto with Fees as low as 0%
Buy Crypto with a bank transfer, credit or debit card, P2P exchange, and more. Not investment advice. All trading risk. Terms apply.
£0£0+0% - nameLTBuyMonero
Sponsored
Buy Crypto with Fees as low as 0%
Buy Crypto with a bank transfer, credit or debit card, P2P exchange, and more. Not investment advice. All trading risk. Terms apply.
£0£0+0% - nameLTBuyBitcoin Cash
Sponsored
Buy Crypto with Fees as low as 0%
Buy Crypto with a bank transfer, credit or debit card, P2P exchange, and more. Not investment advice. All trading risk. Terms apply.
£0£0+0%