In this work we propose Dynamit, a monitoring framework to detect reentrancy vulnerabilities in Ethereum smart contracts. The novelty of our framework is that it relies only on transaction metadata and balance data from the blockchain system; our approach requires no domain knowledge, code instrumentation, or special execution environment. Dynamit extracts features from transaction data and uses a machine learning model to classify transactions as benign or harmful. Therefore, not only can we find the contracts that are vulnerable to reentrancy attacks, but we also get an execution trace that reproduces the attack. Using a random forest classifier, our model achieved more than 90 percent accuracy on 105 transactions, showing the potential of our technique.

Smart contracts manage blockchain assets and embody business processes. However, mainstream smart contract programming languages such as Solidity lack explicit notions of roles, action dependencies, and time. Instead, these concepts are implemented in program code. This makes it very hard to design and analyze smart contracts. We argue that DCR graphs are a suitable formalization tool for smart contracts because they explicitly and visually capture the mentioned features. We utilize this expressiveness to show that many common high-level design patterns representing the underlying business processes in smart-contract applications can be naturally modeled this way. Applying these patterns shows that DCR graphs facilitate the development and analysis of correct and reliable smart contracts by providing a clear and easy-to-understand specification.

Decentralized Finance (DeFi) systems leverage blockchain oracles to access off/on-chain data as a service. Therefore, maintaining the integrity of oracle data is essential. However, the integrity of these oracles data can be compromised through different attacks, and the effectiveness of these attacks varies depending on the specific stage of the oracle’s lifecycle. This work presents a comprehensive analysis of this lifecycle, identifying potential attack types and examining the efficacy of existing defense mechanisms. We propose a generalized model encompassing data creation, submission, consensus, election, and deprecation stages. We evaluate our model against seven recent high-profile DeFi exploits totaling $ 187 million. We have also studied bond systems as a preventive measure against at least a subset of oracle exploits. Our findings suggest that while bond systems increase the cost of attacks, thereby fortifying oracle data integrity against adversarial manipulations, they also require careful calibration to avoid hindering honest participation.

Logical flaws in smart contracts are often exploited, leading to significant financial losses. Our tool, HighGuard, detects transactions that violate business logic specifications of smart contracts. HighGuard employs dynamic condition response (DCR) graph models as formal specifications to verify contract execution against these models. It is capable of operating in a cross-chain environment for detecting business logic flaws across different blockchain platforms. We demonstrate HighGuard's effectiveness in identifying deviations from specified behaviors in smart contracts without requiring code instrumentation or incurring additional gas costs. By using precise specifications in the monitor, HighGuard achieves detection without false positives. Our evaluation, involving 54 exploits, confirms HighGuard's effectiveness in detecting business logic vulnerabilities. Our open-source implementation of HighGuard and a screencast of its usage are available at: https://github.com/mojtaba-eshghie/HighGuard https://www.youtube.com/watch?v=sZYVV-slDaY

Many smart contracts are prone to exploits, which has given rise to analysis tools that try to detect and fix vulnerabilities. Such analysis tools are often trained and evaluated on limited data sets, which has the following drawbacks: 1. The ground truth is often based on the verdict of related tools rather than an actual verification result; 2. Data sets focus on low-level vulnerabilities like reentrancy and overflow; 3. Data sets lack concrete exploit examples. To address these shortconUngs, we introduce XruiGEN, which uses a model-based oracle specification of the business logic of the smart contracts to synthesize valid exploits using LLMs. Our experiments, involving 104 synthesized vulnerability-exploit pairs, demonstrated a 57% success rate in exploiting targeted aspects of the contract. They achieved exploit efficiency with an average of only 3.5 transactions per exploit, highlighting the effectiveness of our methodology.

Smart contracts manage blockchain assets and embody business processes, yet mainstream languages lack explicit support for process concepts like roles, action dependencies, and time constraints leading to implementation complexity and analysis challenges. To address this, we utilize Dynamic Condition Response (DCR) graphs, a formal business process modeling language to formalize business logic semantics of smart contracts. Modeling smart contracts in DCR graphs involves translating its underlying behavioral logic—the "what" it does, not the "how" it is implemented in detail—into a declarative visual model using DCR's explicit constructs for events, roles, data, time, and inter-event relationships. Furthermore, we systematically model 15 common high-level smart contract design patterns, representing recurring solutions for business logic-level problems. These formalizations reduce ambiguity compared to informal descriptions, and serve as language-independent specifications. We demonstrate modeling process using three complete smart contract case studies, combining six design patterns. Our modeling methodology and formlizations enable future automated analysis and verification.

We propose a "Model to Mitigate" methodology: designing a platform-agnostic model of smart contract business logic and analyzing it before implementation. Using Dynamic Condition Response (DCR) graphs—originally for modeling business processes—we formally specify smart contracts. Our method captures high-level properties like event ordering, role-based access control, and time constraints to prevent design-rooted vulnerabilities. While we verify our approach on existing smart contracts (i.e., post-implementation scenarios), the proposed methodology is applicable during design time (pre-development). Our method applied on real-world exploited and audited smart contracts yields six key insights to enhance smart contract security and efficiency.  

Advancements in invariants-based smart contract analysis and verification call for tools that reliably and efficiently check semantic difference between invariants.These invariants, logical expressions that should hold in blockchain transactions are enforced through require/assert statements in Solidity smart contracts.  We present SInDi, a semantic invariant differencing tool for Solidity contracts that symbolically checks the differences of any two given invariants and quickly generates a verdict. Our evaluation on real-world smart contracts demonstrates SInDi's accuracy of 100% and efficiency of 0.09 seconds on average per verdict compared to human verdicts. Furthermore, we develop an invariant denoising pipeline based on SInDi that effectively removes up to 41.8% of weak dynamically-mined invariants to facilitate further analysis and verification tasks based on these auto-generated invariants.