Automated Security Testing

SecScan

Introduction

In the world of blockchain, Token is a concept symbolizing different assets that drive decentralized finance. When tokens are implemented as smart contracts, they follow specific standards to ensure unified manipulation, such as making token transfer between addresses. The well-known established standards include ERC-20, ERC-721. However, adhering to a token standard never guarantees the "merit" of a token. Some token owner would insert some malicious behaviors in the token implementations, resulting in token holders being unable to enjoy their rightful asset benefits.

Worse, the malicious tokens deliberately disguise themselves by employing various tricks to conduct their maclious behaviors. Even a seasoned contract security engineer would require significant time to distinguish such issues. In reponse to the severe situation, we introduces SecScan, an automatic solution based on cutting-edge static analysis techniques. Overall, SecScan accepts ERC-20 tokens of any solidity versions and detects malicous behaviors. The detection process is both efficient, completing in under three seconds per token, and effective.

Next, we delve into the inner operations of SecScan. For each input program, we first construct our Intermediate Representation (GIR) from the solidity compiler. Our IR namely GIR, shares the same spirit as program dependence graph. It not only encompasses various dependency information such as data-, control-, and order dependencies, but also provides a comprehensive depiction of these dependencies. Specifically, our data dependence analysis is enhanced with static single assignment form and field sensitive alias analysis, And we have further captured the implicit control dependencies introduced by features such as revert statements, and function modifiers. Subsequently, we employ value flow analysis on the ERC-20 interfaces of the contract to identify different financial concepts, such as balance variables, to enhance GIR. Such financial concept identification enables us to comprehend token behaviors at a high level.

On this powerful GIR, we conduct various kinds of detection for malicious token behaviors, such as abnormal tax modification, minting, and blacklist. A portion of the malicious behaviors is modeled as value flow reachability problem. In this case, we have developed a highly productive value flow engine that abstracts many program details, such as deep function call chains, enabling users to describe malicious behavior at its core. To further enhance productivity, we leveraged Large Language Model (LLM) to help us in writing these checkers. As for the malicious behaviors involving numerical values, we address them strictly with constraint solving. Specifically, the behaviors of a token is encoded into symbolic constraints, while the malicious behaviors are encoded as predicates to check. This crucially guarantees our high precision.

SecScan has identified a significant number of malicious behaviors across various aspects and is continuously ensuring the security of users in investment contracts.