On May 23rd, 2018, a new bug was found in an EduCoin smart contract, causing more than 2 billion EDU tokens to go missing from several exchanges. EduCoin reached a market capitalization of $0.00 in the last 24 hours.
What was the vulnerability in the EduCoin smart contract?
Let’s focus on the transferFrom function, which, as its name suggests, transfers a fixed value (line 1, _value) from a given address (line 1, _from) to another address (line 1, _to)：
However, this function does not check if this transfer is allowed or not:
allowed[_from][msg.sender] -= _value; // bug!
Without validating whether the amount of tokens specified is within a transferable limit (allowed[_from][msg.sender]), an integer overflow may occur, allowing a negative value for the function allowed[_from][msg.sender]. This gives hackers the ability to transfer EDU tokens from any address to their own address, and as a result, more than 2 billion EDU tokens have been stolen. Hypothetically, hackers could ransack all EDU holders by exploiting this existing bug.
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 generated by CertiK’s formal verification engine in only 24.9ms:
The entire verification process takes seconds to complete and outputs a full report with the bug detected as well as providing a counterexample that breaks the specification, proving the existence of the overflow bug.
Had EduCoin had their smart contracts verified by CertiK, the bug would have been detected and fixed before its release.
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
