## SmartExecutor ##
SmartExecutor is a guided symbolic execution tool for security analysis on EVM bytecode. It is designed to reduce the sequence explosion of symbolic execution to provide a scalable solution to symbolic execution while trying to maximize code coverage. It has a dual-phase process. In Phase 1, it symbolically executes all possible function sequences within the given depth limit.
Phase 2 then targets the not-fully-covered functions based on instruction coverage. This is the phase where the guidance takes place. SmartExecutor can direct the execution flow by prioritizing the states more significant to the target functions and selecting the functions at states to be executed that are more likely to cover the targets. The state significance value calculation and the function selection are based on static data dependency analysis and runtime execution data like function coverage and target functions.
This is the [link](https://ieeexplore.ieee.org/document/10316942) to our conference paper: SmartExecutor: Coverage-Driven Symbolic Execution Guided by a Function Dependency Graph.
### Run SmartExecutor through Docker:
1, Pull the Docker image of SmartExecutor:
```bash
$ sudo docker pull 23278942/smartexecutor
```
2, Run SmartExecutor with a single Docker command. Replace a_host_directory with the path to your host directory containing the Solidity file, for example, Crowdsale.sol.
```bash
$ sudo docker run -it --rm -v a_host_directory:/home/smartExecutor/ image_id analyze ./Crowdsale.sol:Crowdsale
```
This command mounts the host directory to a directory inside the container and analyzes the contract Crowdsale defined in the Solidity file Crowdsale.sol.
To analyze the sample Solidity file provided with the Docker image, you can use the following command:
```bash
$ sudo docker run -it --rm image_id analyze /opt/smartExecutor/tests/testdata/solidity_files/Crowdsale.sol:Crowdsale
```
3, Additional Options
To see more intermediate data, add the -v option followed by a value (3 or larger):
```bash
$ sudo docker run -it --rm image_id -v 3 analyze /opt/smartExecutor/tests/testdata/solidity_files/Crowdsale.sol:Crowdsale
```
Click [here](./example_output/Crowdsale.sol_terminal_output.txt) to see the terminal output.
Click [here](./example_output/Crowdsale.sol_terminal_output_verbose.txt) to see the verbose intermediate results printed out in the terminal.
<!--
Example of running SmartExecutor inside the Docker container
```
# create and enter the Docker container that mounts a host directory to a directory inside the created container
sudo docker run -it --rm -v a_host_directory:/home/smartExecutor/ --entrypoint /bin/bash docker_image_id
# call SmartExecutor to execute Contract Crowdsale defined in the Solidity file Crowdsale.sol
semyth analyze ./Crowdsale.sol:Crowdsale
# set option '-v' to 3 to show the verbose intermediate results
semyth -v 3 analyze ./Crowdsale.sol:Crowdsale
```
-->
### Run SmartExecutor in Pycharm IDE:
1, Create a project through Pycharm IDE by cloning https://github.com/contractAnalysis/smartExecutor.git.
2, Create a virtual environment and install dependencies.
3, Find semyth.py in the root directory and add the parameters. Take the example of Crowdsale.sol:
```
analyze
./tests/testdata/solidity_files/Crowdsale.sol:Crowdsale
```
4, Run semyth.py by right clicking it and select "Run semyth".
### Using SmartExecutor as a Command-Line Tool
Install SmartExecutor through pip:
```
pip install smartExecutorx
```
Run SmartExecutor:
```bash
$ semyth analyze <solidity-file>:<contract-name>
```
Replace <solidity-file> with the path to your Solidity file and <contract-name> with the name of the contract you want to analyze.
<!--
Note that the usage of SmartExecutor is almost the same as Mythril except that you have to begin with **semyth** instead of **myth** and you need to include the option **-fdg**, which is used to signal that the scalable alternative is in active. When **-fdg** is not given, SmartExecutor runs the basic model, i.e., Mythril itself.
For this reason, here show some useful documents of Mythril:
- [Instructions for using Mythril](https://mythril-classic.readthedocs.io/en/master/)
- [Mythril's documentation](https://mythril-classic.readthedocs.io/en/develop/)
- [Vulnerability Remediation](https://swcregistry.io/)
-->
If you find this tool helpful, we would appreciate it if you could cite it. Here is the BibTex:
```json
@INPROCEEDINGS{10316942,
author={Wei, Qiping and Sikder, Fadul and Feng, Huadong and Lei, Yu and Kacker, Raghu and Kuhn, Richard},
booktitle={2023 5th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS)},
title={SmartExecutor: Coverage-Driven Symbolic Execution Guided by a Function Dependency Graph},
year={2023},
volume={},
number={},
pages={1-8},
keywords={Codes;Limiting;Smart contracts;Explosions;Ethereum smart contract;symbolic execution;vulnerability detection;sequence explosion;function dependency},
doi={10.1109/BRAINS59668.2023.10316942}}
```
Raw data
{
"_id": null,
"home_page": "https://github.com/contractAnalysis/smartExecutor",
"name": "smartExecutorx",
"maintainer": null,
"docs_url": null,
"requires_python": ">=3.8.0",
"maintainer_email": null,
"keywords": "hacking disassembler security ethereum",
"author": "contractAnalysis",
"author_email": null,
"download_url": "https://files.pythonhosted.org/packages/76/c2/e5ac47d097f6176c081c9badacf5cd0853aad0faa91c5a9624ded161f3b0/smartExecutorx-4.0.0.tar.gz",
"platform": null,
"description": "\r\n\r\n## SmartExecutor ##\r\n\r\nSmartExecutor is a guided symbolic execution tool for security analysis on EVM bytecode. It is designed to reduce the sequence explosion of symbolic execution to provide a scalable solution to symbolic execution while trying to maximize code coverage. It has a dual-phase process. In Phase 1, it symbolically executes all possible function sequences within the given depth limit.\r\n\r\nPhase 2 then targets the not-fully-covered functions based on instruction coverage. This is the phase where the guidance takes place. SmartExecutor can direct the execution flow by prioritizing the states more significant to the target functions and selecting the functions at states to be executed that are more likely to cover the targets. The state significance value calculation and the function selection are based on static data dependency analysis and runtime execution data like function coverage and target functions.\r\n\r\n\r\nThis is the [link](https://ieeexplore.ieee.org/document/10316942) to our conference paper: SmartExecutor: Coverage-Driven Symbolic Execution Guided by a Function Dependency Graph. \r\n\r\n\r\n\r\n### Run SmartExecutor through Docker: \r\n\r\n1, Pull the Docker image of SmartExecutor:\r\n```bash\r\n$ sudo docker pull 23278942/smartexecutor\r\n```\r\n\r\n2, Run SmartExecutor with a single Docker command. Replace a_host_directory with the path to your host directory containing the Solidity file, for example, Crowdsale.sol.\r\n```bash\r\n$ sudo docker run -it --rm -v a_host_directory:/home/smartExecutor/ image_id analyze ./Crowdsale.sol:Crowdsale\r\n```\r\nThis command mounts the host directory to a directory inside the container and analyzes the contract Crowdsale defined in the Solidity file Crowdsale.sol.\r\n\r\nTo analyze the sample Solidity file provided with the Docker image, you can use the following command:\r\n```bash\r\n$ sudo docker run -it --rm image_id analyze /opt/smartExecutor/tests/testdata/solidity_files/Crowdsale.sol:Crowdsale \r\n```\r\n\r\n3, Additional Options\r\n\r\nTo see more intermediate data, add the -v option followed by a value (3 or larger):\r\n```bash\r\n$ sudo docker run -it --rm image_id -v 3 analyze /opt/smartExecutor/tests/testdata/solidity_files/Crowdsale.sol:Crowdsale \r\n```\r\n\r\nClick [here](./example_output/Crowdsale.sol_terminal_output.txt) to see the terminal output.\r\n\r\nClick [here](./example_output/Crowdsale.sol_terminal_output_verbose.txt) to see the verbose intermediate results printed out in the terminal.\r\n\r\n<!--\r\nExample of running SmartExecutor inside the Docker container\r\n```\r\n# create and enter the Docker container that mounts a host directory to a directory inside the created container\r\nsudo docker run -it --rm -v a_host_directory:/home/smartExecutor/ --entrypoint /bin/bash docker_image_id \r\n\r\n# call SmartExecutor to execute Contract Crowdsale defined in the Solidity file Crowdsale.sol\r\nsemyth analyze ./Crowdsale.sol:Crowdsale\r\n\r\n# set option '-v' to 3 to show the verbose intermediate results\r\nsemyth -v 3 analyze ./Crowdsale.sol:Crowdsale \r\n\r\n```\r\n-->\r\n\r\n\r\n### Run SmartExecutor in Pycharm IDE:\r\n\r\n1, Create a project through Pycharm IDE by cloning https://github.com/contractAnalysis/smartExecutor.git.\r\n\r\n2, Create a virtual environment and install dependencies.\r\n\r\n3, Find semyth.py in the root directory and add the parameters. Take the example of Crowdsale.sol:\r\n```\r\nanalyze\r\n./tests/testdata/solidity_files/Crowdsale.sol:Crowdsale\r\n```\r\n4, Run semyth.py by right clicking it and select \"Run semyth\".\r\n\r\n\r\n### Using SmartExecutor as a Command-Line Tool\r\n\r\nInstall SmartExecutor through pip:\r\n```\r\npip install smartExecutorx\r\n```\r\n\r\nRun SmartExecutor:\r\n\r\n```bash\r\n$ semyth analyze <solidity-file>:<contract-name>\r\n```\r\nReplace <solidity-file> with the path to your Solidity file and <contract-name> with the name of the contract you want to analyze. \r\n\r\n<!--\r\nNote that the usage of SmartExecutor is almost the same as Mythril except that you have to begin with **semyth** instead of **myth** and you need to include the option **-fdg**, which is used to signal that the scalable alternative is in active. When **-fdg** is not given, SmartExecutor runs the basic model, i.e., Mythril itself.\r\n\r\nFor this reason, here show some useful documents of Mythril:\r\n\r\n- [Instructions for using Mythril](https://mythril-classic.readthedocs.io/en/master/)\r\n- [Mythril's documentation](https://mythril-classic.readthedocs.io/en/develop/)\r\n- [Vulnerability Remediation](https://swcregistry.io/)\r\n-->\r\nIf you find this tool helpful, we would appreciate it if you could cite it. Here is the BibTex:\r\n```json\r\n@INPROCEEDINGS{10316942,\r\n author={Wei, Qiping and Sikder, Fadul and Feng, Huadong and Lei, Yu and Kacker, Raghu and Kuhn, Richard},\r\n booktitle={2023 5th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS)}, \r\n title={SmartExecutor: Coverage-Driven Symbolic Execution Guided by a Function Dependency Graph}, \r\n year={2023},\r\n volume={},\r\n number={},\r\n pages={1-8},\r\n keywords={Codes;Limiting;Smart contracts;Explosions;Ethereum smart contract;symbolic execution;vulnerability detection;sequence explosion;function dependency},\r\n doi={10.1109/BRAINS59668.2023.10316942}}\r\n\r\n```\r\n",
"bugtrack_url": null,
"license": "MIT",
"summary": "Security analysis tool for Ethereum smart contracts",
"version": "4.0.0",
"project_urls": {
"Homepage": "https://github.com/contractAnalysis/smartExecutor"
},
"split_keywords": [
"hacking",
"disassembler",
"security",
"ethereum"
],
"urls": [
{
"comment_text": "",
"digests": {
"blake2b_256": "76c2e5ac47d097f6176c081c9badacf5cd0853aad0faa91c5a9624ded161f3b0",
"md5": "5e047d984f4b4a8e2286a6a057ffc7e2",
"sha256": "80c25777003e44fb4e361aaa4338f5720b5844c25249c9976a29ec151926ae7d"
},
"downloads": -1,
"filename": "smartExecutorx-4.0.0.tar.gz",
"has_sig": false,
"md5_digest": "5e047d984f4b4a8e2286a6a057ffc7e2",
"packagetype": "sdist",
"python_version": "source",
"requires_python": ">=3.8.0",
"size": 4584560,
"upload_time": "2024-05-01T17:35:43",
"upload_time_iso_8601": "2024-05-01T17:35:43.151241Z",
"url": "https://files.pythonhosted.org/packages/76/c2/e5ac47d097f6176c081c9badacf5cd0853aad0faa91c5a9624ded161f3b0/smartExecutorx-4.0.0.tar.gz",
"yanked": false,
"yanked_reason": null
}
],
"upload_time": "2024-05-01 17:35:43",
"github": true,
"gitlab": false,
"bitbucket": false,
"codeberg": false,
"github_user": "contractAnalysis",
"github_project": "smartExecutor",
"travis_ci": false,
"coveralls": false,
"github_actions": false,
"circle": true,
"requirements": [
{
"name": "blake2b-py",
"specs": []
},
{
"name": "coloredlogs",
"specs": [
[
">=",
"10.0"
]
]
},
{
"name": "coincurve",
"specs": [
[
">=",
"13.0.0"
]
]
},
{
"name": "cython",
"specs": []
},
{
"name": "cytoolz",
"specs": [
[
"<",
"0.12.0"
]
]
},
{
"name": "asn1crypto",
"specs": [
[
">=",
"0.22.0"
]
]
},
{
"name": "configparser",
"specs": [
[
">=",
"3.5.0"
]
]
},
{
"name": "coverage",
"specs": [
[
"<",
"7.0"
],
[
">",
"6.0"
]
]
},
{
"name": "py_ecc",
"specs": [
[
">=",
"1.4.7"
],
[
"<",
"5.0.0"
]
]
},
{
"name": "eth_abi",
"specs": [
[
"<",
"3.0.0"
],
[
">=",
"2.0.0b4"
]
]
},
{
"name": "eth-account",
"specs": [
[
"<",
"0.6.0"
],
[
">=",
"0.5.6"
]
]
},
{
"name": "ethereum-input-decoder",
"specs": [
[
">=",
"0.2.2"
]
]
},
{
"name": "eth-hash",
"specs": [
[
"<",
"0.4.0"
],
[
">=",
"0.3.1"
]
]
},
{
"name": "eth-keyfile",
"specs": [
[
"<",
"0.6.0"
],
[
">=",
"0.5.1"
]
]
},
{
"name": "eth-keys",
"specs": [
[
"<",
"0.4.0"
],
[
">=",
"0.2.1"
]
]
},
{
"name": "eth-rlp",
"specs": [
[
"<",
"0.3.0"
],
[
">=",
"0.1.0"
]
]
},
{
"name": "eth-typing",
"specs": [
[
"<",
"3.0.0"
],
[
">=",
"2.1.0"
]
]
},
{
"name": "eth-utils",
"specs": [
[
"<",
"2"
]
]
},
{
"name": "hexbytes",
"specs": [
[
"<",
"0.3.0"
]
]
},
{
"name": "jinja2",
"specs": [
[
">=",
"2.9"
]
]
},
{
"name": "MarkupSafe",
"specs": [
[
"<",
"2.1.0"
]
]
},
{
"name": "mock",
"specs": []
},
{
"name": "mypy-extensions",
"specs": [
[
"<",
"1.0.0"
]
]
},
{
"name": "persistent",
"specs": [
[
">=",
"4.2.0"
]
]
},
{
"name": "py-flags",
"specs": []
},
{
"name": "py-evm",
"specs": [
[
"==",
"0.5.0a1"
]
]
},
{
"name": "py-solc-x",
"specs": []
},
{
"name": "py-solc",
"specs": []
},
{
"name": "pytest",
"specs": [
[
">=",
"3.6.0"
]
]
},
{
"name": "pyparsing",
"specs": [
[
">=",
"2.0.2"
],
[
"<",
"3"
]
]
},
{
"name": "pytest-cov",
"specs": []
},
{
"name": "pytest_mock",
"specs": []
},
{
"name": "requests",
"specs": []
},
{
"name": "rlp",
"specs": [
[
"<",
"3"
]
]
},
{
"name": "semantic_version",
"specs": []
},
{
"name": "transaction",
"specs": [
[
">=",
"2.2.1"
]
]
},
{
"name": "typing-extensions",
"specs": [
[
"<",
"4"
],
[
">=",
"3.7.4"
]
]
},
{
"name": "z3-solver",
"specs": [
[
">=",
"4.8.8.0"
]
]
},
{
"name": "matplotlib",
"specs": []
},
{
"name": "pre-commit",
"specs": [
[
"<",
"2.21.0"
]
]
},
{
"name": "certifi",
"specs": [
[
">=",
"2020.06.20"
]
]
}
],
"tox": true,
"lcname": "smartexecutorx"
}
JSON
