Enhancing Web3 Dapp Security: A Deep Dive into MetaTrust Prover's Advanced Verification

Understanding MetaTrust Prover

MetaTrust Prover, the security scanning engine developed by AI security service provider MetaTrust Labs, stands as an advanced tool revolutionizing the formal verification of Solidity smart contracts. Its features are tailored to meet the intricate demands of Web3 Dapp development, offering a meticulous approach to source-code-centric verification. Let's delve into the key features.

Key Features of Prover

Discover how Prover's source-code-centric approach, Solidity-style specification language, automated property recommendations, and comprehensive verification reports elevate the standards of Web3 Dapp security.

1. Source-Code-Centric Formal Verification

Employing formal methods to scrutinize and validate the source code of smart contracts, Prover establishes a robust foundation for ensuring correctness and reliability. This approach, in contrast to existing methods, focuses on mathematical proofs of adherence to specified requirements, departing from traditional byte-code-oriented verification.

2. Solidity-Style Specification Language

Facilitating a straightforward specification process, Prover supports a specification language reminiscent of Solidity. Developers can easily articulate function pre/post-conditions, contract invariants, and advanced rule-based properties. Simplifying the writing of specifications equates to crafting more accessible and concise contracts.

3. Automated Property Recommendations

Leveraging a fine-tuned GPT model named propertyGPT, Prover automatically suggests high-quality specification candidates. Users can confirm these recommendations without having to manually draft specifications, streamlining the verification of contract correctness. This automated approach enhances efficiency and accessibility.

4. Comprehensive Verification Reports

Prover generates mathematical proofs and thorough Proof of Concepts (PoCs) for implementation bugs, fostering confidence in the contract code. This comprehensive report not only validates correctness but also aids developers in pinpointing and rectifying faults in the contract implementation, contributing to an efficient development process.

Real-World Application: Incident Overview

Incident Overview

On October 4, 2023, the cryptocurrency token named $888 suffered a security breach, resulting in a loss of $9.8K. The attack exploited a logic issue within the _transfer function, allowing the attacker to double their balance by setting the token recipient account as himself.

Hack Transaction Link: https://bscscan.com/tx/0x8459fd362d54b33bbb97454b36b8886757890d87d3c25827fc23647caf19537c

Token Specification for Prover Scan

The Prover tool was utilized to scan the Token contract, employing a custom language extending Solidity grammar. The specifications covered invariants, rules, and function pre/post-conditions, revealing vulnerabilities in the _transfer function.

1pragma solidity ^0.8.6;
2contract Token {
3    invariant inv1 {
4        _totalSupply == __sum__(_balances);
5    }
6
7    rule EqualizationOfTransferBalancesFullSymbol() {
8        address $to;
9        uint256 $init_balance;
10        _balances[msg.sender] = $init_balance;
11        uint256 balanceBefore = _balances[$to];
12        uint256 $amount;
13        transfer($to, $amount);
14
15        if (msg.sender != $to) {
16            assert((balanceBefore + $amount) == _balances[$to]);
17        } else {
18            uint256 balanceAfter = _balances[$to]；
19            assert(balanceBefore == balanceAfter);
20        }
21    }
22}
1pragma solidity ^0.8.6;
2contract Token {
3    invariant inv1 {
4        _totalSupply == __sum__(_balances);
5    }
6
7    rule EqualizationOfTransferBalancesFullSymbol() {
8        address $to;
9        uint256 $init_balance;
10        _balances[msg.sender] = $init_balance;
11        uint256 balanceBefore = _balances[$to];
12        uint256 $amount;
13        transfer($to, $amount);
14
15        if (msg.sender != $to) {
16            assert((balanceBefore + $amount) == _balances[$to]);
17        } else {
18            uint256 balanceAfter = _balances[$to]；
19            assert(balanceBefore == balanceAfter);
20        }
21    }
22}

Specification Violation

Both the invariant (inv1) and the rule (EqualizationOfTransferBalancesFullSymbol) were violated due to logic bugs within the _transfer function. The violated conditions specifically relate to the equality check: assert(balanceBefore == balanceAfter);.

Buggy Token Code Analysis

The Buggy Token Code contains the relevant code snippet with the introduced vulnerabilities. https://bscscan.com/address/0x0529ce778b5a4ab9a80b9935a3214b870b003469#code

Prover Scan Report

Upon scanning the contract with Prover, the report highlighted the violation condition: assert(balanceBefore == balanceAfter);. Further details from the "Rule Call Resolutions" section indicated that the violation occurs when msg.sender is equal to $to.

The relevant values during the transaction were:

• senderAmount (initial balance of msg.sender): 20,000

• recipientAmount (initial balance of $to): 20,000

• After _balances[sender] = senderAmount.sub(amount);, _balances[sender] became 19,900

• After _balances[recipient] = recipientAmount.add(amount);, _balances[recipient] became 20,100

As a result, the final assertion assert(balanceBefore == balanceAfter); was violated.

Tool Comparison

In contrast to other products like Cetora, MetaTrust Prover demonstrated its effectiveness with a simpler architecture, direct source-code-level operation, and a tailored Solidity-style specification language. By seamlessly integrating the real-world incident into the discussion of MetaTrust Prover's features and advantages, we showcase how the tool naturally addresses and mitigates security vulnerabilities in Web3 Dapp development.

Advantages of Prover

MetaTrust Prover emerges as a trailblazer in securing Web3 Dapp development, showcasing unparalleled advantages through a real-world case. With a foundation of six years of extensive research, Prover delivers expert formal verification analysis tailored specifically for smart contracts. Its pioneering capability of conducting strict semantic analysis at the source-code level, as evidenced in the incident on October 4, 2023, establishes Prover as the world's first tool to delve deep into Solidity semantics. This unique prowess stems from a profound understanding of the intricacies of smart contract languages. Moreover, Prover's fully automated formal verification process not only streamlines the verification journey but also enhances efficiency and accuracy by autonomously generating high-quality specifications. Coupled with a user-friendly design that ensures a minimal learning curve, Prover empowers developers to fortify their smart contracts with confidence, mitigating risks and advancing the security landscape of decentralized applications.

Conclusion

In the rapidly evolving landscape of Web3, where the security of smart contracts is paramount, MetaTrust Prover emerges as an indispensable asset for developers and security experts. In an industry where trust and reliability are critical, MetaTrust Prover stands as a cornerstone, empowering developers to navigate the complexities of smart contract security with confidence, ultimately fortifying the foundation of the Web3 ecosystem.

About Us

At MetaTrust, our primary focus is on creating a secure infrastructure that caters to the needs of developers in the WEB 3.0 space. We offer an array of AI-Driven automation tools and security services to assist Web3 developers and project stakeholders in achieving a secure development environment.

Website || Twitter || Telegram || Try Prover Now