How Formal Verification Would Have Fortified Beauty Chain (BEC) Contract

How Formal Verification Would Have Fortified Beauty Chain (BEC) Contract
CertiK: formal verification platform for smart contract and blockchain ecosystems
Creating a safe Ethereum contract that is free from exploitable bugs is much harder than it sounds. Researchers have discovered in March that over 34,000 Ethereum smart contracts may be vulnerable for exploitation.

In recent Beauty Chain (BEC) coin incidence, a security loophole from one line of code almost resulted in the market cap drop to almost zero. As many articles have discussed this attack in details, let’s just briefly review the incidence.

What Happened
The code is straightforward: the batchTransfer function, as its name suggests, transfers a fixed amount of tokens (line 1, _value) to the address in the given array (line 1, _receivers). The transaction is completed by first, calculating the total number of tokens to be deducted from the sender (line 4) and making sure the sender have enough balance, then transferring the tokens from the sender to each receiver (line 12).

But, what went wrong?

It turns out that the following line has the common integer overflow problem:

uint256 amount = uint256(cnt) * _value;
This overflow gave hackers a chance to withdraw more than the balance of an account. The hackers used a dynamic array of two addresses, and a value of 2²⁵⁵ to abuse the vulnerable contract and successfully transferred 2²⁵⁶ tokens to their accounts as recorded here:

How does CertiK verification detect this bug automatically?
These types of bug are usually straightforward in hindsight, but not quite so when you try to locate it from a pile of codes. Subtle bugs are always buried in deep and hard to detect.

What if I tell you that this bug can be easily tracked down by using an automated formal verification platform? Below is a screenshot of a sample report that is automatically generated by our formal verification engine:

We added the labels for batchTransfer function to specify:

// assuming function batchTransfer completes execution
@tag assume_completion
// prove that there is no overflow problems
@post __has_overflow == false
These labels are processed, translated and validated by our formal verification engine to prove the functional correctness of the implementation. In the BEC sample code, the entire verification process completes in seconds with a clear counter-example that breaks the specification proving the existence of the overflow bug.

CertiK verification engine tracks down the integer overflow bug
If, for instance, Beauty Chain had their contract verified by CertiK, the one-billion-dollar loss would be saved.

About CertiK
At CertiK, our mission is to give people the power to trust, and provide the world’s best formal verification platform for smart contracts and blockchain ecosystem. Founded by top formal verification experts and scientists from Yale University and Columbia University, CertiK provides the best scalable formal verification service in the market with the most competitive price.

To get a price quote for your smart contract verification, please send an email to: [email protected]