Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

support for Uniswap v2 testing workflow #393

Open
Tracked by #346
karmacoma-eth opened this issue Oct 14, 2024 · 0 comments
Open
Tracked by #346

support for Uniswap v2 testing workflow #393

karmacoma-eth opened this issue Oct 14, 2024 · 0 comments
Labels
bug Something isn't working

Comments

@karmacoma-eth
Copy link
Collaborator

karmacoma-eth commented Oct 14, 2024

Describe the bug

Different sha3_expr in in create2 init code lead to different inferred address vs actually deployed address.

In the example below, uniswapV2Factory.createPair(address(token), address(weth)) results in the following sha3_expr:

sha3_expr=f_sha3_680(Concat(372682917519380244141939632342652170012265661726725,
              f_sha3_320(4184670640661422675847470105623367512667768574483259588612),
              f_sha3_93088(...init code concrete value...)))

But in the pairFor helper function, this is the expression used:

    pair = address(uint(keccak256(abi.encodePacked(
            hex'ff',
            factory,
            keccak256(abi.encodePacked(token0, token1)),
            hex'96e8ac4277198ff8b6f785478aa9a39f403cb768dd02cbee326c3e7da348845f' // init code hash
        ))));

(note the hardcoded initcode hash value)

On the halmos side, it results in the following sha3_expr:

sha3_expr=f_sha3_680(Concat(372682917519380244141939632342652170012265661726725, f_sha3_320(4184670640661422675847470105623367512667768574483259588612), 68258024698789349894765071221733254692395760896603232917352833510768193864799))

If we were to evaluate f_sha3_93088(...init code concrete value...) concretely, we would indeed get the same value:

keccak(bytes.fromhex(hex(a)[2:])).hex()
'96e8ac4277198ff8b6f785478aa9a39f403cb768dd02cbee326c3e7da348845f'

Because of the sha3_expr mismatch, pairFor returns a different address (bbbb0011) than the address actually deployed (bbbb000b) and subsequent calls fail

To Reproduce

necessary steps from https://github.com/igorganich/damn-vulnerable-defi-halmos/blob/master/test/puppet-v2/PuppetV2_Halmos.t.sol#L86 (h/t @igorganich)

    function setUp() public {
        // Deploy tokens to be traded
        token = new DamnValuableToken();
        weth = new WETH();

        // Deploy Uniswap V2 Factory and Router
        uniswapV2Factory = IUniswapV2Factory(/* deploy here */);
        uniswapV2Router = IUniswapV2Router02(/* deploy here */);

        // Create Uniswap pair
        address pair = uniswapV2Factory.createPair(address(token), address(weth));
        address inferredPair = pairFor(address(uniswapV2Factory), address(token), address(weth));
        assertEq(deployedPair, inferredPair);
    }
@karmacoma-eth karmacoma-eth added the bug Something isn't working label Oct 14, 2024
@daejunpark daejunpark mentioned this issue Nov 13, 2024
17 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant