How Formal Verification Would Have Prevented the Stolen of 2 Billion EduCoin
On May 23rd, a new bug was found in EduCoin’s smart contract, prompting several exchanges to result in more than 2 billion EDU tokens missing. EduCoin reaches market capitalization of $0.00 over last 24-hour.
Let’s briefly review this incidence and see how CertiK’s formal verification engine detected the issue by one click.
What Happened
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 that the amount of tokens that is allowed to be transferred (allowed[_from][msg.sender]), an overflow may occur and make allowed[_from][msg.sender] to be negative. This gives hackers the ability to transfer EDU tokens from any addresses to their own address and more than 2 billion EDU tokens have been stolen since May 23, 2018. Hypothetically, the hackers could ransack all EDU holders by exploiting this existing bug.
How to detect this bug automatically using CertiK?
These types of bugs are usually straightforward in hindsight. But not quite so when you try to locate it from a pile of codes.
What if I tell you that this bug can be easily tracked down by “one click” using CertiK? Below is a screenshot of a sample report that generated by CertiK’s formal verification engine in only 24.9ms:
The entire verification process completes in seconds with the bug detected and a straightforward counter-example that violates the specification. If, for instance, EduCoin had their contract verified by CertiK, the bug would have been fixed before its release.
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. 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.
Please follow CertiK on telegram: https://t.me/certikorg. To get a price quote to verify your smart contract, feel free to send an email to: info@certik.org
