Open huzhanchi opened 2 weeks ago
EVM hashes the function uniswapV3SwapCallback and encodes it in the first 4 bytes of the call data.
You can find this hash using solidity by executing solc --hashes <filename>
where the filename contains the functionuniswapV3SwapCallback along with its correct arguments.
Assume the hash you get from solc is something like fa461e33
, the following will be the constraints:
calldata[0] == 250
(i.e., int("fa", 16) == 250
)calldata[1] == 70
calldata[2] == 30
calldata[3] == 51
You can access the calldata by directly indexing the indices 0, 1, 2, and 3
You can access the calldata by directly indexing the indices 0, 1, 2, and 3 Hi norhh,thanks for reply. "state.environment.calldata" is the right way to get calldata in Mythril detect module ?
It is a BitVec
Maybe I got the the reason,in the attack process, "functionuniswapV3SwapCallback " should be callback from another contract. So SymbolicCalldata do not contain concrete data.
It is not meant to contain concrete calldata. You have to add it as a constraint and run the solver to check if you are executing the desired function.
It is not meant to contain concrete calldata. You have to add it as a constraint and run the solver to check if you are executing the desired function.
I misunderstood the information given in the debug like "If(2_calldatasize <= 0, 0, 2_calldata[0])", and then I directly made an equal operation on the BitVec, it worked! Thanks for your patience.
Hi, another issue. I have write a module.there are two cases, one is detected as expected, another is not. this module has two additional constraints:
for the second constraint, mainly refer the function "is_unique_jumpdest" of "ArbitraryJump"
module core logic
def is_unique_sender(sender: BitVec, state: GlobalState) -> bool:
try:
# 0x fa 46 1e 33
b0 = symbol_factory.BitVecVal(250, 256)
b1 = symbol_factory.BitVecVal(70, 256)
b2 = symbol_factory.BitVecVal(30, 256)
b3 = symbol_factory.BitVecVal(51, 256)
constraints = state.world_state.constraints + [state.environment.calldata[0] == b0,state.environment.calldata[1] == b1,state.environment.calldata[2] == b2,state.environment.calldata[3] == b3]
model = get_model(constraints)
except UnsatError:
return True, constraints
concrete_jump_dest = model.eval(sender.raw, model_completion=True)
try:
constraints += [symbol_factory.BitVecVal(concrete_jump_dest.as_long(), 256) != sender]
model = get_model(constraints)
except UnsatError:
return True, constraints
return False, constraints
def _analyze_state(self, state):
state = copy(state)
instruction = state.get_current_instruction()
# 0x fa 46 1e 33
b0 = symbol_factory.BitVecVal(250, 256)
b1 = symbol_factory.BitVecVal(70, 256)
b2 = symbol_factory.BitVecVal(30, 256)
b3 = symbol_factory.BitVecVal(51, 256)
sender = state.environment.sender
(is_unique, constraints) = is_unique_sender(sender, state)
if is_unique is True:
return []
test case malicious contract
Whether there is "require(msg.sender == lp_address)" or not, detect result in my expection. And also apply a modifier also work well too.
contract VulnCallback {
address public lp_address = 0x1E227979f0b5BC691a70DEAed2e0F39a6F538FD5;
function uniswapV3SwapCallback(int256 amount0Delta, int256 amount1Delta, bytes calldata data) external {
require(msg.sender == lp_address);
payable(0x48Af6Ec8f9105c6a4a984ACa6D5E064629e3B7Db).transfer(address(this).balance);
}
}
variable "pool0" could be controlled arbitrary from the malicious CALLER lp contract, at that point "msg.sender" could be any one. The following test contract has no detected issue.
contract VulnCallback {
address public lp_address = 0x1E227979f0b5BC691a70DEAed2e0F39a6F538FD5;
function uniswapV3SwapCallback(int256 amount0Delta, int256 amount1Delta, bytes calldata data) external {
(address caller, address pool0, uint24 fee1) = abi.decode(data,(address, address, uint24));
require(msg.sender == address(pool0), "not authorized");
payable(0x48Af6Ec8f9105c6a4a984ACa6D5E064629e3B7Db).transfer(address(this).balance);
}
}
Mythril restricts the user addresses to the list of ACTORS
, which you can find in mythril.laser.ethereum.transaction.symbolic
In this case you can either construct 3 different constraints pertaining to the 3 actors or construct one constraint pertaining to "SOMEGUY" from the class Actors
Description
In the Defi protocol, it is very common to use "uniswapV3SwapCallback" like interface function to receive the callbak from LP, However some implementation of uniswapV3SwapCallback has no premission controll. Just as the uniswap official give the caution:
You can also check the background in my article here:
refer:https://medium.com/@zhanchihu/watch-your-back-while-you-want-to-do-aribitrage-with-uniswap-flashloan-f456e4f3e99d
Tests
todo
Implementation details
I want to implement a module to hook the CALL instruction, and give the constraint like
Now, my problem is how can I get the selector in the current CALL instruction. I have checked the "state.environment.calldata", and will to extract the selector, but in debug mode it look like this![image](https://github.com/Consensys/mythril/assets/7611082/c2b31b96-3028-4bd4-9fb6-08ac9daa9e1b)
Is there any convient way for me to get selector?