Enhancing Reliability of Symbolic Execution Tools for Smart Contract Analysis through Rule-Based False Positive Reduction

1

Enhancing Reliability of Symbolic Execution Tools for Smart Contract Analysis through Rule-Based False Positive Reduction Muhammad Ali Hassan Ahmad1 , Muhammad Hashim Ali2 , Muhammad Ali Amer3 , Muhammad Naiman Jalil4 , Muhammad Hassan5 , and Affan Rauf6 1

arXiv:2608.10265v1 [cs.SE] 10 Aug 2026

2,3,6

Lakehead University, Ontario, Canada National University of Computer and Emerging Sciences, Pakistan 4 United Arab Emirates University, United Arab Emirates 5 German Research Center for Artificial Intelligence, Germany

Abstract—A blockchain is a decentralized, secure ledger system that enables transparent and immutable record-keeping, essential for trust and security in digital transactions. Smart contracts are self-executing agreements encoded on a blockchain, enabling different parties to fulfill the terms of the agreement automatically. These contracts trigger corresponding actions when conditions are met, ensuring decentralized and transparent transactions. Writing reliable smart contracts is challenging due to the lack of standardization. To find security vulnerabilities, tools based on various approaches, including symbolic execution, are used. However, these tools often report a large number of false positives, raising concerns about their reliability. The time and effort spent investigating false positives diverts resources from addressing actual vulnerabilities. Therefore, such tools must also be evaluated according to the rate of false positives they exhibit. More importantly, the algorithms and heuristics used by the tools must be enhanced to distinguish between true vulnerabilities and false alarms. In this paper, we first demonstrate the prevalence of false positives in vulnerability reports generated by Mythril, a symbolic execution-based analysis tool for Ethereum smart contracts. We analyze the root causes of these inaccuracies and devise a rule-based approach based on the gained insight to reduce false positives. We implement our rules for the most impactful vulnerabilities in Mythril and assess the effectiveness of our approach. Our results show a significant reduction in false positives without compromising the detection of true vulnerabilities, thus enhancing the tool’s reliability.

I. I NTRODUCTION Blockchains have gained popularity due to their convenience of secure, transparent, and decentralized recordkeeping, which eliminates intermediaries and lowers fraud risk. A blockchain is a decentralized distributed ledger system that records transactions across multiple systems, once a transactions is recorded there appears no possibility for later modification. Smart contracts are the brain that makes the blockchain function beyond a ledger. They are self-executing programs stored on the blockchain that automatically run and carry out the terms of an agreement when predefined conditions are met. They are used for secure and transparent management of transactions and record-keeping in blockchain systems. Once deployed on the blockchain, they also become permanent, requiring them to be thoroughly reviewed and tested before

deployment to eliminate errors and vulnerabilities. However, writing and testing secure smart contracts can be challenging due to the lack of standardized practices and tools. Security attacks targeting vulnerable smart contracts have been on the rise, which has led to financial loss, erosion of trust, and other security issues. Several smart contract analysis tools exist that detect different vulnerabilities; however, most of these tools, even the most popular ones, report a large number of false positives along with real vulnerabilities. These large numbers of false positives are confirmed by multiple smart contract auditing bodies in the form of benchmarks. A high rate of false positives in a security analysis tool can be problematic for several reasons. For example, investing excessive time in analyzing reported false positives impacts developers’ productivity and consequently may incur significant financial costs. For auditors, false positives result in a shift of emphasis from critical issues and, as a result, may pose a risk to the reliability of smart contracts. As end users rely on the integrity of smart contracts, which are validated using various tools, any challenge to the reliability of these tools also raises concerns about the efficacy of the auditing process, affecting the trust users have in the functionality of these contracts. The tools must accurately detect vulnerabilities rather than producing a high number of false positives. Previous research addresses either reporting smart contract vulnerabilities or reporting other problems, including false negatives, in the analysis tools. To the best of our knowledge, no previous work has focused on reducing false positives in symbolic analysis tools. This paper highlights false positives in smart contract analysis tools as a threat to the reliability of the whole smart contract ecosystem. It proposes a rule-based approach to minimize false positives associated with six significant vulnerabilities in symbolic execution based tools, implements these rules in Mythril’s [1] execution, and evaluates their effectiveness on Gigahorse [2] smart contracts, showing that Mythril, augmented by our rules, considerably reduces the number of false positives.

2

II. R ELATED W ORK Asem Ghaleb et al. [3] propose a systematic approach to evaluate the proposed analysis tools and their effectiveness. To do this, the author uses a tool called [4] SolidiFI. SolidiFI injects bugs into all potential locations in a smart contract to introduce targeted security vulnerabilities. SolidiFI then checks the generated buggy contract using the static analysis tools and identifies the bugs that the tools cannot detect, along with identifying the bugs reported as false positives. Paper has a dataset of 50 smart contracts in which they inject 9369 distinct bugs. These bugs were evaluated by 6 smart contract analysis tools, which were Oyente [5], Securify [6], Mythril [1], SmartCheck [7], Manticore [8], and Slither [9]. The experiment injects the bugs into the smart contract and then evaluates them using the analysis tools, and then evaluates whether the tool correctly identified all the injected bugs. This Paper is mainly focused on false negatives. Many of the detected bugs were not caught by the analysis tools such as Mythril, which failed to detect the largest set of bugs in the experiments. Reza M. Parizi et al. [10] mainly try to answer two different questions relating to smart contract analysis tools regarding effectiveness and accuracy. There are 4 main tools that [10] uses, namely, Oyente, Mythril, Securify, and SmartCheck. The paper uses 10 smart contracts to experiment on. The experiment selects a new tool randomly and a new smart contract randomly. It then applies the tool to the smart contract and collects the results. [10] showed that the SmartCheck tool is statistically more effective than the other automated security testing tools at a 95 percent significance level. Concerning accuracy, Mythril was found to be significantly accurate, issuing the lowest number of false alarms among peer tools. On evaluating the accuracy, the Mythril tool showed the highest accuracy score; however, the Oyente tool again performed the worst in accuracy. Ardit Dika et al. [11] examine the different audited and vulnerable smart contracts and use different analysis tools to gauge their effectiveness, accuracy, and consistency. [11] analyses both bytecode and solidity contracts. It focuses on both false negatives and false positives. [11] uses only 21 audited smart contracts and 24 vulnerable smart contracts. 4 tools were used to analyze the smart contracts: Oyente, Securify, Remix [12], and SmartCheck [7]. [11] analyzes different smart contracts and analyzes them according to the false positives and false negatives. It then creates a vulnerability matrix to find which tool accurately catches what vulnerability. According to [11], SmartCheck found the most vulnerabilities. Alexander Mense et al. [13] summarize known vulnerabilities in smart contracts found by literature research. It compares currently available contract analysis tools for their capabilities to identify and detect vulnerabilities in smart contracts based on a taxonomy for vulnerabilities. [13] lists different vulnerabilities present in smart contracts and classifies them according to the severity level. These vulnerabilities include, but are not limited to, gas-less send, external calls, and mishandled exceptions. [13] then uses analysis tools, namely, Oyente, Securify, Remix, SmartCheck, F* [14], Mythril, and Gasper [15]. Re-

entrancy ranks the highest among all the vulnerabilities, with 6 out of 7 tools detecting it. The results show the different analysis tools detecting different vulnerabilities. S. Kim et al. [16] collected 391 papers and extracted 67 relevant to the smart contract analysis. These papers were classified into 3 different topics: static analysis for vulnerability detection, static analysis for program correctness, and dynamic analysis, which were then explored with further classifications. The selected papers focused on analyzing smart contracts using either static or dynamic techniques. In the context of static analysis for vulnerability detection, symbolic execution is employed to simulate concrete executions with inputs represented as symbolic values. Additionally, concolic testing emerges as the dominant technique for detecting vulnerabilities in Ethereum Virtual Machine (EVM) bytecode. [16] evaluates that dynamic analysis primarily relies on techniques such as fuzzing and runtime verification to analyze program behavior during execution. Enmei Lai et al. [17] analyze the integer overflow of Solidity smart contracts. It summarizes 11 kinds of integer overflow features. After this analysis, a static detection tool for integer overflow is designed based on the idea of the SmartCheck tool 1 . The designed tool can detect integer overflow vulnerabilities in smart contracts. 7000 smart contracts were tested on the designed tool, out of which 430 smart contracts had an integer overflow vulnerability. [17] evaluates 7000 smart contracts using the designed tool, and the accuracy of the detection results is almost 100 percent. There were 109 smart contracts with multiplication overflow vulnerabilities, 218 smart contracts with addition overflow vulnerabilities, and 103 with subtraction overflow vulnerabilities. [17] also compares their tool with other smart contract vulnerability detection tools. Tikhomirov et al. [7]. Provide a taxonomy of Solidity issues and introduce SmartCheck, an extensible static analyzer (Java). Evaluated on real-world contracts against manual audits, SmartCheck reports a broad range of security findings with comparatively high accuracy and low false-positive rates. Jiaming Ye et al. [18] present Clairvoyance 2 , a crossfunction and cross-contract static analysis by identifying infeasible paths to detect re-entrancy vulnerabilities in a smart contract. It presents a large-scale empirical study to evaluate the effectiveness of three recent general-purpose static tools using 11714 real-world contracts. To address the re-entrancy issue, [18] developed Clairvoyance, a static analysis tool that uses interprocedural control-flow analysis to analyze the code of smart contracts and identify potential vulnerabilities. According to the findings, the tools are not sufficiently effective in handling the re-entrancy bug. The reason is that most of their reports are false negatives. To avoid these false positives happening to the tool, [18] audits incorrect reports manually. For the number of detection results of the four static tools, Slither reports 162 vulnerabilities in total, of which 3 reports are true positives, while the other 159 reports are false positives. Oyente has at least 28 reports, of which 4 results 1 https://github.com/smartdec/smartcheck 2 https://github.com/nikitastupin/clairvoyance

3

are true positives, while the rest 24 reports are false positives. Sefa Akca et al. [19] propose techniques that will allow complete automated analysis of smart contracts, using both static and dynamic techniques. The author injects well-known vulnerabilities into smart contracts. Four major works in [19] are static checks, test generators, run-time monitoring, fault seeding tools, and empirical evaluation. The approach for analysis of smart contracts includes three main components: 1) A vulnerability detection technique, SolAnalyser [19]. 2) An automated input generation for smart contracts, 3) Use of a tool, MuContract. SolAnalyser, with static and dynamic checks supported by test generation, was effective at detecting vulnerabilities across all 1838 contracts and the 12866 mutated versions, with a precision of 72 percent and a recall rate of 100 percent. The technique was capable of detecting more types of vulnerabilities than all five existing analysis tools used in the experiment. Yuchiro Chinen et al. [20] present a static analysis tool named RA (Re-entrancy analyzer) to analyze smart contract vulnerabilities against re-entrancy attacks. [20] aims to design an inter-contract static analysis tool that uses only EVM bytecodes as input, eliminates false negatives and false positives, and does not require analysts to have prior knowledge of the attacks on contracts. We can use [20] to evaluate and analyze smart contract vulnerabilities, especially re-entrancy issues, in our research. [20] Develops a static analysis tool that focuses on inter-contract analysis using EVM bytecodes as input, effectively reducing false negatives and false positives. The novelty of the RA tool [20] lies in its ability to perform analysis without requiring analysts to possess prior knowledge of specific attacks on contracts. Joao F. Ferreira et al. [21] present SmartBugs3 , an extensible and easy-to-use execution framework that simplifies the execution of analysis tools on smart contracts written in Solidity, the primary language used in Ethereum. One of the primary objectives of SmartBugs [21] is to enhance the reproducibility of research focused on automated reasoning and testing of smart contracts. [21] demonstrates the ease of integrating new tools into SmartBugs and compares its performance with existing tools. Specifically, [21] extended SmartCheck and utilized SmartBugs to showcase the significant improvement in vulnerability detection, particularly related to Bad Randomness, Time Manipulation, and Access Control. Xingrun Yan et al. [22] propose a semantic analysisbased method for the smart contract code to effectively defend against vulnerability attacks and improve detection efficiency. [22] implements the approach as a self-contained tool, which is then evaluated with 99 smart contracts and compared with other detection tools. The results demonstrate that the method can enhance both the accuracy and the ability to identify vulnerabilities. [22] used four datasets, each comprising distinct vulnerabilities, to measure the effectiveness of their method. The methodology accurately detected all instances of fallback function re-entrancy vulnerabilities and cross-function re-entrancy vulnerabilities across the datasets. The authors 3 https://github.com/smartbugs/smartbugs

compared their methodology with two tools, Mythril and Slither [9], which both failed to identify all instances of these vulnerabilities. Nikolay Ivanov et al. [23] conduct an evolutionary analysis and classify 133 threat mitigation solutions for smart contracts using a five-dimensional taxonomy. They combine eight mitigation methods and map vulnerabilities addressed by these solutions. Their methodology includes 1. Classify solutions using taxonomy. 2. Synthesize the workflow of eight core methods. 3. Map vulnerability. 4. Analyze trends and gaps. The paper Daojing He et al. [24] systematically categorizes smart contract vulnerability detection tools into six classes. The paper evaluates 27 tools for their accuracy and multiversion handling capability. The results demonstrate that most tools focus on older smart contract versions, while the new tools involving machine learning are more accurate; however, they flag fewer vulnerabilities. The paper proposes to combine static, dynamic, and neural network-based tools for accurate multi-version detection. While the key limitations include the time-intensive nature of static methods, and the challenges dynamic tools face in detecting sequence-specific vulnerabilities, with few tools supporting multi-version analysis. The paper Chong Chen et al. [25] systematically reviews the popular large language model, ChatGPT4 , to assess its effectiveness and limitations in identifying smart contract vulnerabilities and to compare it to native tools. ChatGPT effectively identifies vulnerabilities like denial-of-service, frontrunning, and unchecked return values. However, it struggles with reentrancy and access control. The key limitations include the limited number of tokens and uncertainty in the analysis, which lead to erroneous or biased judgments. It also tends to produce false positives and relies heavily on specific protection mechanisms. Zhiyang Chen et al. [26] explore the use of dynamically inferred invariants to enhance smart contract security and introduce the Trace2Inv framework for generating these invariants from transaction histories. Individual invariant guards effectively block real-world exploits with low gas overhead, and combining multiple guards increases coverage while maintaining a low false positive rate. Limitations include the risk of missing bypass strategies, biased hack selection, the need for dynamic updates tied to variables like Oracle prices, and challenges in integrating these guards with other DeFi protocols. Yuqiang Sun et al. [27] present GPTScan, a tool that integrates GPT with static analysis to identify logic vulnerabilities in smart contracts. It achieves a low false positive rate of 4.39% for non-vulnerable contracts and over 90% precision for token contracts, making it effective for large-scale scanning of on-chain contracts. GPTScan outperforms existing tools in detecting vulnerabilities within the Web3Bugs and DefiHacks datasets, with static confirmation reducing two-thirds of false positives while minimally affecting false negatives. However, its modifier filtering may lead to inaccuracies, the static analysis lacks path sensitivity and could benefit from symbolic execution, and the use of a temperature parameter of zero 4 https://platform.openai.com/docs/api-reference/introduction

4

results in deterministic outputs that limit creativity. III. P ROPOSED A PPROACH This paper aims to enhance the reliability of symbolic execution-based smart contract analysis tools by reducing the rate of false positives. This reduction directly increases precision, which is defined as: True Positives True Positives + False Positives Improving precision generally increases a tool’s reliability to detect vulnerabilities. High precision indicates that a most identified vulnerabilities are true vulnerabilities, and the tool is less likely to flag false positives, making the tool’s positive predictions more reliable. Precision =

A. Approach: Rule-Based False Positive Reduction We define vulnerability-specific rules to minimize false positives. These rules, directly patched in the implementation of a tool, help identify and block false positives within the symbolic execution process. These rules which often function as constraints are derived from characteristics of the analyzed smart contracts, vulnerabilities, and known patterns of false positives reported by analysis tools. Each rule is presented in Section V. B. Implementation and Rationale We implement our proposed rules in Mythril’s [1] implementation to assess the effectiveness of our approach. We selected Mythril due to its popularity, widespread adoption, symbolic execution-based nature, open-source nature, active maintenance, and capability to report a broad spectrum of significant vulnerabilities. For reproducibility, we utilized Mythril version v0.23.10 with commit 21b3e92 of the Mythril’s git repository5 . C. Evaluation Methodology To assess and improve Mythril’s [1] precision, we utilized reputable sources of ground truth, specifically, Gigahorse Benchmarks [2]. These benchamarks provide open-source, labeled smart contracts, curated collections in both source and binary formats, each labeled with vulnerabilities. For reproducibility, we utilized commit ebcf377 of the Gigahorse Benchmarks repository6 . Our evaluation employs a controlled, iterative comparison against distinct benchmark datasets, as summarized in Table II. The Gigahorse Benchmarks dataset, totaling 140 contracts, comprises two distinct collections critical for evaluation: 100 vulnerable contracts derived from the vulnerable-sources directory, each explicitly labeled with known vulnerabilities; and 40 invulnerable contracts from the invulnerable-bytecode directory, which are 5 https://github.com/ConsenSysDiligence/mythril/commit/ 21b3e92747f6b5ef1e22825756ba63f5b1c58621 6 https://github.com/nevillegrech/gigahorse-benchmarks/commit/ ebcf37769d46253ae540d496cd84445120c57188

Fig. 1. Process of analyzing Smart Contracts using Mythril and GigaHorse Benchmarks and comparing the reported vulnerabilities.

confirmed to be clean. This structure allows us to assess the tool’s performance against both known issues and benign code. The Benchmark labels serve as a reference to determine whether a vulnerability flagged by Mythril corresponds to an actual issue. Any vulnerability flagged by Mythril but absent in the ground truth reference was considered a false positive. The methodology is structured to quantify the improvement achieved by our rule-based approach: 1) Baseline Assessment: We apply the vanilla Mythril implementation to the datasets. The reported vulnerabilities are compared against the ground truth labels to establish a baseline false positive count. 2) Enhanced Analysis: The same process is repeated using our improved version of Mythril, which integrates the proposed rules for false positive reduction. This comparative analysis allows us to measure the absolute reduction in false positives and validate the practical benefits of integrating our approach into production-grade analysis tools. IV. BASELINE E VALUATION We use vanilla Mythril [1] to analyze all Gigahorse Benchmarks [2] smart contracts. As expected, Mythril reported vulnerabilities in several contracts. We utilized the labels provided within the Gigahorse Benchmarks as the ground truth to assess the accuracy of vulnerabilities reported by vanilla Mythril. This evaluation was performed on two distinct subsets: • Vulnerable Contracts (N = 100): Contracts explicitly labeled with known vulnerabilities. If a vulnerability was reported by Mythril and matched the benchmark label, it was a true positive (TP). If Mythril missed a known vulnerability, it was a false negative (FN). • Invulnerable Contracts (N = 40): Contracts confirmed to be clean (benign). Any vulnerability flagged by Mythril in these contracts was classified as a false positive (FP). The overall evaluation process is illustrated in Fig. 1. Our complete comparative analysis across the two Gigahorse subsets is presented in Table I. A review of the results confirms that the Vanilla Mythril implementation generates a significant number of false positives across multiple vulnerability categories and datasets. Specifically, in our baseline analysis of the Gigahorse Invulnerable contracts, vanilla Mythril reported a total of

5

TABLE I C OMPARATIVE P ERFORMANCE OF VANILLA VS . I MPROVED M YTHRIL ON G IGAHORSE B ENCHMARKS GH Invulnerable (N = 40) False Positives (FP) FP (V) FP (I)

Vulnerability Type

False Positives (FP) FP (V) FP (I)

GH Vulnerable (N = 100) False Negatives (FN) True Positives (TP) FN (V) FN (I) TP (V) TP (I)

State Access after an External Call 15 0 57 0 0 Assertion Violation 0 0 0 0 0 Dependence on Predictable Env. Variable 36 0 18 0 0 External Call To User-Supplied Address 8 1 25 2 0 Integer Arithmetic: Overflow and Underflow 34 50 11 12 4 Multiple Calls in a Single Transaction 9 0 19 0 0 Total Functions Flgged 102 51 130 14 4 GH: GigaHorse. FP: False Positives. FN: False Negatives. TP: True Positives. V: Vanilla Mythril. I: Improved Mythril.

TABLE II DATASETS U SED IN T HIS S TUDY

Dataset Gigahorse Benchmarks (Vulnerable) Gigahorse Benchmarks (Invulnerable) Total

Number of Smart Contracts 100 40 140

102 false positives. In the next step, we incorporated the rules we proposed to reduce false positives into Mythril’s implementation. V. P ROPOSED RULES The following subsections discuss the implementation of proposed rules concerning six impactful vulnerabilities and how they improve the precision of the results produced by Mythril. A. State access after an external call State access after an external call refers to the ability to read or modify the internal state of a smart contract after an external function call has been made. Previously, the check for reentrancy vulnerability method was called after state changes in analyze state to detect potential re-entrancy vulnerabilities caused by those changes. This approach, however, led to false positives. To eliminate this, the code was modified to directly call the vulnerability check at every state change within analyze state, ensuring comprehensive evaluation and elimination of false positives. The analyze state method in the StateChangeAfterCall module was modified to iterate over all StateChangeCallsAnnotation objects and their associated state change states. If a re-entrancy vulnerability is detected, the analyze state method creates a new PotentialIssue object and returns a list containing only that object. If no vulnerabilities are detected, the method returns an empty list. This ensures that only true positives are reported. The check for reentrancy vulnerability first checks if any constraints in the state change state could prevent reentrancy. Algorithm 1 follows the following steps to correctly identify true positives only and not report any of false positives. 1) It first checks if the current function being executed is the constructor, and if so, it returns an empty list.

0 0 0 0 3 0 3

0 0 0 0 12 0 12

0 0 0 0 13 0 13

Algorithm 1 State access after an external call 1: if length of offset > 1 then 2: for i = 0 to offset-1 do 3: offset to call 1 4: end for 5: end if 6: if constraints == true then 7: return false 8: else 9: new constraints = gas and destination address 10: if Generate transaction sequence is successful then 11: return true 12: end if 13: end if

2) It then iterates over all StateChangeCallsAnnotation objects and their associated state change states. 3) For each state change state, the method checks if it was preceded by a low-level call. 4) If so, it creates a PotentialIssue object and adds it to the potential issues list of the StateChangeCallsAnnotation object. 5) If there are constraints, it returns False since a re-entrancy vulnerability is not possible in that state. 6) If there are no constraints, the method creates a new Constraints object and adds constraints to ensure that the gas and destination address of the external call meet certain conditions. 7) It then tries to generate a transaction sequence from the global state to the change state. 8) If the constraints are satisfied and a transaction sequence can be generated, it means that there is a potential reentrancy vulnerability, and the method returns True. The analyze state method takes a GlobalState object as its argument and returns a list of PotentialIssue objects if reentrancy vulnerabilities are detected. B. Assertion Violation An assertion violation occurs when a predefined condition within the implementation is not satisfied. It can occur when a condition or assumption results in false during execution. These assumptions or assertions are usually checks on the data

6

validity, program state, or expected user input. An assertion violation is flagged when any of these checks are not satisfiable. It also signifies that the implementation is not prepared for unforeseen and unexpected situations. This could be due to a bug in the implementation, any unexpected user input, or a rare instance that was not handled in the implementation. Assertion violation belongs to the Exception class. The Exception class’s implementation is responsible for the detection of an assertion violation. The detection approach is followed by analyzing the entire execution state or the global state, and then identifying where the smart contract may reach an undefined state that contradicts an assertion. This specific approach is achieved by modifying hooks ( pre hooks) within the smart contracts, these hooks serve as interception points or flags in the program’s execution flow. By strategically positioning these hooks, the Exceptions class gains deeper insight into program’s execution flow and can pinpoint potential assertion violations before they occur. Additionally, this strategic positioning allows additional control-flow decisions to accurately differentiate between true and false positives. This change within the implementation blocks the high number of false positives and reports the potential true positives before they occur. Algorithm 2 Assertion Violation 1: if opcode is a CALL-related instruction then 2: Get target address ▷ From The Stack 3: if it is an external call then 4: Add instruction address to call offsets list 5: end if 6: else 7: if there are multiple call offsets recorded then 8: for each pair of consecutive call offsets do 9: call 1 ← first call offset 10: call 2 ← next call offset 11: Create a list of constraints 12: Add constraints ▷ from the WORLD STATE

and mstate 13: end for 14: end if 15: end if

The analyze state method performs the actual detection of assertion violations. The method first checks the current opcode to determine if it is a JUMP, INVALID, or REVERT opcode. If it is a JUMP opcode, the method annotates the current state with a LastJumpAnnotation object containing the address of the current instruction. If it is a REVERT opcode and not an assertion violation, the method simply returns an empty list. If it is an INVALID opcode and the previous opcode was a REVERT and the assertion condition is always false, the method considers this to be an assertion violation. If an assertion violation is detected, the method creates an Issue object containing information about the violation and returns a list containing the issue. If no assertion violation is detected, the method returns an empty list. The following changes were made to the code to achieve this:

1) The pre hooks of the detection module were changed to include ”REVERT” to detect more assertion violations. 2) The is assertion failure function was modified to check for both assertion violations and revert statements. 3) The is assertion always false function was modified to check for both assertion failures and revert statements. 4) The Exceptions class was modified to only return an issue if the current state is an assertion violation and the previous opcode is REVERT, indicating that the assertion condition is always false. If a vulnerability is detected, the algorithm creates an issue with relevant details and recommendations. Finally, it returns a list of identified issues. C. Dependence on Predictable Environment Variable Dependence on predictable environment variables refers to a situation where the behavior or state of a smart contract relies on certain external factors that are expected to remain constant, such as external data, parameters, or conditions. If the external environment variables (i.e., parameters) were to change, this could result in false positives. We modified analyze state function where the control flow decisions were not accurate in the original code. The modified analyze state function helps in achieving the objective of reducing false positive vulnerabilities and focusing on reporting the true positive ones. The function achieves this by the applying following rules and constraints: Algorithm 3 Dependence on Predictable Environment Variable 1: if the opcode is a CALL-related instruction then 2: Get target address 3: if an external call then 4: Add the address to the call offsets list 5: end if 6: else 7: if multiple call offsets recorded then 8: for each pair of consecutive call offsets do 9: call 1 ← First Call’s Offset 10: call 2 ← Next Call’s Offset 11: Create a list of constraints 12: end for 13: end if 14: end if

1) Checking if the control flow decision depends on one of the predictable environment variables (coinbase, gas limit, block number, or timestamp). 2) It monitors a tainted variable, which is a variable that can be modified by an outside user. 3) Verifying whether the tainted value influences the constraints in the world state. 4) If it doesn’t, the function considers this case as a false positive and doesn’t report it. 5) If the tainted value does influence the constraints, the function tries to find a valid transaction sequence that satisfies the constraints.

7

6) If a sequence is found, it generates an issue report for this vulnerability as a true positive. By following these steps, the updated function helps reduce the number of false positive vulnerabilities reported and focuses on reporting the true positive ones. This approach improves the accuracy of vulnerability detection and helps concentrate on true positive vulnerabilities. D. External Call to User-Supplied Address External Call to User Supplied Address refers to a scenario where a smart contract invokes a function or sends a transaction to an address provided as an argument or parameter by another contract. This allows smart contracts to interact with external contracts dynamically. The original code did not check for state modifications before and after the external calls. This often led to not identifying re-entrancy vulnerability. We changed the analyze state function and added some constraints to solve this issue. The analyze state function analyzes the given state, identifying potential issues related to insecure external calls in smart contracts. The proposed improvement helps in achieving the objective of reducing false positive vulnerabilities and focusing on reporting the true positives only. The function achieves this by the applying following rules and constraints: This function, analyze state, analyzes the given state to identify potential issues related to insecure external calls in smart contracts. Algorithm 4 External call to user-supplied address ▷ Tainted data is present constraintDependency ← [ ] for dependsOn in state.world.state.constraints do for annotation in state.mstate.stack[-2].annotations

1: if tainted data = True then 2: 3: 4:

do if annotation = predictable value annotation

5:

then constraintDependency ← constraintDependency ∪ {annotation} 7: Add annotation to constraintDependency Set 8: end if 9: end for 10: end for 11: constraintDependency ← [ ] 12: end if 6:

To achieve the primary goal of reporting true positives while minimizing false positives, the function follows the following steps: 1) Ignore calls made in the constructor: The function starts by checking whether the current function is a constructor. 2) If it is, the function returns an empty list, as it does not analyze constructor calls. 3) Check for state modifications: The function inspects the instructions of the smart contract to identify state 4) Modifications (SSTORE) both before and after the external call. This helps to determine if there is any state

modification happening after the external call, which is a necessary condition for a reentrancy vulnerability to occur. 5) Raise UnsatError for no state modifications after the call: If there are no state modifications after the external call, the function raises an UnsatError exception. 6) Add constraints for external calls: The function defines constraints to check for external calls with user-controlled addresses for any remaining gas. These constraints are necessary for identifying potential re-entrancy vulnerabilities. 7) Find a valid transaction sequence: Using a solver, the function attempts to find a valid transaction sequence that satisfies the constraints. If the solver can find such a sequence, it indicates a potential re-entrancy issue, which is reported as a vulnerability. By following these steps, the analyze state function focuses on reporting true positive vulnerabilities related to insecure external calls and reduces false positives by filtering out cases where the external call does not lead to a re-entrancy vulnerability. E. Integer Arithmetic Overflow and Underflow Integer arithmetic overflow and underflow occur when the result of an arithmetic operation exceeds the maximum or falls below the minimum representable value for the data type being used. The current arithmetic helper function relied on a Z3 function and relied on the return value of the function to be true. This caused unpredictable behavior when the constraints in the arithmetic helper function were not precise enough. We modified this arithmetic helper function to perform checks on the Z3 solver itself. The function bitvec helper uses Z3 [28] to check whether a value is greater than or less than a certain threshold. The proposed improvement helps in achieving the objective of reducing false positive vulnerabilities and focusing on reporting the true positives only. The function achieves this by applying the following constraints and rules: Algorithm 5 Integer Arithmetic Overflow and Underflow 1: maximum gas limit ← 1000000 2: Get account balance: account balance 3: if gas ≤ MAX GAS LIMIT

∧ gas ≥ MIN GAS LIMIT then 4: if account balance > 0 then 5: return satisfied ▷ Constraints are satisfied 6: else 7: return !satisfied ▷ Account balance is too low. 8: end if 9: else 10: return !satisfied ▷ Gas limit exceeds the maximum. 11: end if Here’s a breakdown of the steps: We create a constraint using the ’UGT’ function from Z3, which stands for ”Unsigned Greater Than”. We propose to add the following rule to the solver, where we

8

1) compares the value of ’raw’ with a computed threshold value (2 * array. size() - 1) for overflow and (-2 * array. size() - 1) for underflow. 2) We check if the constraints added to the solver are satisfiable by calling ’solver. check()’. If the result is ’sat’ (satisfiable), it means there is a solution that satisfies the constraints. In this case, it indicates that the value of ’raw’ is greater than the threshold, implying an overflow. 3) After checking the satisfiability, we remove the added constraint from the solver. This step is essential only if we want to remove the constraints that were added during the solving process using backtracking. The arithmetic helper takes two objects and an operation. The objects must be of the BitVector type, and the operation must be specified using a callable object. The function performs the valid arithmetic operation on those objects and stores the annotations and the result in a new BitVector object. The result object has the same size as the input objects, and the annotations are the union of the annotations of the input objects. Then, the function checks for the potential overflow and underflow by comparing the result with the maximum and the minimum possible values of the input object’s data type. The function returns the result object only if no overflow or underflow is detected. Applying these rules provide a convenient and safe way to perform arithmetic operations and reduce false positives. F. Multiple calls in a single transaction Multiple calls in a single transaction refer to the ability to execute multiple function calls or interactions with different contracts within a single blockchain transaction. If a single function call is not successful, a false positive will be generated. The analyze state function did not check if the previous external call was successful or not. We modified the function and added some constraints to counter this and ensure that the reported vulnerabilities were genuine. The proposed updates in the analyze state function reduce false positives by improving the checks and constraints for preventing multiple sends (i.e., external calls) within a single transaction. The additional checks and constraints ensure that the function only reports vulnerabilities when the previous external call was successful, thereby increasing the confidence that the reported vulnerabilities are genuine issues. Algorithm 6 Multiple calls in a single transaction 1: let x = state.world.state.constraints 2: let y = state.mstate.constraints 3: let z = state.mstate.stack 4: if len(call offsets) > 1 then 5: for i ← (0 to len(call offsets) - 1) do ▷ First Call Offset 6: call 1 ← call offsets[i] 7: call 2 ← call offsets[i + 1] ▷ Next Call Offset 8: constraints ← x + [y[-1], y[-2]] 9: constraints.append(z[-1] = 1) 10: end for 11: end if

TABLE III S UMMARY OF P ERFORMANCE G AINS (VANILLA VS . I MPROVED M YTHRIL ) Metric Vanilla (V) False Positive (FP) Reduction GH Invuln FP Total (N = 40) 102 → 51 GH Vuln FP Total (N = 100) 130 → 14 GH Vuln (N = 100) Performance Precision (TP/(TP + FP)) 8.5% FDR (FP/(TP + FP)) 91.5% Recall (TP/(TP + FN)) 75.0% F1-Score (Overall) 0.152 FDR: False Discovery Rate.

Improved (I) 50.0% ↓ 89.2% ↓ 48.1% 51.9% 81.2% 0.605

Some of the improvements made to the function include: 1) Ensuring that at least two calls are present in the call offsets list before proceeding with the vulnerability detection logic. 2) Verifying that the previous external call was successful by checking if the top element of the stack is equal to 1. 3) Distinguish between external and internal calls by checking the target address of the calls. These improvements make the function more focused on true positive vulnerabilities and reduce the likelihood of false positives. VI. R ESULTS AND E VALUATION A. Gigahorse Benchmark Results We evaluate the efficacy of our proposed rule-based improvements by comparing Vanilla Mythril [1] against our Improved Mythril on the Gigahorse benchmark [2], which consists of 40 invulnerable and 100 vulnerable smart contracts. Our core objective was to reduce the number of False Positives (FP) across the six targeted vulnerabilities. The complete findings are detailed in Table I, with a summary of the performance metrics provided in Table III. a) False Positive Analysis: The results show a significant reduction in false positives, verifying the tool’s ability to perform accurate analysis: • GigaHorse Invuln: The Invuln or the invulnerable dataset is designed to accurately measure false positives FP. The total count of FPs decreased from 102 to 51, a 50.0% reduction. All FPs were eliminated with a 100.0% success rate for four (State Access after External Call, Assertion Violation, Dependence on Predictable Environment Variable, and Multiple Calls in a Single Transaction) of the six vulnerability types we implemented. • GigaHorse Vuln: The results on the Vuln or the vulnerable dataset are even more notable. The total count of FPs decreased from 130 to 14, a 89.2% reduction. This is a significant gain, as reflected by the False Discovery Rate (FDR), which decreased from 91.5% to 51.9%. b) True Positives and Recall: The proposed rules we implemented are designed to preserve and improve detection capabilities, enhance the precision of the tools, and correctly identify and report vulnerabilities. While the primary objective was FPs reduction, our results also demonstrate a positive shift

9

in a tool’s ability to correctly identify and report true positives TPs. The total count of TPs increased from 12 to 13, which directly corresponds to the false negatives FNs that decreased from 4 to 3. This indicates that Mythril’s implementation with our proposed rules identified one vulnerability that the standard vanilla Mythril missed. Quantitatively, this small change translates to a rise in Recall from 75.0% to 81.2%. B. Discussion: Overall Performance and Limitations We compare the standard Mythril (vanilla) with the improved Mythril using standard performance metrics. Improved Mythril is the standard version of Mythril implemented using our proposed rules. We also report the F1-score, as it combines both precision and recall, and provides a comprehensive measure of overall accuracy. The improved Mythril reached an F1-score of 0.605, from 0.152 that vanilla Mythril achieved, reflecting a nearly 4× gain in overall performance. Table III reports and compares the following performance metrics: Precision, False Discovery Rate, Recall, F1-Score, % FPs Reduction. The only outlier among the six targeted vulnerability classes is Integer Arithmetic: Overflow and Underflow, which contributes to the majority of the remaining FPs (12 of 14) and all FNs (3 of 3). In addition, it is the only vulnerability type for which the FPs increased from (34 to 50) on the Invulnerable dataset. Further research is required to understand this unexpected behavior and then to develop more sophisticated rules specific to this complex class. Despite this, the substantial gains observed in Tables I and III for the other five most significant vulnerability types overwhelmingly validate the efficacy of our proposed rules. VII. M ETHODOLOGY G ENERALIZATION AND P ORTABILITY We implemented our proposed rules in Mythril; however, the underlying methodology is designed for wide applicability. These rules are based on standard Ethereum Virtual Machine (EVM) principles and a small set of basic analysis primitives that are common to most analysis tools. Their design allows the logic to be easily separated and ported as a light layer to other symbolic analysis frameworks. A. Basic Analyzer Capabilities Required The minimum requirements for a target analyzer to successfully port proposed rules include four fundamental capabilities: 1) Path Feasibility Query: The ability to determine if a specific execution path leading to a vulnerability alert can actually be reached by any valid transaction input. This typically uses an underlying constraint solver. 2) Data Taint Tracking: The ability to mark input data (like transaction arguments or specific environment variables) and trace how that data influences the program’s execution. 3) Call Type Classification: The ability to accurately distinguish between internal jumps within the contract code and genuine external calls that cross address boundaries.

4) State Effect Detection: The ability to identify when a specific execution path permanently alters the contract’s storage or transfers assets. B. Generalized Filtering Rules The primary goal of the rules is to suppress alerts where the detected vulnerability exists on a path that is infeasible or where a state check proves the alert is safe. The general principle applied to our six targeted vulnerability classes is as follows: • Integer Arithmetic (Overflow/Underflow): A wraparound is reported only if a path feasibility check confirms that inputs exist to trigger the overflow or underflow. • State Access after External Call (Re-entrancy): Flag a state read or write made after an external call only when a feasibility check confirms no control flow guard (e.g., a re-entrancy lock) is active on that path. • Assertion Violation: A program failure is flagged only if the failure condition depends on an external input that the path solver can prove to be always false or that leads to a feasible failure state. • Dependence on Predictable Environment Variable: If a contract decision relies on a tainted, predictable environment value, an alert is issued only if a feasible path leads directly to a contract asset or storage change. • External Call to User-Supplied Address: If an external call uses an address derived from tainted user input, the issue is reported only if a subsequent asset transfer or storage change is also proven feasible on that same path. • Multiple Calls in a Single Transaction: Count the number of unique, true external message calls along a feasible path. The alert is triggered only if ≥ 2 such calls are detected along with a resultant state effect. C. Portability and Limits Portability: As the methodology relies only on these core principles, symbolic execution frameworks that expose similar capabilities, such as Oyente [5] and Manticore [8], are conceptually suited for implementing this approach. This suggests that the measured precision gains are not exclusive to the tool used for implementation. Limits: Our results are restricted to Mythril on the Gigahorse dataset (Section VI), we do not claim performance for other tools. If a target tool lacks a required primitive (e.g., taint tracking), the corresponding filtering rule must be disabled or use a simplified check. VIII. C ONCLUSION AND F UTURE W ORK This paper addressed the issue of high False Positive (FP) rates in the symbolic analysis of Ethereum smart contracts by applying a set of lightweight, rule-based patches to Mythril across six key vulnerability classes. Using the Gigahorse benchmarks, our implementation achieved a significant reduction in False positives. Specifically, we reduced FPs by 50.0% on the invulnerable set and by 89.2% on the vulnerable set,

10

leading to a near fourfold increase in the F1-Score, from a practically unusable 0.152 to 0.605 (Table III). This improvement was achieved while also maintaining, and slightly improving, detection capability (Recall 75.0% → 81.2%). IX. F UTURE W ORK Future work may extend the scope and robustness of this study along three directions. First, in Integer Arithmetic, investigate the unexpected behavior and develop more sophisticated rules that reduce the remaining false positives. Second, under Evaluation, the ground truth reference may be expanded to include additional datasets for more rigorous testing of each proposed rule. Finally, in Portability, the proposed rules are to be applied to the implementation of other tools to formally evaluate the generality of the approach. R EFERENCES [1] “Mythril,” 2018. [Online]. Available: https://github.com/ConsenSys/ mythril [2] N. Grech, “Gigahorse-benchmarks,” 2019. [Online]. Available: https: //github.com/nevillegrech/gigahorse-benchmarks [3] A. Ghaleb and K. Pattabiraman, “How effective are smart contract analysis tools? evaluating smart contract static analysis tools using bug injection,” CoRR, vol. abs/2005.11613, 2020. [Online]. Available: https://arxiv.org/abs/2005.11613 [4] K. Asem Ghaleb and Pattabiraman, “Solidifi benchmark,” 2020. [Online]. Available: https://github.com/DependableSystemsLab/ SolidiFI-benchmark [5] D.-H. Loi Luu, H. Chu, P. Olickel, A. Saxena, and Hobor, “Oyente,” 2020. [Online]. Available: https://github.com/enzymefinance/oyente [6] P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Bünzli, and M. Vechev, “Securify,” 2020. [Online]. Available: https://github.com/ eth-sri/securify [7] S. Tikhomirov, E. Voskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, and Y. Alexandrov, “Smartcheck: Static analysis of ethereum smart contracts,” in 2018 IEEE/ACM 1st International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), 2018, pp. 9–16. [8] “Manticore,” 2017. [Online]. Available: https://github.com/trailofbits/ manticore [9] Y. Feng, E. Torlak, and R. Bodik, “Precise attack synthesis for smart contracts,” 2019. [10] R. M. Parizi, A. Dehghantanha, K. R. Choo, and A. Singh, “Empirical vulnerability analysis of automated smart contracts security testing on blockchains,” CoRR, vol. abs/1809.02702, 2018. [Online]. Available: http://arxiv.org/abs/1809.02702 [11] A. Dika and M. Nowostawski, “Security vulnerabilities in ethereum smart contracts,” in 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), 2018, pp. 955–962. [12] “Remix - solidity ide,” 2017. [Online]. Available: http://remix.ethereum. org [13] A. Mense and M. Flatscher, “Security vulnerabilities in ethereum smart contracts,” in Proceedings of the 20th International Conference on Information Integration and Web-Based Applications & Services, ser. iiWAS2018. New York, NY, USA: Association for Computing Machinery, 2018, pp. 375–380. [Online]. Available: https://doi.org/10. 1145/3282373.3282419 [14] K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy et al., “Formal verification of smart contracts: Short paper,” in Proceedings of the 2016 ACM workshop on programming languages and analysis for security, 2016, pp. 91–96. [15] T. Chen, X. Li, X. Luo, and X. Zhang, “Under-optimized smart contracts devour your money,” in 2017 IEEE 24th international conference on software analysis, evolution and reengineering (SANER). IEEE, 2017, pp. 442–446. [16] S. Kim and S. Ryu, “Analysis of blockchain smart contracts: Techniques and insights,” in 2020 IEEE Secure Development (SecDev), 2020, pp. 65–73.

[17] E. Lai and W. Luo, “Static analysis of integer overflow of smart contracts in ethereum,” in Proceedings of the 2020 4th International Conference on Cryptography, Security and Privacy, ser. ICCSP 2020. New York, NY, USA: Association for Computing Machinery, 2020, pp. 110–115. [Online]. Available: https://doi.org/10.1145/3377644.3377650 [18] Y. Xue, M. Ma, Y. Lin, Y. Sui, J. Ye, and T. Peng, “Cross-contract static analysis for detecting practical reentrancy vulnerabilities in smart contracts,” in 2020 35th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2020, pp. 1029–1040. [19] S. Akca, A. Rajan, and C. Peng, “Solanalyser: A framework for analysing and testing smart contracts,” in 2019 26th Asia-Pacific Software Engineering Conference (APSEC), 2019, pp. 482–489. [20] Y. Chinen, N. Yanai, J. P. Cruz, and S. Okamura, “Ra: Hunting for reentrancy attacks in ethereum smart contracts via static analysis,” in 2020 IEEE International Conference on Blockchain (Blockchain), 2020, pp. 327–336. [21] J. F. Ferreira, P. Cruz, T. Durieux, and R. Abreu, “Smartbugs: A framework to analyze solidity smart contracts,” CoRR, vol. abs/2007.04771, 2020. [Online]. Available: https://arxiv.org/abs/2007. 04771 [22] X. Yan, S. Wang, and K. Gai, “A semantic analysis-based method for smart contract vulnerability,” in 2022 IEEE 8th Intl Conference on Big Data Security on Cloud (BigDataSecurity), IEEE Intl Conference on High Performance and Smart Computing, (HPSC) and IEEE Intl Conference on Intelligent Data and Security (IDS), 2022, pp. 23–28. [23] N. Ivanov, C. Li, Q. Yan, Z. Sun, Z. Cao, and X. Luo, “Security threat mitigation for smart contracts: A comprehensive survey,” in ACM Computing Surveys, 2023. [Online]. Available: https://dl.acm.org/doi/10.1145/3593293 [24] D. He, R. Wu, X. Li, S. Chan, and M. Guizani, “Detection of vulnerabilities of blockchain smart contracts,” 2023. [Online]. Available: https://ieeexplore.ieee.org/document/10034747/ [25] C. Chen, J. Su, J. Chen, Y. Wang, T. Bi, J. Yu, Y. Wang, X. Lin, T. Chen, and Z. Zheng, “When chatgpt meets smart contract vulnerability detection: How far are we?” 2024. [Online]. Available: http://arxiv.org/abs/2309.05520 [26] Z. Chen, Y. Liu, S. M. Beillahi, Y. Li, and F. Long, “Demystifying invariant effectiveness for securing smart contracts,” 2024, pp. 1772– 1795. [Online]. Available: https://dl.acm.org/doi/10.1145/3660786 [27] Y. Sun, D. Wu, Y. Xue, H. Liu, H. Wang, Z. Xu, X. Xie, and Y. Liu, “Gptscan: Detecting logic vulnerabilities in smart contracts by combining gpt with program analysis,” pp. 1–13, 2024. [Online]. Available: https://dl.acm.org/doi/10.1145/3597503.3639117 [28] L. De Moura and N. Bjørner, “Z3: An efficient smt solver,” in Tools and Algorithms for the Construction and Analysis of Systems, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 14. Springer, 2008, pp. 337–340.

Related documents

• Practical Source Code Recovery from Binary Functions Using Anchor-Based Retrieval and LLM Reasoning#361503
• Systematic Codes Correcting Two Deletions with Three Redundant Symbols over Large Alphabets#1142860
• Looping Is Not Reliability: State-Bound Evidence and Typed Revision Contracts for Agentic Code Repair#405691
• Retention Without Activation: A Minimal Relational System of Failure Under Persistence#715282
• SCDBench: A Benchmark for LLM-Based Smart Contract Decompilers#238542