Security analysis tool for EVM bytecode. Supports smart contracts built for Ethereum, Hedera, Quorum, Vechain, Roostock, Tron and other EVM-compatible blockchains.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
mythril/tests/testdata/outputs_expected/ether_send.sol.o.jsonv2

46 lines
1.8 KiB

Balance modelling and symbolic sender variables (#1025) * add actor address to symbolic This will allow us to simulate semi-symbolic transaction senders * add value transfer to transaction global state creation * add proper balance tracking to world state and account * use address value vs string * disable actor address variable * use address directly * allow balance functions with int types * use value as getters since bitvecs aren't hashable * implement correct value transfer for suicide * use actor from actor pool * allow use of Or with *arg pattern * use bitvec instead of strings * add dynamic balance implementation to state datamodels * cleanup svm interface * use balance lambda in suicide op implementation * use bitvec instead of string address * update world state and account creation in symbolic * update tests to include overflow results * apply style rules * ignore previous open states for now * update native test to conform to new laser interface * fix incorrect types in the symbolic virtual machine * allow multiple types as input for address in account * fix type hint in symbolic.py * get int out of string in call * fix type in call op implementation * adapt test_transaction to conform to new laser interface * use static address to keep contracts from trying to enter themselves and make address type more dynamic * update evm test to conform to new laser interface * implement suicide to uncreated account * apply style rules * dynamically create colormap This removes the need for a globally maintained accountlist * get value out of address * add accounts getter * change symbolic test call to be valid with respect to the world state and account apis * remove dependency on globally recorded accounts * fix typing issues * fix type annotations in symbolic.py * fix remaining mypy warnings * simplify assertion check * execute lambda to get balance * make variable name plural * add documentation to svm constructor * use list comprehension to make code cleaner * remove comment * change variable name to plural * remove commented code * change variable name to conform to changed interface
6 years ago
[
{
"issues": [
{
"description": {
"head": "Anyone can withdraw ETH from the contract account.",
"tail": "Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent an equivalent amount of ETH to it. This is likely to be a vulnerability."
},
"extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>"
},
"locations": [
{
"sourceMap": "722:1:0"
}
],
"severity": "High",
"swcID": "SWC-105",
"swcTitle": "Unprotected Ether Withdrawal"
},
{
"description": {
"head": "The binary addition can overflow.",
"tail": "The operands of the addition operation are not sufficiently constrained. The addition could therefore result in an integer overflow. Prevent the overflow by checking inputs or ensure sure that the overflow is caught by an assertion."
},
"extra": {
"discoveryTime": "<DISCOVERY-TIME-DATA>"
},
"locations": [
{
"sourceMap": "883:1:0"
}
],
"severity": "High",
"swcID": "SWC-101",
"swcTitle": "Integer Overflow and Underflow"
}
],
Balance modelling and symbolic sender variables (#1025) * add actor address to symbolic This will allow us to simulate semi-symbolic transaction senders * add value transfer to transaction global state creation * add proper balance tracking to world state and account * use address value vs string * disable actor address variable * use address directly * allow balance functions with int types * use value as getters since bitvecs aren't hashable * implement correct value transfer for suicide * use actor from actor pool * allow use of Or with *arg pattern * use bitvec instead of strings * add dynamic balance implementation to state datamodels * cleanup svm interface * use balance lambda in suicide op implementation * use bitvec instead of string address * update world state and account creation in symbolic * update tests to include overflow results * apply style rules * ignore previous open states for now * update native test to conform to new laser interface * fix incorrect types in the symbolic virtual machine * allow multiple types as input for address in account * fix type hint in symbolic.py * get int out of string in call * fix type in call op implementation * adapt test_transaction to conform to new laser interface * use static address to keep contracts from trying to enter themselves and make address type more dynamic * update evm test to conform to new laser interface * implement suicide to uncreated account * apply style rules * dynamically create colormap This removes the need for a globally maintained accountlist * get value out of address * add accounts getter * change symbolic test call to be valid with respect to the world state and account apis * remove dependency on globally recorded accounts * fix typing issues * fix type annotations in symbolic.py * fix remaining mypy warnings * simplify assertion check * execute lambda to get balance * make variable name plural * add documentation to svm constructor * use list comprehension to make code cleaner * remove comment * change variable name to plural * remove commented code * change variable name to conform to changed interface
6 years ago
"meta": {},
"sourceFormat": "evm-byzantium-bytecode",
"sourceList": [
"0x3746c7c2ae7b0d4c3f8b1905df9a7ea169b9f93bec68a10a00b4c9d27a18c6fb"
],
"sourceType": "raw-bytecode"
}
]