Can 'Unchecked K-value Issues' be Detected by Tools?

01  Beosin-VaaS: Improving the security of smart contracts for developers

As the industry-leading company specializing in blockchain security, Beosin is one of the world's first experts to apply formal verification technology to smart contract security audit, with more than 20 years of experience in formal verification. VaaS is a highly automated security detection tool for smart contracts with 97% accuracy, which can automatically detect hundreds of security issues of smart contracts in "one click".

Recently Beosin summarized a rich library of smart contract security issues through in-depth analysis of a large number of different business scenarios, and we also extracted the contract information of a total of 140K addresses on ETH and BSC through the formal verification tool VaaS, and found that these address may have K-value validation issues. Today, we will explain the K-value validation issue and give professional fix recommendations.

02  What is a K-value validation issue?

Since the actual exchange and transfer operation of Uniswap DEX is implemented in the swap() function of Pair, in order to prevent an attacker from bypassing the Router contract and directly calling the Pair contract for swap() transfer, a K-value check needs to be performed in the swap() function of the Pair contract, i.e., the K-value in the pair remains constant after swapping. If there is a security vulnerability in the code related to the K-value check, then an attacker can swap out a large amount of tokens from Pair using a minimum amount. We will explain this with a case study below.

Example: swap function does not check the K value

The core of Uniswap is the constant product model K=x*y, where the K value is the product of the number of tokens held by the pair contract, and it is required that the K value must increase after each subsequent transaction is completed (considering the fee). Therefore, without K-value verification, it will easily become a target by hackers.

Take the Impossible Finance event as an example. This is a Uniswap-like project which implements two functions for swapping tokens: cheapSwap and swap, where the CheapSwap function lacks K-check (as shown below), but the project is aware of the consequences of missing the K-check and has added the onlyIFRouter modifier to restrict the cheapSwap function to be called only by the specified Router contract.

Under normal circumstances, when a user redeems tokens using a Router contract, the getAmountsOut function is first used to calculate the correct tokens amounts; then safeTransferFrom is called to transfer the user's redeemed consumed tokens to the target pair contract; and finally, the internal call to _swap function is used to execute the cheapSwap function to transfer the redeemed tokens to the target address.

However, since the cheapSwap function lacks a K-value validation, if an attacker deploys a malicious token contract and calls back the normal pair contract for swapping when the safeTransferFrom function is called by the Router contract, the target tokens can be swapped out at a wrong price, as the amounts used for swapping after the callback are still not updated and no longer meet the validation after changing the state of the ledger.

03  VaaS scanned 140K contracts and find two contracts with such vulnerability

We summarized the characteristics of the K-value validation problem and extracted the generic properties of the problem for detection by Beosin-VaaS. After that, we extracted 140K contract addresses on ETH and BSC by analyzing the node information. All of these contracts are similar business contracts, which may have potential K-value validation problems. Beosin-VaaS tested all these addresses and finally found two contracts with this unchecked K-value vulnerability.

*Some details are hidden

Both contracts are with a mismatch between the left and right ratios in K-value validation: 10,000 on one side and 1,000 on the other, which can lead to security vulnerabilities.

04  Beosin-VaaS: Achieving real pre-warning to avoid getting hacked

For such security issues, Beosin security team recommends that proper K-value checks must be done in critical swap functions, and don't depend on external validation for K-value checks and security validation just to save gas and code volume.

For project devs, if such vulnerabilities can be detected by an automated tool, the risk of being hacked after going live will be greatly minimized.  

Beosin VaaS product provides static scanning, fuzzy testing, and formal verification capabilities for smart contract codes. The platform supports 140+ defined testing cases, including traditional vulnerabilities and business logic correctness on multiple public blockchains such as ETH, BSC, MATIC, AAVE, ONT, EOS, etc. It can precisely locate the risky codes with an above 97% accuracy rate and give recommendations to help developers improve their smart contracts’ security.