ucsb-seclab / greed

A symbolic execution engine for EVM smart contract binaries.
https://ucsb-seclab.github.io/greed/
MIT License
73 stars 10 forks source link

AssertionError: Invalid bv_unsigned_value of non constant bitvector #24

Closed Wzy-source closed 4 weeks ago

Wzy-source commented 2 months ago

Ubuntu 22.04 LTS I followed the tutorial to install and compile the code, but the following error occurred in the running example

Traceback (most recent call last):
  File "/home/wzy/Gala/test.py", line 3, in <module>
    p = Project(target_dir="/home/wzy/contract/")
  File "/home/wzy/Gala/greed/greed/project.py", line 41, in __init__
    self.function_at = self.tac_parser.parse_functions()
  File "/home/wzy/Gala/greed/greed/TAC/TAC_parser.py", line 279, in parse_functions
    function = TAC_Function(block_id, signature, high_level_name, is_public, blocks, formals)
  File "/home/wzy/Gala/greed/greed/function.py", line 37, in __init__
    self.callprivate_source_target = self._get_callprivate_source_target()
  File "/home/wzy/Gala/greed/greed/function.py", line 56, in _get_callprivate_source_target
    target_bb_id = hex(bv_unsigned_value(stmt.arg1_val))
  File "/home/wzy/Gala/greed/greed/solver/shortcuts.py", line 122, in bv_unsigned_value
    return _SOLVER.bv_unsigned_value(bv)
  File "/home/wzy/Gala/greed/greed/solver/yices2.py", line 58, in bv_unsigned_value
    assert self.is_concrete(
AssertionError: Invalid bv_unsigned_value of non constant bitvector

Could you tell me how to solve it? Thank you

Wzy-source commented 2 months ago

source code:

from greed import Project
if __name__ == '__main__':
    p = Project(target_dir="/home/wzy/contract/")
degrigis commented 2 months ago

Hey there! Interesting, somehow the lifting done by Gigahorse produced some unexpected values. Would it be possible to share with us the contract test-case? @Wzy-source

Wzy-source commented 2 months ago

Okay, this is the source code I used for testing. You can also find it in the Ethereum mainnet 0x0000000000ffe8b47b3e2130213b802212439497

/**
 *Submitted for verification at Etherscan.io on 2019-07-30
*/

pragma solidity 0.5.10; // optimization enabled, 99999 runs, evm: petersburg

/**
 * @title Immutable Create2 Contract Factory
 * @author 0age
 * @notice This contract provides a safeCreate2 function that takes a salt value
 * and a block of initialization code as arguments and passes them into inline
 * assembly. The contract prevents redeploys by maintaining a mapping of all
 * contracts that have already been deployed, and prevents frontrunning or other
 * collisions by requiring that the first 20 bytes of the salt are equal to the
 * address of the caller (this can be bypassed by setting the first 20 bytes to
 * the null address). There is also a view function that computes the address of
 * the contract that will be created when submitting a given salt or nonce along
 * with a given block of initialization code.
 * @dev This contract has not yet been fully tested or audited - proceed with
 * caution and please share any exploits or optimizations you discover.
 */
contract ImmutableCreate2Factory {
  // mapping to track which addresses have already been deployed.
  mapping(address => bool) private _deployed;

  /**
   * @dev Create a contract using CREATE2 by submitting a given salt or nonce
   * along with the initialization code for the contract. Note that the first 20
   * bytes of the salt must match those of the calling address, which prevents
   * contract creation events from being submitted by unintended parties.
   * @param salt bytes32 The nonce that will be passed into the CREATE2 call.
   * @param initializationCode bytes The initialization code that will be passed
   * into the CREATE2 call.
   * @return Address of the contract that will be created, or the null address
   * if a contract already exists at that address.
   */
  function safeCreate2(
    bytes32 salt,
    bytes calldata initializationCode
  ) external payable containsCaller(salt) returns (address deploymentAddress) {
    // move the initialization code from calldata to memory.
    bytes memory initCode = initializationCode;

    // determine the target address for contract deployment.
    address targetDeploymentAddress = address(
      uint160(                    // downcast to match the address type.
        uint256(                  // convert to uint to truncate upper digits.
          keccak256(              // compute the CREATE2 hash using 4 inputs.
            abi.encodePacked(     // pack all inputs to the hash together.
              hex"ff",            // start with 0xff to distinguish from RLP.
              address(this),      // this contract will be the caller.
              salt,               // pass in the supplied salt value.
              keccak256(          // pass in the hash of initialization code.
                abi.encodePacked(
                  initCode
                )
              )
            )
          )
        )
      )
    );

    // ensure that a contract hasn't been previously deployed to target address.
    require(
      !_deployed[targetDeploymentAddress],
      "Invalid contract creation - contract has already been deployed."
    );

    // using inline assembly: load data and length of data, then call CREATE2.
    assembly {                                // solhint-disable-line
      let encoded_data := add(0x20, initCode) // load initialization code.
      let encoded_size := mload(initCode)     // load the init code's length.
      deploymentAddress := create2(           // call CREATE2 with 4 arguments.
        callvalue,                            // forward any attached value.
        encoded_data,                         // pass in initialization code.
        encoded_size,                         // pass in init code's length.
        salt                                  // pass in the salt value.
      )
    }

    // check address against target to ensure that deployment was successful.
    require(
      deploymentAddress == targetDeploymentAddress,
      "Failed to deploy contract using provided salt and initialization code."
    );

    // record the deployment of the contract to prevent redeploys.
    _deployed[deploymentAddress] = true;
  }

  /**
   * @dev Compute the address of the contract that will be created when
   * submitting a given salt or nonce to the contract along with the contract's
   * initialization code. The CREATE2 address is computed in accordance with
   * EIP-1014, and adheres to the formula therein of
   * `keccak256( 0xff ++ address ++ salt ++ keccak256(init_code)))[12:]` when
   * performing the computation. The computed address is then checked for any
   * existing contract code - if so, the null address will be returned instead.
   * @param salt bytes32 The nonce passed into the CREATE2 address calculation.
   * @param initCode bytes The contract initialization code to be used.
   * that will be passed into the CREATE2 address calculation.
   * @return Address of the contract that will be created, or the null address
   * if a contract has already been deployed to that address.
   */
  function findCreate2Address(
    bytes32 salt,
    bytes calldata initCode
  ) external view returns (address deploymentAddress) {
    // determine the address where the contract will be deployed.
    deploymentAddress = address(
      uint160(                      // downcast to match the address type.
        uint256(                    // convert to uint to truncate upper digits.
          keccak256(                // compute the CREATE2 hash using 4 inputs.
            abi.encodePacked(       // pack all inputs to the hash together.
              hex"ff",              // start with 0xff to distinguish from RLP.
              address(this),        // this contract will be the caller.
              salt,                 // pass in the supplied salt value.
              keccak256(            // pass in the hash of initialization code.
                abi.encodePacked(
                  initCode
                )
              )
            )
          )
        )
      )
    );

    // return null address to signify failure if contract has been deployed.
    if (_deployed[deploymentAddress]) {
      return address(0);
    }
  }

  /**
   * @dev Compute the address of the contract that will be created when
   * submitting a given salt or nonce to the contract along with the keccak256
   * hash of the contract's initialization code. The CREATE2 address is computed
   * in accordance with EIP-1014, and adheres to the formula therein of
   * `keccak256( 0xff ++ address ++ salt ++ keccak256(init_code)))[12:]` when
   * performing the computation. The computed address is then checked for any
   * existing contract code - if so, the null address will be returned instead.
   * @param salt bytes32 The nonce passed into the CREATE2 address calculation.
   * @param initCodeHash bytes32 The keccak256 hash of the initialization code
   * that will be passed into the CREATE2 address calculation.
   * @return Address of the contract that will be created, or the null address
   * if a contract has already been deployed to that address.
   */
  function findCreate2AddressViaHash(
    bytes32 salt,
    bytes32 initCodeHash
  ) external view returns (address deploymentAddress) {
    // determine the address where the contract will be deployed.
    deploymentAddress = address(
      uint160(                      // downcast to match the address type.
        uint256(                    // convert to uint to truncate upper digits.
          keccak256(                // compute the CREATE2 hash using 4 inputs.
            abi.encodePacked(       // pack all inputs to the hash together.
              hex"ff",              // start with 0xff to distinguish from RLP.
              address(this),        // this contract will be the caller.
              salt,                 // pass in the supplied salt value.
              initCodeHash          // pass in the hash of initialization code.
            )
          )
        )
      )
    );

    // return null address to signify failure if contract has been deployed.
    if (_deployed[deploymentAddress]) {
      return address(0);
    }
  }

  /**
   * @dev Determine if a contract has already been deployed by the factory to a
   * given address.
   * @param deploymentAddress address The contract address to check.
   * @return True if the contract has been deployed, false otherwise.
   */
  function hasBeenDeployed(
    address deploymentAddress
  ) external view returns (bool) {
    // determine if a contract has been deployed to the provided address.
    return _deployed[deploymentAddress];
  }

  /**
   * @dev Modifier to ensure that the first 20 bytes of a submitted salt match
   * those of the calling account. This provides protection against the salt
   * being stolen by frontrunners or other attackers. The protection can also be
   * bypassed if desired by setting each of the first 20 bytes to zero.
   * @param salt bytes32 The salt value to check against the calling address.
   */
  modifier containsCaller(bytes32 salt) {
    // prevent contract submissions from being stolen from tx.pool by requiring
    // that the first 20 bytes of the submitted salt match msg.sender.
    require(
      (address(bytes20(salt)) == msg.sender) ||
      (bytes20(salt) == bytes20(0)),
      "Invalid salt - first 20 bytes of the salt must match calling address."
    );
    _;
  }
}

(env) wzy:~/Gala-2.0$ which python /home/wzy/Gala-2.0/env/bin/python (env) wzy:~/Gala-2.0$ python Python 3.10.12 (main, Nov 20 2023, 15:14:05) [GCC 11.4.0] on linux Type "help", "copyright", "credits" or "license" for more information. > from greed import Project > Project("/home/wzy/test_contract/") Traceback (most recent call last): File "", line 1, in File "/home/wzy/Gala-2.0/greed/greed/project.py", line 41, in init self.function_at = self.tac_parser.parse_functions() File "/home/wzy/Gala-2.0/greed/greed/TAC/TAC_parser.py", line 279, in parse_functions function = TAC_Function(block_id, signature, high_level_name, is_public, blocks, formals) File "/home/wzy/Gala-2.0/greed/greed/function.py", line 37, in init self.callprivate_source_target = self._get_callprivate_source_target() File "/home/wzy/Gala-2.0/greed/greed/function.py", line 56, in _get_callprivate_source_target target_bb_id = hex(bv_unsigned_value(stmt.arg1_val)) File "/home/wzy/Gala-2.0/greed/greed/solver/shortcuts.py", line 122, in bv_unsigned_value return _SOLVER.bv_unsigned_value(bv) File "/home/wzy/Gala-2.0/greed/greed/solver/yices2.py", line 58, in bv_unsigned_value assert self.is_concrete( AssertionError: Invalid bv_unsigned_value of non constant bitvector

robmcl4 commented 2 months ago

Interesting, I fail to replicate. Unfortunately we've been rather poor with proper version numbering. Can you get us some git commit hashes?

in greed: git rev-parse HEAD, and in greed/gigahorse-toolchain: git rev-parse HEAD

for the record, I failed to repro using greed commit 5e3b64f6 and gigahorse commit 800cdff3

degrigis commented 2 months ago

@Wzy-source ^^^

lcfr-eth commented 1 month ago

solved this today by cd yices2 && git checkout 8e6297e then rerunning setup.sh

this reverts to use the last release version instead of master from git which introduces breaking changes.

khvitri commented 1 month ago

solved this today by cd yices2 && git checkout 8e6297e then rerunning setup.sh

this reverts to use the last release version instead of master from git which introduces breaking changes.

This worked for some reason.