Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Zhiyang Chen, Jan Gorzny, Martin Derka

TL;DR

This work addresses the gap between effective off-line transaction-malicious-detection and real-time prevention of hacks in smart contracts, which is currently limited by the EVM's inability to access prior transaction traces. It proposes extending the EVM and Ethereum clients to support real-time validation of transaction trace properties using Past-time Linear Temporal Logic (PLTL), showing that many real-world detectors can be expressed in PLTL and implemented as runtime checks via injected hooks. The paper details concrete safety properties (e.g., flashloan usage, re-entrancy, TVL changes), formalizes PLTL with past-time and quantifiers, and outlines an architectural path (HOOK opcode, tracer module, modified EVM) to enforce these properties with manageable overhead. The approach promises to significantly improve on-chain security by blocking malicious transactions before they execute, with practical deployment considerations across nodes and rollups and avenues for future refinement.

Abstract

In the realm of smart contract security, transaction malice detection has been able to leverage properties of transaction traces to identify hacks with high accuracy. However, these methods cannot be applied in real-time to revert malicious transactions. Instead, smart contracts are often instrumented with some safety properties to enhance their security. However, these instrumentable safety properties are limited and fail to block certain types of hacks such as those which exploit read-only re-entrancy. This limitation primarily stems from the Ethereum Virtual Machine's (EVM) inability to allow a smart contract to read transaction traces in real-time. Additionally, these instrumentable safety properties can be gas-intensive, rendering them impractical for on-the-fly validation. To address these challenges, we propose modifications to both the EVM and Ethereum clients, enabling smart contracts to validate these transaction trace properties in real-time without affecting traditional EVM execution. We also use past-time linear temporal logic (PLTL) to formalize transaction trace properties, showcasing that most existing detection metrics can be expressed using PLTL. We also discuss the potential implications of our proposed modifications, emphasizing their capacity to significantly enhance smart contract security.

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

TL;DR

This work addresses the gap between effective off-line transaction-malicious-detection and real-time prevention of hacks in smart contracts, which is currently limited by the EVM's inability to access prior transaction traces. It proposes extending the EVM and Ethereum clients to support real-time validation of transaction trace properties using Past-time Linear Temporal Logic (PLTL), showing that many real-world detectors can be expressed in PLTL and implemented as runtime checks via injected hooks. The paper details concrete safety properties (e.g., flashloan usage, re-entrancy, TVL changes), formalizes PLTL with past-time and quantifiers, and outlines an architectural path (HOOK opcode, tracer module, modified EVM) to enforce these properties with manageable overhead. The approach promises to significantly improve on-chain security by blocking malicious transactions before they execute, with practical deployment considerations across nodes and rollups and avenues for future refinement.

Abstract

In the realm of smart contract security, transaction malice detection has been able to leverage properties of transaction traces to identify hacks with high accuracy. However, these methods cannot be applied in real-time to revert malicious transactions. Instead, smart contracts are often instrumented with some safety properties to enhance their security. However, these instrumentable safety properties are limited and fail to block certain types of hacks such as those which exploit read-only re-entrancy. This limitation primarily stems from the Ethereum Virtual Machine's (EVM) inability to allow a smart contract to read transaction traces in real-time. Additionally, these instrumentable safety properties can be gas-intensive, rendering them impractical for on-the-fly validation. To address these challenges, we propose modifications to both the EVM and Ethereum clients, enabling smart contracts to validate these transaction trace properties in real-time without affecting traditional EVM execution. We also use past-time linear temporal logic (PLTL) to formalize transaction trace properties, showcasing that most existing detection metrics can be expressed using PLTL. We also discuss the potential implications of our proposed modifications, emphasizing their capacity to significantly enhance smart contract security.
Paper Structure (15 sections, 5 equations, 2 figures)

This paper contains 15 sections, 5 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Related Work
  3. Smart Contract Safety Property Runtime Validation
  4. Transaction Trace Properties for Malice Detection
  5. Linear Temporal Logic for Smart Contract Formal Specification
  6. Motivating Example
  7. Challenges for Runtime Validation
  8. Example Safety Properties
  9. Logic
  10. Expressing Real-world Transaction Trace Properties with Past-Time Linear Temporal Logic
  11. Extending EVM to Check Transaction Trace Properties
  12. EVM Execution Modifications
  13. Use Cases
  14. Overhead Analysis
  15. Conclusion

Figures (2)

  • Figure 1: The dForce incident, illustrated. The entire exploit takes place during a single transaction on Arbitrum. The view function get_virtual_price() is accessed when executing the remove_liquidity() function, and is used as an oracle by dForce.
  • Figure 2: Modified Geth client to support checking transaction trace properties. The client is extended with a new module that allows smart contracts to check transaction trace safety properties. The module is responsible for maintaining the state of the contract and checking the properties. The module is triggered by hooks in the EVM execution.

Theorems & Definitions (1)

  • Definition 5.1: $PLTL$