By Pruvendo
Blockchain smart contracts is not new technology.
For 7 years people have been engaged in smart contract’s development for the most different types of projects, from DAOs to GameFi. But security problems, which were relevant 7 years ago, are still relevant now.
Why, despite the application of audit to almost every web3 project, the vast majority of smart contracts continue to be vulnerable and contain exploits?
The main reasons that most smart contracts are insecure:
- Technologies that do not meet modern realities.Due to the fact that most vulnerabilities are not obvious, it’s required an enormous amount of time to find them using most prevalent methods like testing or code review.
- Lack of time on production.Usually smart contracts are written in a short time to meet the TTM deadline. And often in such conditions, security is not the main goal, considering that the security check key point is audit.
- Insufficient tools.The fact that there are no tools or solutions in the smart contract developer’s toolset which could allow them to quickly detect vulnerabilities in smart contracts during the development process.
- The complexity of smart contract logic.Smart contracts often contain tens of thousands lines of code, a large number of functions and variables, which make it impossible to cover all probable scenarios that may trigger errors or vulnerabilities, when there are millions of possible combinations and interactions between them.
All this leads to the fact that vulnerabilities remain in smart contracts after the project is launched. And, due to that in most cases smart contracts are immutable, it’s nearly impossible to prevent the attack and money loss (usually the major problem is not even money, but reputational loss).
But what tool or method could help to avoid all these risks and would allow to create 100% secure-by-design smart contract, unavailable to be hacked or attacked?
The formal verification (FV).
How? — let’s analyze its application using examples of the most common vulnerabilities of smart contracts.
Integer Arithmetic Error
Shortly — the overflow of integers and the problem that there could be inaccuracy in values during the calculation process.
The way that FV prevents this error is simple — during the process of formal verification of the smart contract all possible values are tested. There couldn’t be an unexpected value, which may cause an error.
Missing Parameters
This occurs from sloppy designs in smart contracts and some other programming mistakes during the process. Application of the FV fixes the entire problem by checking every possible input and prerequisite for every operation. This solves the problem from its basics.
Smart Contract Security Audit
How about using actual audit (code review + testing) to verify security of formally verified smart contracts? The answer is already in the question: if the smart contract is formally verified, then methods, which are currently used by auditors will not find any bugs or exploits due to their absence.
Last thoughts
There are many ways to attack a smart contract. But all of them developed in a situation where smart contracts had many vulnerabilities and had no mechanisms to avoid this.
The application of formal verification changes the rules of the game between hackers and security engineers, invalidating hackers of ways to attack.
All Comments