Smart contracts have been evaporated of ￥100 million by just one line of code? You may need to know something about formal verification!
As the core of Ethereum ecology, smart contracts have developed rapidly in recent years. However, with the frequent emergence of smart contract security issues recently, the disadvantages of smart contracts have become even more apparent. Vulnerabilitys caused by these problems made the market value of famous projects such as DAO, Parity, and BEC almost zero overnight.
In response to these security issues, Chengdu LianAn Technology Co. Ltd. tries to apply the “formal verification” method, which was originally applied in the military industry, to smart contract security audits. Formal verification is based on mathematical modeling methods to describe the system. Through formal verification, the developer can review the security of the program in advance and eliminate logical vulnerabilitys and security vulnerabilitys to ensure the security of the contract.
More details about formal verification , we recently interviewed Yang Xia, the founder&CEO of Chengdu LianAn Technology Co. Ltd., and discussed about the status, principles, and market conditions of formal verification.
Blockchain_Camp: Please introduce the VaaS platform briefly.
Yang Xia: VaaS (Verification as a Services) is the first highly-automated formal verification platform that supports both EOS and Ethereum blockchains, with advantages of high verification efficiency, high degree of automation, low human participation, ease of use, and support for multiple contract development languages.
VaaS is mainly used for the security audit of smart contracts through the “military level” security verification, in order to improve the security of the blockchain ecosystem and achieve the purpose of effectively controlling the risk of vulnerabilitys. VaaS platform’s “one-click” formal verification tool that pinpoints risky code locations and risk causes, effectively validates the general security vulnerability, security attributes, and functional correctness of smart contract or blockchain applications, thereby increase its level of security. the relevant research results have applied for 5 software invention patents.
Blockchain_Camp : What is the difference between formal verification and the practice of traditional Internet security companies?
Yang Xia: The traditional Internet security company is “ Defend by attack.” However, we are directly focusing on the security of the code itself to prevent unsafe incidents. For example, doctors of Western Medicine only treat you when you are sick, while doctors of traditional Chinese medicine emphasize the improvement your resistance. Once your body is healthier, it will be very difficult to get sick.
Blockchain_Camp: What’s the theory of formal verification?
Yang Xia: Formal verification is a method based on Mathematics and Logic. In particular, Before deploying smart contracts, the code and documentation should be modeled formally, then rigorously verifying the security and functional correctness of the code through the mathematical means. we can effectively confirm Whether there are security vulnerabilitys and logic vulnerabilitys in smart contracts . This method can effectively compensate for the traditional defects of finding code logic vulnerabilitys through traditional experience. The advantage of formal verification is that It is impossible to exhaust all possible inputs by means of traditional tests, however, we can overcome this problem from the angle of mathematical proof.
