Symbolic Execution

Smart contract auditing is a crucial step in ensuring the security and reliability of blockchain applications. Accelchain employs Symbolic Execution as a powerful technique for auditing contracts, identifying vulnerabilities, and adhering to the guidelines specified by the Ethereum.org SWC (Smart Contract Weaknesses and Common Vulnerabilities) Registry.

Symbolic Execution Overview

Definition: Symbolic Execution involves systematically exploring possible program states by running contract bytecode and its dependencies through a compiler.
Process: The contract is executed symbolically, and the analysis encompasses multiple transactions and potential states.

Compiler Integration

Comprehensive Analysis: Accelchain integrates with a compiler to analyze contract bytecode thoroughly.
Dependency Consideration: The process includes all dependencies, such as imported contracts, ensuring a holistic approach to auditing.

Test Case Generation:

SWC IDs and Test Cases: Test cases are designed with a focus on SWC IDs specified by the Ethereum.org registry.
Exploration of States: Test cases systematically explore various program states, identifying potential vulnerabilities.

Audit Report Generation:

Detailed Information: The resulting audit report provides detailed information on identified vulnerabilities.
Report Components: SWC Error ID, Error Title, Function with the error, lines containing the error, and severity are included.
Severity Levels: Issues are categorized by severity, allowing prioritization based on the criticality of each vulnerability.

Note that Accelchain's symbolic execution is targeted at finding common vulnerabilities, and is not able to discover issues in the business logic of an application. Furthermore, symbolic executors are generally unsound, as they are often unable to explore all possible states of a program.

To overcome this, Accelchain provides users with a combined comprehensive Audit Report based on findings generated from multiple features like for static analysis, Symbolic execution etc.

PreviousAudit NextAI Static Analysis

Last updated 1 year ago

Symbolic Execution Overview

Definition: Symbolic Execution involves systematically exploring possible program states by running contract bytecode and its dependencies through a compiler.
Process: The contract is executed symbolically, and the analysis encompasses multiple transactions and potential states.

Compiler Integration

Comprehensive Analysis: Accelchain integrates with a compiler to analyze contract bytecode thoroughly.
Dependency Consideration: The process includes all dependencies, such as imported contracts, ensuring a holistic approach to auditing.

Test Case Generation:

SWC IDs and Test Cases: Test cases are designed with a focus on SWC IDs specified by the Ethereum.org registry.
Exploration of States: Test cases systematically explore various program states, identifying potential vulnerabilities.

Audit Report Generation:

Detailed Information: The resulting audit report provides detailed information on identified vulnerabilities.
Report Components: SWC Error ID, Error Title, Function with the error, lines containing the error, and severity are included.
Severity Levels: Issues are categorized by severity, allowing prioritization based on the criticality of each vulnerability.

To overcome this, Accelchain provides users with a combined comprehensive Audit Report based on findings generated from multiple features like for static analysis, Symbolic execution etc.