How CertiK Formal Verification Engine Could Help ICON Detect ICX EnableTokenTransfer Issue

On Jun 16th 2018, reports have emerged that a bug was found in the ICON smart contract code. This error is being exploited by malicious actors to disable ICX token transfer, which could halt thousands of transactions. Though the hackers cannot 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 ICON team to spend a significant amount of efforts in damage control.

What Happened?

Let’s try explore, in layman’s terms, the specifics around the issue. Within the ICX token contract, there is a function to enable/disable the transfer of ICX tokens amongst token holders. The original intent of this function was to allow only the owner of the ICX contract to have the permissions to invoke it. However, the function was implemented in a reverse manner. Therefore, instead of the permission to invoke the function being limited to the owner of the ICX contract, it then enabled everyone other than the owner to have permission to enable/disable the transfer of ICX tokens.

Now let’s focus on the real code:

require(msg.sender != walletAddress); // 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); // right!

These types of bugs are usually straightforward in hindsight, because you have a better idea of which specific areas of the code to focus on. But this is both a difficult and meticulous task when you’re trying to locate it from a pile of codes during a holistic QA check. Traditional testings in identifying such issues are labor intensive, time consuming, and also prone to human errors.

How to detect this bug using CertiK?

Above is a short demo video illustrating the verification process with the bug detected and a straightforward counter-example that violates the specification. If ICON had utilized the CertiK platform to conduct a verification of the contract , the bug would have been identified and fixed before its release.

This is where CertiK’s Formal Verification Engine can provide tremendous value, by leveraging smart labels to the source code, such bugs can be easily identified in milliseconds.

The ICON team has recognized the issue and started to mitigate the impact at earliest time, read here to get more details: https://medium.com/helloiconworld/official-statement-regarding-erc20-icx-transfer-error-94a9fc9d69c3

To read the ICX source code: https://etherscan.io/address/0xb5a5f22694352c15b00323844ad545abb2b11028#code

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.

Telegram: https://t.me/certikorg
Twitter: https://twitter.com/certikorg
Email: info@certik.org