Adds Manticore tool analysis report

tools/manticore-analysis/analysis.md

@@ -0,0 +1,66 @@
+# Manticore
+[Manticore](https://github.com/trailofbits/manticore) is a versatile symbolic execution tool that can analyze Ethereum Smart Contracts,
+Linux binaries, and Windows binaries. It's widely used for security auditing and testing of
+applications where security is paramount. Its main features include:
+- **Program Exploration**: executing a program with symbolic inputs and exploring all the possible states it can reach,
+- **Input Generation**: producing concrete inputs that result in a given program state,
+- **Error Discovery**: detecting crashes and other failure cases in binaries and Smart Contracts,
+- **Instrumentation**: providing fine-grained control of state exploration via event callbacks and instruction hooks,
+- **Programmatic Interface**: exposing programmatic access to its analysis engine via a Python API.
+
+Manticore can analyze the following types of programs:
+
+- Ethereum Smart Contracts (EVM bytecode)
+- Linux ELF binaries (x86, x86_64, aarch64, and ARMv7)
+- WASM Modules
+
+## Installation and execution:
+- Usage example (version 3.5):
+  - Install container orchestration software [docker compose](https://docs.docker.com/reference/cli/docker/compose/),
+  - Execute the following commands:
+    ```shell
+    docker-compose up -d
+    manticore examples/evm/umd_example.sol
+    ```
+
+> **Sidenotes**:
+> - Installing by PIP results in [protobuf incorrect version error](sample_execution/execution_errors.md#pip-instalation)
+(described better here: https://github.com/trailofbits/manticore/issues/2600)
+> - Build attempt with docker image version 3.7+ result in [attribute error](sample_execution/execution_errors.md#docker-v37-and-latest-)
+> - Build attempt with docker image version 3.6 results in [tool custom exception](sample_execution/execution_errors.md#docker-v36)
+> - Manticore may be built on docker image version 3.5. Execution example may be found [here](sample_execution/sample_execution.md),
+  and output files generated by the Manticore may be found under: `./Manticore/sample_execution_outputs`
+
+> **Support**:
+> This project is no longer internally developed and maintained. The team responsible for creating this tool announced its
+> readiness to review and accept small, well-written pull requests by the community (only bug fixes and minor
+> enhancements shall be considered). But there have veen no changes in the tool`s codebase since December 2022. All error
+> executions may be found in [this file](sample_execution/execution_errors.md)
+
+### Custom detector investigation
+Manticore has no documented ways to introduce new detectors. It requires adding a new detector class to [detectors.py](https://github.com/trailofbits/manticore/blob/master/manticore/ethereum/detectors.py) file and importing it in cli.py (for command line interface analysis).
+## Recommendations and possible investments in the tool:
+* Issues encountered in the latest versions of the application should be resolved.
+----
+# Guidelines for using Ethereum precompiles in Hedera:
+1. Hedera supports ED25519 accounts, ecrecover works correctly only for ECSDA accounts. This must be noted during potential
+   contract migration (Slither detector placed in this repository can be used to check for ecrecover usage in the contract to
+   migrate).
+2. There are precompiles which may be missing from Hedera EVM that are present in current EVM version.
+   For example Cancun-related updates are yet to be implemented as for end of April 2024.
+3. By the [docs](https://docs.hedera.com/hedera/sdks-and-apis/sdks/token-service/associate-tokens-to-an-account).
+   When using the Hedera Token Service it is important to check if the token is associated with the receiving account.
+4. List of pain points between Hedera EVM and vanilla Ethereum EVM:
+  - ECDSA aliases can be possibly changed in Hedera, which can lead to a new account address, this may influence whitelists
+    systems, transaction validation, and potential vulnerability in replay attacks and authorization issues,
+  - If a contract relies on specific addresses for functionality or permissions, redeploying or updating these contracts
+    may be necessary to align with new address formats.
+    More information [here](https://medium.com/@Arkhia/creating-an-ecdsa-based-account-with-an-alias-on-hedera-5d5d8b2cc1e9)
+  - OpenZeppelin - the most widely used library used in Solidity Smart Contracts. Contracts using ecrecover:
+    - ERC20Wrapper
+    - ERC2771Forwarder
+    - ERC721Wrapper
+    - ERC20Permit
+    - governance/utils/Votes
+    - Utils: EIP712Verifier, cryptography/ECDSA, SignatureChecker
+5. A list of differences between Hedera EVM and vanilla Ethereum EMV should be created and maintained. 

tools/manticore-analysis/docker-compose.yaml

@@ -0,0 +1,6 @@
+services:
+  manticore:
+    image: trailofbits/manticore:0.3.5
+    extra_hosts:
+      - "host.docker.internal:host-gateway"
+    entrypoint: ["sleep", "infinity"]

tools/manticore-analysis/sample_execution/036_error.md

@@ -0,0 +1,30 @@
+```shell
+2024-04-18 06:48:25,221: [84] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
+2024-04-18 06:48:25,223: [84] m.main:INFO: Beginning analysis
+2024-04-18 06:48:25,242: [84] m.e.manticore:INFO: Starting symbolic create contract
+2024-04-18 06:48:27,423: [84] m.e.manticore:INFO: Starting symbolic transaction: 0
+2024-04-18 06:48:30,698: [84] m.c.worker:ERROR: Exception in state 7: ManticoreError('Forking on unfeasible constraint set',)
+Traceback (most recent call last):
+  File "/usr/local/lib/python3.6/dist-packages/manticore/core/worker.py", line 132, in run
+    current_state.execute()
+  File "/usr/local/lib/python3.6/dist-packages/manticore/ethereum/state.py", line 8, in execute
+    return self._platform.execute()
+  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 3106, in execute
+    self.current_vm.execute()
+  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 1322, in execute
+    raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
+manticore.core.state.Concretize
+
+During handling of the above exception, another exception occurred:
+
+Traceback (most recent call last):
+  File "/usr/local/lib/python3.6/dist-packages/manticore/core/worker.py", line 153, in run
+    m._fork(current_state, exc.expression, exc.policy, exc.setstate)
+  File "/usr/local/lib/python3.6/dist-packages/manticore/core/manticore.py", line 516, in _fork
+    raise ManticoreError("Forking on unfeasible constraint set")
+manticore.exceptions.ManticoreError: Forking on unfeasible constraint set
+
+2024-04-18 06:48:30,737: [84] m.e.manticore:INFO: 0 alive states, 1 terminated states
+2024-04-18 06:48:31,102: [84] m.c.manticore:INFO: Results in /manticore/mcore_nr9y98__
+2024-04-18 06:48:31,104: [84] m.c.manticore:INFO: Total time: 3.663041591644287
+```

tools/manticore-analysis/sample_execution/037_error.md

@@ -0,0 +1,14 @@
+```shell
+2022-09-30 04:11:12,830: [5105] m.e.manticore:INFO: Starting symbolic create contract
+Process Process-1:
+Traceback (most recent call last):
+  File "/usr/lib/python3.8/multiprocessing/process.py", line 315, in _bootstrap
+    self.run()
+  File "/usr/lib/python3.8/multiprocessing/process.py", line 108, in run
+    self._target(*self._args, **self._kwargs)
+  File "/home/ubuntu/.local/lib/python3.8/site-packages/manticore/ethereum/manticore.py", line 1766, in worker_finalize
+    finalizer(q.get_nowait())
+  File "/home/ubuntu/.local/lib/python3.8/site-packages/manticore/ethereum/manticore.py", line 1757, in finalizer
+    if only_alive_states and last_tx.result in {"REVERT", "THROW", "TXERROR"}:
+AttributeError: 'NoneType' object has no attribute 'result'
+```

tools/manticore-analysis/sample_execution/execution_errors.md

@@ -0,0 +1,74 @@
+### PIP instalation:
+```Shell
+File ".../manticore-env/bin/manticore", line 5, in <module>
+    from manticore.__main__ import main
+  File ".../manticore-env/lib/python3.9/site-packages/manticore/__init__.py", line 10, in <module>
+    from .ethereum.manticore import ManticoreEVM
+  File ".../manticore-env/lib/python3.9/site-packages/manticore/ethereum/__init__.py", line 3, in <module>
+    from .manticore import ManticoreEVM, config
+  File ".../manticore-env/lib/python3.9/site-packages/manticore/ethereum/manticore.py", line 15, in <module>
+    from ..core.manticore import ManticoreBase, ManticoreError
+  File ".../manticore-env/lib/python3.9/site-packages/manticore/core/manticore.py", line 29, in <module>
+    from .worker import (
+  File ".../manticore-env/lib/python3.9/site-packages/manticore/core/worker.py", line 4, in <module>
+    from .state_pb2 import StateList, MessageList, State, LogMessage
+  File ".../manticore-env/lib/python3.9/site-packages/manticore/core/state_pb2.py", line 32, in <module>
+    _descriptor.EnumValueDescriptor(
+  File ".../manticore-env/lib/python3.9/site-packages/google/protobuf/descriptor.py", line 755, in __new__
+    _message.Message._CheckCalledFromGeneratedFile()
+TypeError: Descriptors cannot not be created directly.
+If this call came from a _pb2.py file, your generated code is out of date and must be regenerated with protoc >= 3.19.0.
+If you cannot immediately regenerate your protos, some other possible workarounds are:
+ 1. Downgrade the protobuf package to 3.20.x or lower.
+ 5. Set PROTOCOL_BUFFERS_PYTHON_IMPLEMENTATION=python (but this will use pure-Python parsing and will be much slower).
+```
+### Docker: v3.7 and :latest: 
+```Shell
+$ manticore --solc-remaps='@openzeppelin/contracts/utils/Context.sol=../../node_modules/@openzeppelin/contracts/utils/Context.sol @zk-kit/incremental-merkle-tree.sol/IncrementalBinaryTree.sol=../../node_modules/@zk-kit/incremental-merkle-tree.sol/IncrementalBinaryTree.sol' --contract=Semaphore ./contracts/Semaphore.sol
+2022-09-30 04:11:12,828: [5105] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
+2022-09-30 04:11:12,828: [5105] m.main:INFO: Beginning analysis
+2022-09-30 04:11:12,830: [5105] m.e.manticore:INFO: Starting symbolic create contract
+Process Process-1:
+Traceback (most recent call last):
+File "/usr/lib/python3.8/multiprocessing/process.py", line 315, in _bootstrap
+self.run()
+File "/usr/lib/python3.8/multiprocessing/process.py", line 108, in run
+self._target(*self._args, **self._kwargs)
+File "/home/ubuntu/.local/lib/python3.8/site-packages/manticore/ethereum/manticore.py", line 1766, in worker_finalize
+finalizer(q.get_nowait())
+File "/home/ubuntu/.local/lib/python3.8/site-packages/manticore/ethereum/manticore.py", line 1757, in finalizer
+if only_alive_states and last_tx.result in {"REVERT", "THROW", "TXERROR"}:
+AttributeError: 'NoneType' object has no attribute 'result'
+```
+### Docker: v3.6
+
+```Shell
+2024-04-18 06:48:25,221: [84] m.main:INFO: Registered plugins: IntrospectionAPIPlugin, <class 'manticore.ethereum.plugins.SkipRevertBasicBlocks'>, <class 'manticore.ethereum.plugins.FilterFunctions'>
+2024-04-18 06:48:25,223: [84] m.main:INFO: Beginning analysis
+2024-04-18 06:48:25,242: [84] m.e.manticore:INFO: Starting symbolic create contract
+2024-04-18 06:48:27,423: [84] m.e.manticore:INFO: Starting symbolic transaction: 0
+2024-04-18 06:48:30,698: [84] m.c.worker:ERROR: Exception in state 7: ManticoreError('Forking on unfeasible constraint set',)
+Traceback (most recent call last):
+  File "/usr/local/lib/python3.6/dist-packages/manticore/core/worker.py", line 132, in run
+    current_state.execute()
+  File "/usr/local/lib/python3.6/dist-packages/manticore/ethereum/state.py", line 8, in execute
+    return self._platform.execute()
+  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 3106, in execute
+    self.current_vm.execute()
+  File "/usr/local/lib/python3.6/dist-packages/manticore/platforms/evm.py", line 1322, in execute
+    raise Concretize("Symbolic PC", expression=expression, setstate=setstate, policy="ALL")
+manticore.core.state.Concretize
+
+During handling of the above exception, another exception occurred:
+
+Traceback (most recent call last):
+  File "/usr/local/lib/python3.6/dist-packages/manticore/core/worker.py", line 153, in run
+    m._fork(current_state, exc.expression, exc.policy, exc.setstate)
+  File "/usr/local/lib/python3.6/dist-packages/manticore/core/manticore.py", line 516, in _fork
+    raise ManticoreError("Forking on unfeasible constraint set")
+manticore.exceptions.ManticoreError: Forking on unfeasible constraint set
+
+2024-04-18 06:48:30,737: [84] m.e.manticore:INFO: 0 alive states, 1 terminated states
+2024-04-18 06:48:31,102: [84] m.c.manticore:INFO: Results in /manticore/mcore_nr9y98__
+2024-04-18 06:48:31,104: [84] m.c.manticore:INFO: Total time: 3.663041591644287
+```

tools/manticore-analysis/sample_execution/outputs/.state_id

@@ -0,0 +1 @@
+83

tools/manticore-analysis/sample_execution/outputs/.testcase_id

@@ -0,0 +1 @@
+31

tools/manticore-analysis/sample_execution/outputs/command.sh

@@ -0,0 +1 @@
+/usr/local/bin/manticore examples/evm/umd_example.sol

tools/manticore-analysis/sample_execution/outputs/global.findings

@@ -0,0 +1,5 @@
+- INVALID instruction -
+  Contract: 0xd4a8f68534750318596cd9a395ee5d2468a8492d  EVM Program counter: 0xf4
+  Solidity snippet:
+    25  assert(x + y + z != 3)
+

tools/manticore-analysis/sample_execution/outputs/global.summary

@@ -0,0 +1,2 @@
+Global runtime coverage:
+d4a8f68534750318596cd9a395ee5d2468a8492d: 99.35%

tools/manticore-analysis/sample_execution/outputs/global_SymExExample.init_asm

@@ -0,0 +1,175 @@
+    0: PUSH1 0x80
+    2: PUSH1 0x40
+    4: MSTORE
+    5: CALLVALUE
+    6: DUP1
+    7: ISZERO
+    8: PUSH2 0x10
+    b: JUMPI
+    c: PUSH1 0x0
+    e: DUP1
+    f: REVERT
+   10: JUMPDEST
+   11: POP
+   12: PUSH2 0x129
+   15: DUP1
+   16: PUSH2 0x20
+   19: PUSH1 0x0
+   1b: CODECOPY
+   1c: PUSH1 0x0
+   1e: RETURN
+   1f: STOP
+   20: PUSH1 0x80
+   22: PUSH1 0x40
+   24: MSTORE
+   25: PUSH1 0x4
+   27: CALLDATASIZE
+   28: LT
+   29: PUSH1 0x3f
+   2b: JUMPI
+   2c: PUSH1 0x0
+   2e: CALLDATALOAD
+   2f: PUSH29 0x100000000000000000000000000000000000000000000000000000000
+   4d: SWAP1
+   4e: DIV
+   4f: PUSH4 0xffffffff
+   54: AND
+   55: DUP1
+   56: PUSH4 0x7eda09e8
+   5b: EQ
+   5c: PUSH1 0x44
+   5e: JUMPI
+   5f: JUMPDEST
+   60: PUSH1 0x0
+   62: DUP1
+   63: REVERT
+   64: JUMPDEST
+   65: CALLVALUE
+   66: DUP1
+   67: ISZERO
+   68: PUSH1 0x4f
+   6a: JUMPI
+   6b: PUSH1 0x0
+   6d: DUP1
+   6e: REVERT
+   6f: JUMPDEST
+   70: POP
+   71: PUSH1 0x80
+   73: PUSH1 0x4
+   75: DUP1
+   76: CALLDATASIZE
+   77: SUB
+   78: DUP2
+   79: ADD
+   7a: SWAP1
+   7b: DUP1
+   7c: DUP1
+   7d: CALLDATALOAD
+   7e: SWAP1
+   7f: PUSH1 0x20
+   81: ADD
+   82: SWAP1
+   83: SWAP3
+   84: SWAP2
+   85: SWAP1
+   86: DUP1
+   87: CALLDATALOAD
+   88: SWAP1
+   89: PUSH1 0x20
+   8b: ADD
+   8c: SWAP1
+   8d: SWAP3
+   8e: SWAP2
+   8f: SWAP1
+   90: DUP1
+   91: CALLDATALOAD
+   92: SWAP1
+   93: PUSH1 0x20
+   95: ADD
+   96: SWAP1
+   97: SWAP3
+   98: SWAP2
+   99: SWAP1
+   9a: POP
+   9b: POP
+   9c: POP
+   9d: PUSH1 0x82
+   9f: JUMP
+   a0: JUMPDEST
+   a1: STOP
+   a2: JUMPDEST
+   a3: PUSH1 0x0
+   a5: DUP1
+   a6: PUSH1 0x0
+   a8: DUP1
+   a9: SWAP3
+   aa: POP
+   ab: PUSH1 0x0
+   ad: SWAP2
+   ae: POP
+   af: PUSH1 0x0
+   b1: SWAP1
+   b2: POP
+   b3: PUSH1 0x0
+   b5: DUP7
+   b6: EQ
+   b7: ISZERO
+   b8: ISZERO
+   b9: PUSH1 0xbf
+   bb: JUMPI
+   bc: PUSH32 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe
+   dd: SWAP3
+   de: POP
+   df: JUMPDEST
+   e0: PUSH1 0x5
+   e2: DUP6
+   e3: SLT
+   e4: ISZERO
+   e5: PUSH1 0xe5
+   e7: JUMPI
+   e8: PUSH1 0x0
+   ea: DUP7
+   eb: EQ
+   ec: DUP1
+   ed: ISZERO
+   ee: PUSH1 0xd7
+   f0: JUMPI
+   f1: POP
+   f2: PUSH1 0x0
+   f4: DUP5
+   f5: EQ
+   f6: ISZERO
+   f7: JUMPDEST
+   f8: ISZERO
+   f9: PUSH1 0xe0
+   fb: JUMPI
+   fc: PUSH1 0x1
+   fe: SWAP2
+   ff: POP
+  100: JUMPDEST
+  101: PUSH1 0x2
+  103: SWAP1
+  104: POP
+  105: JUMPDEST
+  106: PUSH1 0x3
+  108: DUP2
+  109: DUP4
+  10a: DUP6
+  10b: ADD
+  10c: ADD
+  10d: EQ
+  10e: ISZERO
+  10f: ISZERO
+  110: ISZERO
+  111: PUSH1 0xf5
+  113: JUMPI
+  114: INVALID
+  115: JUMPDEST
+  116: POP
+  117: POP
+  118: POP
+  119: POP
+  11a: POP
+  11b: POP
+  11c: JUMP
+  11d: STOP