Chapter 4: Development¶

MIESC: Integrated Security Framework for Ethereum Contracts¶

4.1 Introduction¶

This chapter documents the development and implementation process of MIESC (Integrated Security Framework for Ethereum Contracts), an open-source framework designed to address the deficiencies identified in the smart contract auditing tools ecosystem. The exposition follows a structure that reflects the actual research process: from identifying concrete problems to the design decisions adopted to solve them, including dead ends encountered and lessons learned during development.

4.1.1 Project Genesis¶

The origin of MIESC lies in a practical auditing experience conducted in 2023, where the author faced the task of evaluating the security of a DeFi protocol with TVL (Total Value Locked) exceeding 50 million dollars. During that process, three problems became evident that academic literature had pointed out but that industry had not satisfactorily resolved:

First problem: Tool fragmentation. To perform a comprehensive audit, it was necessary to run Slither, Mythril, Echidna and request manual analysis with GPT-4. Each tool required independent installation, specific configuration, and produced results in incompatible formats. The time invested in orchestrating the tools exceeded the actual analysis time.

Second problem: Dependency on commercial services. Using GPT-4 for semantic analysis meant sending confidential source code to external servers. In the context of a pre-launch audit, where the code represents valuable intellectual property and potentially contains exploitable vulnerabilities, this transmission was unacceptable from a risk management perspective.

Third problem: Results interpretation. The tools collectively generated more than 200 findings, many of them duplicates or false positives. The task of consolidation, prioritization, and verification consumed several days of manual work.

These problems are not unique to the author's experience. Durieux et al. (2020), in their empirical evaluation of 47,587 contracts, documented that "no individual tool detects more than 75% of known vulnerabilities, and manual combination of tools is impractical at scale" (p. 535). Rameder et al. (2022) reached similar conclusions, noting that "the heterogeneity of interfaces and output formats constitutes a significant barrier to industrial adoption of academic tools" (p. 12).

4.1.2 Development Objectives¶

MIESC's technical objectives were formulated as a direct response to the identified problems, following the problem-driven design approach proposed by Shaw (2012):

1. Heterogeneous integration: Develop an abstraction layer that allows invoking multiple security tools through a unified interface, hiding differences in installation, configuration, and output format.

2. Defense in depth: Organize tools in complementary layers based on their analysis techniques, so that the strengths of some compensate for the weaknesses of others.

3. Results normalization: Implement a mapping schema that translates findings from each tool to standard taxonomies (SWC, CWE, OWASP), enabling automatic deduplication and prioritization.

4. Data sovereignty: Guarantee that all processing, including artificial intelligence analysis, executes locally without transmitting source code to external services.

5. Zero operational cost: Use exclusively open-source tools and open-weight language models, eliminating cost barriers that limit access to quality audits.

4.1.3 Quantitative Project Metrics¶

Table 4.1 presents project metrics in version 4.0.0, measured using standard code analysis tools.

Table 4.1. Quantitative metrics of MIESC v4.0.0 project

The maintainability index of 72.3 exceeds the threshold of 65 proposed by Oman and Hagemeister (1992) for "highly maintainable" code, which validates design decisions oriented toward extensibility.

4.2 System Architecture¶

4.2.1 The Defense-in-Depth Principle: Foundations and Application¶

MIESC's architecture is founded on the Defense-in-Depth (DiD) principle, a concept originated in military doctrine that was adapted to information systems security during the 1990s. The Department of Defense (1996) formalized this principle as "the application of multiple protective measures in series, so that an adversary must overcome or avoid each measure successively to compromise the protected system" (p. 3-12).

The application of this principle to smart contract analysis is an original contribution of this work. The theoretical justification is based on the empirical observation that different analysis techniques have complementary strengths and weaknesses:

Static analysis: Examines code without executing it, detecting known vulnerability patterns with high speed but without the ability to reason about runtime behavior. Feist et al. (2019) report that Slither achieves 82% precision but only 75% recall, indicating that approximately one in four vulnerabilities escapes detection.

Symbolic execution: Explores execution paths through symbolic representation of variables, capable of discovering vulnerabilities dependent on specific input values. Baldoni et al. (2018) document its effectiveness but also its main limitation: the combinatorial explosion of paths in complex code.

Fuzzing: Generates random or guided inputs to discover unexpected behaviors, particularly effective for finding edge cases not contemplated by the developer. Miller et al. (1990) established this technique, which Grieco et al. (2020) adapted specifically for smart contracts with Echidna.

Formal verification: Mathematically proves code properties through automated proof systems. Clarke et al. (2018) describe the theoretical foundations, while Lahav et al. (2022) document its practical application in Certora Prover.

AI analysis: Language models capable of detecting business logic vulnerabilities that require semantic understanding of code. Sun et al. (2024) demonstrate that GPTScan detects 90.2% of logic vulnerabilities that escape traditional tools.

Schneier (2000) articulates the underlying philosophy:

"Defense in depth recognizes that no individual security control is perfect. By implementing multiple layers, the probability that an attacker can evade all controls is reduced" (p. 284).

4.2.2 Selection Process: From Theory to Seven Layers¶

The decision to implement exactly seven layers was not arbitrary but the result of an iterative evaluation process. Initially, three alternative configurations were considered:

3-layer configuration (discarded): Grouped techniques into static analysis, dynamic analysis, and formal verification. This configuration, similar to that proposed by Atzei et al. (2017), was too coarse: within "dynamic analysis" coexisted fuzzing and symbolic execution, fundamentally different techniques that benefit from independent orchestration.

5-layer configuration (initial version): Separated static analysis, fuzzing, symbolic execution, formal verification, and AI analysis. This configuration, implemented in MIESC v1.0 and v2.0, proved functional but had two deficiencies: (1) it did not distinguish between coverage fuzzing and mutation testing, and (2) it grouped all AI techniques without differentiating property testing from semantic analysis.

7-layer configuration (final version): Result of refining the 5-layer configuration based on operational experience and the findings of Rameder et al. (2022), who argue that "categorization granularity directly affects orchestration and deduplication capability" (p. 18).

Table 4.2 presents the complementarity analysis that grounded the final selection.

Table 4.2. Complementarity analysis of techniques by vulnerability type

Note: Estimated effectiveness based on Durieux et al. (2020) and operational experience

4.2.3 Definitive Layer Model¶

Figure 7. MIESC Defense-in-Depth Architecture

Layer numbering reflects the typical execution order during an audit: faster techniques with lower computational cost (static analysis) execute first, allowing identification of obvious problems before investing resources in more expensive techniques (symbolic execution, formal verification).

4.2.4 Tool Selection Justification¶

The selection of the 25 tools that compose MIESC followed a structured evaluation process based on five criteria:

1. Demonstrated effectiveness: Preference for tools with empirical evaluation published in academic literature.

2. Compatible license: Exclusion of tools with licenses that would prevent redistribution or commercial use of the integrated framework.

3. Active maintenance: Preference for projects with recent commits and active community.

4. Complementarity: Avoid redundancy between tools of the same layer.

5. Installability: Capacity for automated installation without complex manual intervention.

Layer 1 - Static Analysis: Slither was selected as the main tool for its balance between precision (82%) and speed (1.2s average), according to benchmarks by Durieux et al. (2020). Solhint complements with style verification and best practices. Securify2 contributes Ethereum-specific security pattern analysis. Semgrep allows defining custom rules for organization-specific patterns.

Layer 2 - Fuzzing: Echidna, developed by Trail of Bits, was selected for its property-based testing capability specific to contracts. Foundry Fuzz contributes integration with the Foundry ecosystem, widely adopted in industry. Medusa provides coverage-based fuzzing with support for complex invariants. Vertigo implements mutation testing, a complementary technique that evaluates the quality of existing tests.

Layer 3 - Symbolic Execution: Mythril, also from Trail of Bits, was selected for its maturity and extensive documentation. Manticore contributes deeper analysis capabilities at the cost of longer execution time. Oyente, although less maintained, was included for its historical relevance and detection of specific patterns not covered by other tools.

Layer 4 - Invariant Testing: Scribble allows annotating contracts with specifications that are verified during execution. Halmos implements bounded model checking, verifying invariants up to a certain exploration depth.

Layer 5 - Formal Verification: SMTChecker is integrated into the Solidity compiler, providing formal verification without additional tools. Certora Prover, although commercial, was optionally included for its ability to verify complex properties that other tools cannot address.

Layer 6 - Property Testing: PropertyGPT uses LLM to generate test properties automatically. Aderyn implements security analysis with frequently updated rules. Wake provides a testing framework with property-based testing capabilities.

Layer 7 - AI Analysis: GPTScan implements the methodology of Sun et al. (2024). SmartLLM combines LLM with RAG (Retrieval-Augmented Generation) for contextualized analysis. LLMSmartAudit provides complete automated auditing. ThreatModel generates STRIDE threat models. GasGauge analyzes gas optimization. UpgradeGuard verifies upgrade pattern security. BestPractices evaluates adherence to documented best practices.

4.3 Software Design¶

4.3.1 The Heterogeneity Problem¶

Each security tool integrated in MIESC presents unique characteristics that hinder unified orchestration:

Diversity of invocation interfaces: Slither is invoked as a Python module, Mythril as a CLI command, Echidna requires YAML configuration files, Certora uses .conf files with its own syntax.

Heterogeneity of output formats: Slither produces structured JSON, Mythril generates formatted text or JSON depending on parameters, Echidna emits test logs, Manticore creates artifact directories.

Inconsistency in severity classification: Slither uses "High/Medium/Low/Informational", Mythril employs "Critical/High/Medium/Low", some tools do not classify severity.

Variability in location information: Some tools report file and line, others add column, others indicate function and contract, some only mention detector name.

This heterogeneity constitutes the main barrier to industrial adoption of academic tools, as documented by Rameder et al. (2022).

4.3.2 Solution: Adapter Pattern with SOLID Principles¶

The adopted solution combines the Adapter pattern, documented by Gamma et al. (1994), with SOLID principles proposed by Martin (2017). This combination is not casual: the Adapter pattern provides the structure to unify interfaces, while SOLID ensures the design is extensible and maintainable.

Single Responsibility Principle (SRP): Each adapter has a single responsibility: translate the interface of a specific tool to MIESC's common interface. The Slither adapter does not know about Mythril's existence, and vice versa.

Open/Closed Principle (OCP): The framework is open for extension (adding new adapters) but closed for modification (the core does not change when adding tools). To integrate a new tool, only implementing an adapter that fulfills the ToolAdapter interface is required.

Liskov Substitution Principle (LSP): All adapters are interchangeable through the ToolAdapter interface. The orchestrator can invoke any adapter without knowing its concrete implementation.

Interface Segregation Principle (ISP): The ToolAdapter interface defines only the essential methods that every adapter must implement, without imposing methods that only some tools would need.

Dependency Inversion Principle (DIP): MIESC's core depends on the ToolAdapter abstraction, not on concrete implementations like SlitherAdapter or MythrilAdapter.

Figure 8. Class diagram of the Adapter pattern in MIESC

4.3.3 Base Interface Implementation¶

The ToolAdapter interface is implemented using Python's abc (Abstract Base Classes) module, following recommendations from van Rossum et al. (2001):

from abc import ABC, abstractmethod
from typing import Dict, Any, List
from dataclasses import dataclass
from enum import Enum

class ToolAdapter(ABC):
    """
    Abstract interface for security tool adapters.

    This class defines the contract that every adapter must fulfill to
    integrate with MIESC. The design follows the Adapter pattern from Gamma
    et al. (1994) and SOLID principles from Martin (2017).

    The abstraction allows MIESC's orchestrator to work with
    any tool without knowing its implementation details,
    fulfilling the Dependency Inversion Principle.
    """

    @abstractmethod
    def get_metadata(self) -> 'ToolMetadata':
        """
        Returns standardized tool metadata.

        Metadata includes information about license, cost,
        and installation requirements, complying with DPGA (2023)
        transparency standards.
        """
        pass

    @abstractmethod
    def is_available(self) -> 'ToolStatus':
        """
        Verifies tool availability in the system.

        This method allows graceful degradation: if a tool
        is not installed, MIESC continues with the others instead of
        failing completely.
        """
        pass

    @abstractmethod
    def analyze(self, contract_path: str, **kwargs) -> Dict[str, Any]:
        """
        Executes security analysis on a contract.

        Args:
            contract_path: Absolute path to .sol file
            **kwargs: Tool-specific parameters
                     (timeout, max_depth, etc.)

        Returns:
            Dictionary with normalized MIESC structure containing
            status, findings, and analysis metadata.
        """
        pass

    @abstractmethod
    def normalize_findings(self, raw_output: Any) -> List[Dict[str, Any]]:
        """
        Normalizes findings to MIESC standard format.

        This method implements mapping from native classifications
        of each tool to standard taxonomies (SWC, CWE, OWASP).
        Normalization is essential for subsequent deduplication.
        """
        pass

4.4 Finding Normalization¶

4.4.1 The Vulnerability Babel Problem¶

Without normalization, findings from different tools are incomparable. Consider the following example of the same reentrancy vulnerability detected by three tools:

Slither:

{
  "check": "reentrancy-eth",
  "impact": "High",
  "confidence": "Medium",
  "elements": [{"source_mapping": {"filename": "Bank.sol", "lines": [42]}}]
}

Mythril:

==== State change after external call ====
SWC ID: 107
Severity: High
Contract: Bank
Function name: withdraw
PC address: 1234

GPTScan:

{
  "vulnerability": "Reentrancy vulnerability in withdraw function",
  "severity": "CRITICAL",
  "line": 42
}

Observations: - Slither calls the vulnerability "reentrancy-eth", Mythril uses "State change after external call", GPTScan says "Reentrancy vulnerability" - Slither uses "High", GPTScan uses "CRITICAL" (same concept, different nomenclature) - Only Mythril references the SWC-107 standard - The structural format is completely different

4.4.2 Solution: Mapping to Standard Taxonomies¶

MIESC implements a normalization schema that maps findings to three complementary taxonomies:

SWC (Smart Contract Weakness Classification): Specific taxonomy for smart contracts maintained by the Ethereum community (SCSVS, 2023). Contains 37 weakness categories with unique identifiers (SWC-100 to SWC-136).

CWE (Common Weakness Enumeration): General software weakness taxonomy maintained by MITRE (2024). Allows correlating smart contract vulnerabilities with known weaknesses in traditional software, facilitating communication with security teams not specialized in blockchain.

OWASP Smart Contract Top 10: List of most critical vulnerabilities developed by OWASP (2023), useful for executive prioritization.

4.4.3 Normalized Finding Format¶

The normalized finding format was designed following the SARIF (Static Analysis Results Interchange Format) standard from OASIS (2020), with specific extensions for smart contracts:

{
  "id": "MIESC-2024-001",
  "type": "reentrancy",
  "severity": "Critical",
  "confidence": 0.95,
  "location": {
    "file": "VulnerableBank.sol",
    "line": 42,
    "column": 8,
    "function": "withdraw",
    "contract": "VulnerableBank",
    "code_snippet": "(bool ok,) = msg.sender.call{value: amount}(\"\");"
  },
  "message": "Reentrancy vulnerability: external call before state update",
  "description": "The contract makes an external call to transfer Ether before updating the sender's balance. An attacker can re-enter the withdraw function before the balance is set to zero, allowing them to drain the contract's funds.",
  "recommendation": "Apply the Checks-Effects-Interactions pattern: update state before making external calls. Alternatively, use OpenZeppelin's ReentrancyGuard modifier.",
  "classifications": {
    "swc_id": "SWC-107",
    "cwe_id": "CWE-841",
    "owasp": "SC01:2023-Reentrancy"
  },
  "detected_by": ["slither", "mythril", "gptscan"],
  "references": [
    "https://swcregistry.io/docs/SWC-107",
    "https://consensys.github.io/smart-contract-best-practices/attacks/reentrancy/"
  ],
  "metadata": {
    "first_detected": "2024-11-29T14:30:00Z",
    "analysis_duration_ms": 1234,
    "miesc_version": "4.0.0"
  }
}

4.4.4 Mapping Tables¶

Mapping from native classifications to standards is implemented through correspondence tables manually validated against each tool's documentation and the SWC registry. Table 4.3 presents an extract.

Table 4.3. Extract of native classification mapping to standards

4.5 Layer Implementation¶

4.5.1 Layer 1: Static Analysis - The Entry Point¶

Static analysis constitutes the first line of defense for both technical and practical reasons. From a technical standpoint, static analysis does not require contract execution, allowing identification of problems even in code that does not compile. From a practical standpoint, its speed (typically less than 5 seconds per contract) allows rapid iteration during development.

4.5.2 Layer 3: Symbolic Execution - Exploring the Possible¶

Symbolic execution represents a qualitative leap from static analysis. While static analysis identifies syntactic patterns, symbolic execution explores the contract's possible state space, discovering vulnerabilities that depend on specific input values.

4.5.3 Layer 7: AI Analysis - Semantic Understanding¶

The artificial intelligence layer represents MIESC's most distinctive contribution. While previous layers detect technical patterns, AI can understand code semantics and detect business logic vulnerabilities that do not correspond to known patterns.

The decision to implement this layer with local models (Ollama) instead of commercial APIs (OpenAI, Anthropic) is based on three considerations:

1. Confidentiality: Pre-audit contract code is valuable intellectual property that should not be transmitted to third parties.

2. Cost: Commercial APIs generate significant costs at scale (estimated $2,500/year for 100 monthly audits).

3. Availability: Dependency on external APIs introduces failure points outside the auditor's control.

4.6 Orchestration and Deduplication¶

4.6.1 The Analysis Pipeline¶

Orchestration of the seven layers follows the Pipeline pattern proposed by Hohpe and Woolf (2003), adapted for parallel intra-layer and sequential inter-layer execution. This strategy maximizes throughput by taking advantage of the fact that tools within the same layer are independent of each other.

4.6.2 Deduplication Algorithm¶

Finding deduplication is critical for framework usability. Without deduplication, a vulnerability detected by five tools would appear five times in the report, hindering prioritization and consuming auditor time.

The implemented algorithm is inspired by record linkage techniques (Fellegi & Sunter, 1969), adapted to the specific domain of smart contract vulnerabilities.

4.7 Solutions to Technical Challenges Encountered¶

MIESC development faced several technical challenges not documented in literature. This section describes the problems encountered and implemented solutions, with the aim of facilitating the work of future researchers.

4.7.1 Manticore Incompatibility with Python 3.11¶

Identified problem: Manticore depends on the wasm library, which uses collections.Callable, an alias removed in Python 3.11 according to PEP 585.

Solution implemented: Patch at installation time that modifies the affected file.

4.7.2 Legacy Tool Containerization¶

Identified problem: Oyente requires old versions of dependencies (solc 0.4.x, z3 4.5.x) incompatible with modern development environments.

Solution implemented: Oyente execution in isolated Docker container.

4.7.3 Migration to Local AI Backend¶

Identified problem: GPTScan and similar tools require OpenAI API keys, which implies economic cost, external server transmission, and third-party availability dependency.

Solution implemented: Migration to Ollama for local language model execution.

4.8 Case Study: VulnerableBank Analysis¶

To concretely demonstrate MIESC's capabilities, a contract with known vulnerabilities was developed that allows evaluating framework effectiveness.

4.8.1 Test Contract¶

Listing 4.1. VulnerableBank contract with reentrancy vulnerability

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.19;

contract VulnerableBank {
    mapping(address => uint256) public balances;
    uint256 public totalDeposits;

    function deposit() public payable {
        require(msg.value > 0, "Deposit must be greater than 0");
        balances[msg.sender] += msg.value;
        totalDeposits += msg.value;
    }

    // VULNERABILITY: External call before state update
    function withdraw() public {
        uint256 balance = balances[msg.sender];
        require(balance > 0, "No balance to withdraw");

        (bool success, ) = msg.sender.call{value: balance}("");
        require(success, "Transfer failed");

        balances[msg.sender] = 0;
        totalDeposits -= balance;
    }
}

4.8.2 Multi-Layer Analysis Results¶

Table 4.4. VulnerableBank analysis results by layer

Total raw: 15 findings After deduplication: 6 unique findings Deduplication rate: 60%

4.9 User Interfaces¶

MIESC implements multiple interfaces to serve different use cases, following the separation of concerns principle (Dijkstra, 1982):

Table 4.5. MIESC interfaces and their use cases

4.10 Chapter References¶

Amdahl, G. M. (1967). Validity of the single processor approach to achieving large scale computing capabilities. Proceedings of the AFIPS Spring Joint Computer Conference, 483-485.

Atzei, N., Bartoletti, M., & Cimoli, T. (2017). A survey of attacks on Ethereum smart contracts. POST 2017, 164-186.

Baldoni, R., Coppa, E., D'Elia, D. C., Demetrescu, C., & Finocchi, I. (2018). A survey of symbolic execution techniques. ACM Computing Surveys, 51(3), 1-39.

Clarke, E. M., Henzinger, T. A., Veith, H., & Bloem, R. (Eds.). (2018). Handbook of model checking. Springer.

ConsenSys. (2023). Smart contract best practices. https://consensys.github.io/smart-contract-best-practices/

Department of Defense. (1996). MIL-HDBK-217F: Reliability prediction of electronic equipment.

Dijkstra, E. W. (1982). On the role of scientific thought. Selected Writings on Computing, 60-66.

Digital Public Goods Alliance. (2023). Digital Public Goods Standard. https://digitalpublicgoods.net/standard/

Durieux, T., Ferreira, J. F., Abreu, R., & Cruz, P. (2020). Empirical review of automated analysis tools on 47,587 Ethereum smart contracts. ICSE 2020, 530-541.

Feist, J., Grieco, G., & Groce, A. (2019). Slither: A static analysis framework for smart contracts. WETSEB 2019, 8-15.

Fellegi, I. P., & Sunter, A. B. (1969). A theory for record linkage. JASA, 64(328), 1183-1210.

Gamma, E., Helm, R., Johnson, R., & Vlissides, J. (1994). Design patterns: Elements of reusable object-oriented software. Addison-Wesley.

Grieco, G., Song, W., Cygan, A., Feist, J., & Groce, A. (2020). Echidna: Effective, usable, and fast fuzzing for smart contracts. ISSTA 2020, 557-560.

Hohpe, G., & Woolf, B. (2003). Enterprise integration patterns. Addison-Wesley.

King, J. C. (1976). Symbolic execution and program testing. Communications of the ACM, 19(7), 385-394.

Lahav, O., Grumberg, O., & Shoham, S. (2022). Automated verification of smart contracts with Certora Prover. ICSE-SEIP 2022, 45-54.

Martin, R. C. (2017). Clean architecture: A craftsman's guide to software structure and design. Prentice Hall.

Miller, B. P., Fredriksen, L., & So, B. (1990). An empirical study of the reliability of UNIX utilities. Communications of the ACM, 33(12), 32-44.

OASIS. (2020). Static Analysis Results Interchange Format (SARIF). https://docs.oasis-open.org/sarif/

Oman, P. W., & Hagemeister, J. (1992). Metrics for assessing a software system's maintainability. ICSM 1992, 337-344.

Rameder, H., Di Angelo, M., & Salzer, G. (2022). Review of automated vulnerability analysis of smart contracts on Ethereum. Frontiers in Blockchain, 5, 814977.

Schneier, B. (2000). Secrets and lies: Digital security in a networked world. Wiley.

SCSVS. (2023). Smart Contract Security Verification Standard. https://github.com/securing/SCSVS

Shaw, M. (2012). The role of design spaces. IEEE Software, 29(1), 46-50.

Sun, Y., et al. (2024). GPTScan: Detecting logic vulnerabilities in smart contracts by combining GPT with program analysis. ICSE 2024, 1-12.

Note: References follow APA 7^th edition format. Document updated: 2025-11-29