Professor Yang Xia of LianAn Technology : As the EOS Main network is coming online, the security of smart contract is guaranteed by VaaS.
The year-long EOS crowdfunding finally came to a successful end at the beginning of this month. The ICO of $4 billion this year has also achieved another record in the history of cryptocurrencies, the longest and the largest. Just as the EOS Main network is about to go online, the issue of smart contract vulnerabilitys is also the focus of attention in addition of the underlying vulnerabilitys of the platform. The Chainb.com specially invited a formal verification expert, Professor Yang Xia, the founder of Chengdu LianAn Technology, to share her ideas with us.
Chainb.com: Recalling the development history of blockchain, what are the areas where this technology is vulnerable to hacking?
Professor Yang: The areas that are vulnerable to hacking in blockchain technology include two aspects: blockchain underlying platforms and blockchain smart contracts. Due to its small code and low complexity, Small contract is easy to attack. Therefore, the main target of hacker attack is smart contract. The main reason for these attacks is that these programs have their own security vulnerabilitys or logic vulnerabilitys.
Chainb.com: For the industry, the exposure of each security problem is undoubtedly a great stick to the development of blockchain technology. Are there any methods to renovate these security risks?
Professor Yang: Once the blockchain platform appears security problems, it will bring about huge property losses, thus causing panic in the currency market. These security issues can be resolved with appropriate measures. For example, before deploying in smart contracts, strict security audits can effectively improve the security of smart contract procedures and prevent potential security risks in advance. Our VaaS which is smart contract security auditing platform adopts formal verification methods and techniques, and is the first tool to automate the detection of contract security vulnerabilitys.
Chainb.com: How does the VaaS platform implement inspection and verification on various attributes of smart contracts? Could you please give me an example?
Professor Yang: The VaaS platform uses formal verification techniques that have been widely used in key areas of safety such as aviation, aerospace, and military. You can effectively discover logical vulnerabilitys and security vulnerabilitys in your code to make up for the lack of the manual search for vulnerabilitys, through the formalization of contract documents and codes and verifying the functional correctness and security attributes of smart contracts by mathematical reasoning and proof. The following example shows how to detect the vulnerability through the formal verification method by taking the example of an overflow security vulnerability check that is frequently performed recently:
If you check whether there is an overflow vulnerability in the code “int8 c = a + b”, the following shows the proof of the functional correctness and security attributes of this line of code;
We first model integer types and define the formal rule “Int8.repr: Z -> int8”. This rule obtains an 8-bit length machine integer by truncating the lower 8 bits of a purely mathematical integer (ranging from infinitesimal to infinity). Then write the formal specification of the additive operation as follows:
{a:int8,b:int8}
// set the prerequisites for code execution to ensure that the type of a and b is an 8-bit signed machine integer;
{c = a + b;} // Source program of the addition operation
{(int8.repr(a+b))
/\ ((Int8.repr (a+b)) = (a+b))} ; // Set the postcondition for code to execute correctly.. The description of (int8.repr(a+b)) is to prove whether the function correctness of the code is satisfied. That is, it is necessary to prove that the source code is to sum a and b instead of counting difference or any other operation logic, and the operation result is convert to int8 type; in addition, it is necessary to prove whether the security properties overflow, so add the postcondition ((Int8.repr (a+b)) = (a+b)), because once a + b> int8.max_singed Or a+b<int8.min_signed will result in (Int8.repr (a+b)) ≠ (a+b).
Finally, prove whether the execution of the code satisfy the postcondition mentioned above according to the precondition. If an unverifiable result is generated, it indicates that the program is not functioning correctly or there is an overflow security vulnerability. Then analyze and modify the source program based on the prof results, and then reproved until the proof is passed.
We use this mathematical proof method to formalize the code as a formula, and prove the same other logic vulnerabilitys and security vulnerabilitys on its attributes. Based on this principle, we have implemented an automated verification tool through which the functional correctness and security attributes of the code can be verified easily and quickly.
