1 of 20

Instrumenting Transaction Trace Properties in Smart Contracts: �Extending EVM for Real-Time Security

Zhiyang Chen, Zircuit & University of Toronto

Jan Gorzny, Zircuit

Martin Derka, Zircuit

{jeff, jan, martin}@zircuit.com�

March, 2025. SANER IWBOSE 2025

2 of 20

Growing DeFi

2

3 of 20

But also growing security incidents

3

4 of 20

Security incidents in 2025 (Until 22 Feb, 2025)

Name	Date	Classification	Technique	Amount lost	Language
Bybit	21 Feb, 2025	Protocol Logic	Safe Multisig wallet Phishing	$1.4b	Solidity
Cardex	18 Feb, 2025	Infrastructure	Private Key Compromise	$0.4m	Solidity
Four.Meme	11 Feb, 2025	Protocol Logic	Liquidity Pool Exploit	$0.183m	Solidity
zkLend	11 Feb, 2025	Protocol Logic	Empty Market Exploit	$9.55m	Cairo
Ionic Protocol	4 Feb, 2025	Protocol Logic	Fake Collateral Exploit	$4m	Solidity
DogWifiTools	28 Jan, 2025	Infrastructure	Private Key Compromise	$10m	Move

5 of 20

However, detection is so successful

6 of 20

Almost all hacks detected

7 of 20

Almost zero false positives

8 of 20

Detection metrics are even open-sourced

Idle finance: https://app.forta.network/agents/idle�

i. Deposit or redeem with flashloan

ii. Detect if the tokenPrice of any IDLE token has decreased �

iii. Large change in TVL �

iv. Big deposit or redeem

9 of 20

Detection is so successful!

High Accuracy
Low False Positive Rate

Protection is so unsuccessful!

Frequent Security Incidents
High Financial Loss

10 of 20

Detection is so successful!

High Accuracy
Low False Positive Rate

Protection is so unsuccessful!

Frequent Security Incidents
High Financial Loss

Why DeFi protocol cannot instrument these detection metrics directly in their protocol to stop hack transactions on the fly?

11 of 20

Challenges:

Limitations of EVM
Cannot define complicated transaction properties

2. High Gas Fee

12 of 20

Example: dForce attack

Curve.Fi gets re-entered, but dForce is the victim.

13 of 20

Which detection metrics may have worked?

i. Re-entrancy Detection

ii. Flashloan Detection�

iii. Large change in TVL

Yes!

14 of 20

Can they be used to stop the hack?

i. Re-entrancy Detection

ii. Flashloan Detection�

iii. Large change in TVL �

No. EVM Limitations

Yes. With high gas cost.

15 of 20

Solution: Allow Defining Properties Over Trace

16 of 20

Solution: Logic to All History States

Initial world state (Genesis)

Hook

A logic that can define properties over all past state transitions (transactions)

17 of 20

Solution: Past-time Linear Temporal Logic(PLTL)

X: next

U: until

S: since

X^{-1}: previously

18 of 20

Solution: Expressiveness of PLTL

We systematically collected 188 Forta attack detectors.

42 can be used for instrumentation within EVM (potentially with high gas cost)

186 detectors can be expressed using PLTL

144 detectors can be expressed by PLTL but cannot be used for instrumentation within EVM (including flash loan detection and re-entrancy detection)

2 detectors that cannot be expressed using PLTL.

The first involves checking the Matic price
The second involves checking pending transactions in mempool

19 of 20

Other Ongoing Works

Their Whitepaper:

https://github.com/phylaxsystems/credible-layer-whitepaper/blob/main/ajax_0.1.pdf

The Phylax Credible Layer https://phylax.systems/

Assertion Enforcement

Assertions are enforced at the sequencer level, meaning they can’t be bypassed.

Write in assertions in Solidity with no code changes, redeployment, or downtime for your protocol when signing up. Also: no false positives as you only prevent states you define.

20 of 20

Conclusions

EVM Extension: We propose an innovative solution that extends EVM to support the definition and real-time validation of trace properties over the complete transaction trace, aiming to halt or suspend malicious transactions on the fly.�
PLTL Utilization: We introduce a formalism of trace properties using past-time linear temporal logic.�
Proactive Security: We discuss possible practical use cases, potential impacts, and prospective directions for future research