Creating a safe Ethereum smart contract that is free of exploitable bugs is much harder than it sounds. Researchers have discovered in March 2018 that over 34,000 Ethereum smart contracts may be vulnerable to exploitation.
In the recent discovery of an exploit in a Beauty Ecosystem Chain (BEC) smart contract, an overlooked loophole in just one line of code that could have led in a market cap drop to near-zero.
What was the vulnerability in the BEC smart contract?
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 had a common integer overflow problem:
uint256 amount = uint256(cnt) * _value;
This overflow gave hackers a chance to withdraw more than the balance of an account. By using a dynamic array of two addresses and a value of 2²⁵⁵ to abuse the vulnerable contract, hackers successfully transferred 2²⁵⁶ tokens to their accounts, a transaction viewable on Etherscan.
How can CertiK's audit process detect this bug automatically?
This type of bugs are usually simple and straightforward, but that's an assessment that's done in hindsight—after code has been implemented and, in some unfortunate situations, exploited. Imagine trying to spot such a small, bothersome piece of code within hundreds (and sometimes even thousands) of lines!
But what if there was a way for bugs like these to be easily tracked down automatically? CertiK has developed special Formal Verification technology that can catch bugs and errors that humans may miss.
Below is a screenshot of a sample report that is automatically generated by our Formal Verification Engine:
We've 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 program. In BEC's sample code, the entire verification process would take seconds to complete as well as provide clear counterexamples that break the specification, proving the existence of the overflow bug.
If, for instance, Beauty Chain had their contract verified by CertiK, the billion-dollar loss would have been avoided entirely.
About CertiK
CertiK leads blockchain security by pioneering the use of cutting-edge Formal Verification technology on smart contracts and blockchains. Unlike traditional security audits, Formal Verification mathematically proves program correctness and hacker-resistance. CertiK was founded by Computer Science professors of Yale University and Columbia University, securing billions in assets, including many of the world’s top projects.
The research efforts of CertiK have received grants from IBM and the Ethereum Foundation, and notable investors include Binance Labs, Bitmain, Lightspeed Venture Partners, Matrix Partners, and NEO Global Capital, among others.
To request an audit or verification of your smart contracts, please email us at mailto:audit@certik.io or visit certik.io
Follow us on social
Twitter: https://twitter.com/CertiKCommunity
Reddit: https://www.reddit.com/r/CertiKOrg/
Telegram: https://t.me/certikorg
LinkedIn: https://www.linkedin.com/company/certik
