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

TL;DR

This paper proposes modifications to the EVM and Ethereum clients to enable real-time validation of transaction trace properties in smart contracts, enhancing security against certain hacks without impacting traditional execution.

Contribution

It introduces EVM modifications and formalizes trace properties using PLTL, allowing real-time security checks that were previously impractical due to EVM limitations.

Findings

Enables real-time transaction trace validation in smart contracts.

Formalizes trace properties using past-time linear temporal logic.

Potential to significantly improve smart contract security.

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.