How CertiK's Formal Verification Engine Could Have Detected ICX's EnableTokenTransfer Issue

On Jun 16th 2018, reports have emerged that a bug was found in the ICON smart contract code. This error was exploited by malicious actors to disable ICX token transfer, which halted thousands of transactions. Though the hackers can't leverage this bug to steal ICX tokens, the issue can still affect the functionality of the network for token holders, damage the reputation of the project, and require the ICON team to spend a significant amount of resources in damage control.

What was the vulnerability in ICON's smart contract code?

Within the ICX token contract, there's a function to enable and disable the transfer of ICX tokens between token holders. The original intent of this function was to allow only the owner of the ICX contract to have permissions to invoke it. However, the function was implemented in reverse, so instead, everyone else other than the contract owner had permissions to enable or disable the transfer of ICX tokens.

Let's take a look at the smart contract code:

require(msg.sender != walletAddress)—this is wrong!

For logical operators, != means "not equal to", == means "equal to". Clearly, this line of code should be written in such correct way:

require(msg.sender == walletAddress);—this is right!

This type of bugs (a result of a simple typo, in this case) is simple, but it can be a meticulous task to have to manually check for them when you're looking in a larger pile of code. Traditional manual tests that are usually employed are labor intensive, time consuming, and prone to human errors.

How can we detect this bug using CertiK's Formal Verification Engine?

Above is a short demo video illustrating the verification process using our proprietary Formal Verification Engine. It outputs the bug as well as a counterexample that violates the specification of the code.

If ICON had utilized CertiK's services to verify its smart contracts, the bug would have been identified and fixed before its release.

Since the bug was detected, the ICON team has issued a statement and has already begun to mitigate the impact. You can also read ICX's source code on Etherscan.

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