1 of 35

Demystifying Invariant Effectiveness

for Securing Smart Contracts

Zhiyang Chen¹, Ye Liu², Sidi Mohamed Beillahi¹, Yi Li², Fan Long¹

¹University of Toronto ²Nanyang Technological University

FSE 2024, Porto de Galinhas, Brazil

2 of 35

Background – Smart Contract

2

A smart contract is a self-executing program on top of blockchain.

Users interact with a smart contract by issuing transactions.

3 of 35

Background – Transaction History

3

Once deployed, a smart contract accumulates a history of transactions.

The transaction history records all past executions, and are all publicly available on chain.

4 of 35

Background - Successful Application: DeFi

4

One of successful applications of smart contracts is Decentralized Finance (DeFi).�

For example, yield-earning protocols in DeFi can automatically distribute users’ tokens to other DeFi protocols to maximize returns or interest.��But they need information such as oracle prices from external smart contracts.

Decentralized Finance (DeFi) refers to financial systems built on blockchain using smart contracts. For example, yield-earning protocols in DeFi allow users to earn interest or rewards on their digital assets by lending or staking them within these smart contracts.

Transition:

People have different DeFi protocols, using these smart contracts. Example. External Dependencies. �� There are many successful applications of smart contracts, one of the famous examples is Decentralized Finance (DeFi). For example, yield-earning protocols in DeFi allow users to earn interest or rewards on their digital assets by lending or staking them within these smart contracts. One key feature of DeFi smart contracts is composability. �� yield-earning protocols: give tokens to other protocols for better interest rate.

Need information like Oracle prices.

5 of 35

DeFi Smart Contracts as Legos

5

A Real World Example - Harvest Finance Hack

12

We collect all transactions in history of Harvest Finance victim contract, and measure them in 4 different metrics – Access Frenquency, Token Flow, Gas Consumption, Values of Special Variables

13 of 35

A Real World Example - Harvest Finance Hack

13

The hack transaction consistently emerges as an outlier in all transaction history.

We collect all transactions in history of Harvest Finance victim contract, and measure them in 4 different metrics – Access Frenquency, Token Flow, Gas Consumption, Values of Special Variables

14 of 35

Limited Trustworthiness of Users and Other DeFi Legos

14

Other DeFi Protocols

: Smart Contracts of a DeFi Protocol A

: Other Smart Contracts

Oracles

DeFi Protocol A

15 of 35

Safeguard Smart Contracts with Invariant Guards

15

Other DeFi Protocols

: Smart Contracts of a DeFi Protocol A

: Other Smart Contracts

Oracles

DeFi Protocol A

16 of 35

Smart Contract Invariants Used as Safety Guards

16

In Solidity:

// Only the owner can execute this function.

function changeOwner(address newOwner) public {

require(msg.sender == owner, "Only the owner can change ownership");

owner = newOwner;

}

17 of 35

Smart Contract Invariants Used by Practitioners

17

Conducted a qualitative study on 63 audited projects from ConsenSys, spanning from May 2020 to March 2023.�
Collected > 2000 invariants.

Categorized > 800 invariants into 8 distinct categories.

Other uncategorized invariants are either too protocol specific or not for security purposes.

18 of 35

Smart Contract Invariants Used by Practitioners

18

Category	Invariants	Count
Access Control	EOA, SO, SM, OO	283
Time Lock	SB, OB, LU	158
Gas Control	GS, GC	2
Re-entrancy	RE	12
Oracle Slippage	OR, OD	15
Special Storage	TSU, TBU	24
Money Flow	TIU, TIRU, TOU, TORU	151
Data Flow	MU, CVU, DFU, DFL	181

19 of 35

Smart Contract Invariants Used by Practitioners

19

Category	Invariants	Count
Access Control	EOA, SO, SM, OO	283
Time Lock	SB, OB, LU	158
Gas Control	GS, GC	2
Re-entrancy	RE	12
Oracle Slippage	OR, OD	15
Special Storage	TSU, TBU	24
Money Flow	TIU, TIRU, TOU, TORU	151
Data Flow	MU, CVU, DFU, DFL	181

20 of 35

Smart Contract Invariants Used by Practitioners

20

Category	Invariants	Count
Access Control	EOA, SO, SM, OO	283
Time Lock	SB, OB, LU	158
Gas Control	GS, GC	2
Re-entrancy	RE	12
Oracle Slippage	OR, OD	15
Special Storage	TSU, TBU	24
Money Flow	TIU, TIRU, TOU, TORU	151
Data Flow	MU, CVU, DFU, DFL	181

Cover 94% of all invariants categorized.

21 of 35

Selected Smart Contract Invariants

21

function deposit(uint amount) public {

require(msg.sender == tx.origin);

// …

// implement deposit

}

Access Control Invariant: EOA - isExternallyOwnedAccount

– Enforce users to interact with this contract directly, rather than through another contract.

22 of 35

Selected Smart Contract Invariants

22

bytes public _lastCallerBlock;

function deposit() public {

_lastCallerBlock = hash(tx.origin, block.number));

// implement deposit …

}

function withdraw() internal view {

require(

hash(tx.origin, block.number)!= _lastCallerBlock

);

// implement withdraw …

}

Time Lock Invariant: OB - isSameOriginBlock

– Prevent users from depositing and withdrawing tokens in the same transaction.

23 of 35

Selected Smart Contract Invariants

23

uint public tokenOutUB; �function withdraw() public{

// implement withdraw …

require(amount < tokenOutUB);

USDC.transfer(msg.sender, amount);

}

Money Flow Invariant: TOU - TokenOutUpperBound

– Restrict the maximum tokens a user can withdraw in one function call

24 of 35

Selected Smart Contract Invariants

24

uint public investedBalanceUB;

uint public totalBalanceUB;

mapping(address => uint) public balance;

function withdrawAll() public{

// implement withdraw …

uint amount = balance[msg.sender];

require( vault.investedBalance() < investedBalanceUB );

require( vault.totalBalance() < totalBalanceUB)

amount = amount * vault.investedBalance() / vault.totalBalance();

USDC.transfer(msg.sender, amount);

}

Data Flow Invariant: DFU - DataFlowUpperBound

– Restrict data flows affecting token transfers

25 of 35

Trace2Inv: Inferring Invariants from Transaction History

25

Historical Transaction

Ethereum Archive Node

EVM Trace Parser

Raw Trace structLogs:

{'pc': 0, 'op': 'PUSH1', 'gas': 71545, 'depth': 1, 'stack': []},

{'pc': 2, 'op': 'PUSH1', 'gas': 71542, 'depth': 1, 'stack': ['0x80']},

{'pc': 4, 'op': 'MSTORE', 'gas': 71539, 'depth': 1, 'stack': ['0x80', '0x40']}

Parsed Invocation Tree:

[DELEGATECALL]{gas:68985 value:0} 0xb650...9b.transfer(address: 0x830e...8c) -> True

[sload] 0xd9db...11: 0x0

[sload] 0xc067...2e: 0x0

Invariant-Related Data:

data flow: [

USDC.balanceOf(address(this)) = 10,

sload[0x2] = 20

]

msg.sender: [0x0000...8f, 0x1695...e6]

Raw Trace

Invariants:

For Function 'initialize0xCC2A9A5B':

'isSenderManager': [ '0x0000...8f', '0x1695...e6'],

'require(origin==sender)': False

Invariant-related

Data Extraction

Invocation Tree Analysis

Type Inference

Dynamic Taint Analysis

Heuristics for Invariant Generation

Invocation Tree

Invariant Related Data

Invariants

1

2

4

3

4

As we noted earlier, each invariant has some undetermined parameters. We designed and implemented a framework, Trace2Inv, aims to infer these invariants from transaction history and concretize those undetermined parameters within the invariant template. Here is our framework and an illustration of our tool.��Given a historical transaction, we provide it to the Ethereum Archive node. The Ethereum Archive node returns raw trace data, which is a list of opcodes. We then use an EVM trace parser to convert this raw EVM opcode trace into an invocation tree, which includes function calls, input arguments, return values, and storage load/store information. From the invocation tree, we can isolate the specific trace snippets related to the contracts of interest.

�Using these execution trace snippets, we apply various techniques depending on the type of invariant, such as invocation tree analysis, type inference, and dynamic taint analysis, to extract invariant-related data. Each invariant type requires different data extraction methods. For different invariant templates, we employ distinct heuristics to determine the parameters within these templates. Ultimately, we obtain all applicable invariants for each function.

26 of 35

Benchmarks of Real-World Victim Contracts

26

70% of transactions as training set

30% of transactions as testing set

42 contracts that fell victim to 27 hacks on Ethereum

On average each contract has > 8300 transactions in history before hacks

Total financial losses over 2 billion USD

27 of 35

How effective are these invariants in blocking hacks?

27

Most Effective Invariant	EOA in Access Control	OB in Time Lock	TOU in Money Flow	DFU in Data Flow
# Contracts Applied (out of 42)	42	33	34	33
# Hacks Blocked (out of 27)	15	11	17	18
Avg. False Positive Rate(%)	0.2	0	0.4	1.6

28 of 35

Does Trace2Inv outperform Other SOTA Tools?

28

Most Effective Invariant	EOA in Access Control	OB in Time Lock	TOU in Money Flow	DFU in Data Flow
# Contracts Applied (out of 42)	42	33	34	33
# Hacks Blocked (out of 27)	15	11	17	18
Avg. False Positive Rate(%)	0.2	0	0.4	1.6

InvCon+[1] (SOTA invariant mining tool)	TxSpector[2] (SOTA attack detection tool)
27	-
3	7 Detected
73.55	15.30

Comparison with Other SOTA Tools

[1] Liu, Ye, and Chengxuan Zhang. "Automated Invariant Generation for Solidity Smart Contracts." arXiv preprint arXiv:2401.00650 (2024)�[2] Zhang, Mengya, et al. "{TXSPECTOR}: Uncovering attacks in ethereum from transactions." 29th USENIX Security Symposium (USENIX Security 20). 2020.

29 of 35

Can we combine these Invariants?

29

Invariant	EOA in Access Control	OB in Time Lock	DFU in Data Flow	EOA ∧ GC ∧ DFU	EOA ∧ (OB ∨ DFU)
# Contracts Applied (out of 42)	42	33	33	42	42
# Hacks Blocked (out of 27)	15	11	18	23	20
Avg. False Positive Rate (%)	0.2	0	1.6	3.99	0.28

30 of 35

Can we combine these Invariants?

30

Invariant	EOA in Access Control	OB in Time Lock	DFU in Data Flow	EOA ∧ GC ∧ DFU	EOA ∧ (OB ∨ DFU)
# Contracts Applied (out of 42)	42	33	33	42	42
# Hacks Blocked (out of 27)	15	11	18	23	20
Avg. False Positive Rate (%)	0.2	0	1.6	3.99	0.28

31 of 35

What about Gas Overhead of Invariant Guards?

31

Invariant	EOA in Access Control	OB in Time Lock	DFU in Data Flow	EOA ∧ GC ∧ DFU	EOA ∧ (OB ∨ DFU)
# Contracts Applied (out of 42)	42	33	33	42	42
# Hacks Blocked (out of 27)	15	11	18	23	20
Avg. False Positive Rate (%)	0.2	0	1.6	3.99	0.28
Avg. Gas Overhead¹ (%)	0.01	0.21	0.01	0.03	0.22

^{1: Results based on 4 selected case studies.}

32 of 35

Takeaways

32

The first comprehensive study on the effectiveness of practical invariants in the victim contracts of real-world hacks.

To facilitate our study, we built Trace2Inv, a fully open-sourced tool designed for transaction trace analysis and dynamic invariant inference.

Our experiment results show some invariants are highly effective, with low false positive rates and minimal gas overhead.

33 of 35

Thank you! Q&A

33

Website: https://sites.google.com/view/trace2inv/

Paper: https://jeffchen006.github.io/pdfs/Chen2024DIE.pdf

Extended Paper: https://arxiv.org/abs/2404.14580�

Invariant Study Results: https://github.com/Trace2Inv-Artifact/Trace2Inv-Invariant-Study-FSE24

Benchmarks: https://github.com/Trace2Inv-Artifact/Trace2Inv-Benchmarks

Artifact: https://github.com/Trace2Inv-Artifact/Trace2Inv-Artifact-FSE24

Tool Demo: https://github.com/jeffchen006/OpenTracer

Tool Paper: https://arxiv.org/abs/2407.10039

Contact: zhiychen@cs.toronto.edu

Battle Tested!

34 of 35

Early Experience and Insights

34

Q: What if a normal user gets blocked by the invariants?� It could be quite easy for normal users to bypass these invariants by splitting their transactions into smaller ones.

Q: Could you give an example?

Suppose a smart contract sets an invariant with TokenOutUpperBound ≤ 100k tokens, and a user wants to withdraw 1M tokens. The user can simply split this into 10 transactions, each withdrawing 100k tokens.

Q: Can a hacker mimics what normal users do to bypass the invariants?�Hackers usually encounter more difficulties in bypassing the invariants.

If they attempt to perform the attack vector through multiple transactions, other participants on the blockchain, such as MEV bots, can potentially insert transactions in between the hack transactions and exploit this situation for arbitrage.

35 of 35

Early Experience and Insights

35

4. Q: But aren't the complex invariant guards still gas expensive?

There's a new opportunity!

Ethereum has accepted EIP-1153[1], which introduces transient storage. This can significantly reduce gas costs for invariants that need to temporarily store values during a transaction.

5. Q: Is your data/tool fully open-sourced?� Yes! Links are provided in the last slide.

We believe our tool can assist future researchers in studying other invariants and testing them on historical transactions.

^[1]^{https://eips.ethereum.org/EIPS/eip-1153}