diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 7bc009862..ef4a0acef 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -61,6 +61,7 @@ jobs: # Install solc unconditionally because it only takes a second or two sudo wget -O /usr/bin/solc https://github.com/ethereum/solidity/releases/download/v0.4.24/solc-static-linux sudo chmod +x /usr/bin/solc + pip install coveralls pip install -e ".[dev-noks]" - name: Run Tests env: @@ -68,15 +69,22 @@ jobs: run: | cp scripts/run_tests.sh . ./run_tests.sh - - name: Coverage Upload - uses: codecov/codecov-action@v1 + - name: Coveralls Parallel + run: | + coveralls + env: + COVERALLS_PARALLEL: true + COVERALLS_REPO_TOKEN: ${{ secrets.COVERALLS_REPO_TOKEN }} + # Send notification when all tests have finished to combine coverage results + coverage-finish: + needs: tests + runs-on: ubuntu-latest + steps: + - name: Coveralls Finished + uses: coverallsapp/github-action@v1.1.1 with: - token: ${{ secrets.CODECOV_TOKEN }} - file: ./coverage.xml - yml: ./codecov.yml -# Disabled this line because Codecov has been extra flaky lately, and having to re-run the entire -# test suite until every coverage upload step succeeds is more of a hassle than it's worth. -# fail_ci_if_error: true + github-token: ${{ secrets.GITHUB_TOKEN }} + parallel-finished: true upload: runs-on: ubuntu-latest if: github.event_name == 'schedule' diff --git a/README.md b/README.md index 2f1cc147d..0375b0499 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ [![Build Status](https://img.shields.io/github/workflow/status/trailofbits/manticore/CI/master)](https://github.com/trailofbits/manticore/actions?query=workflow%3ACI) -[![Codecov](https://img.shields.io/codecov/c/github/trailofbits/manticore)](https://codecov.io/github/trailofbits/manticore) +[![Coverage Status](https://coveralls.io/repos/github/trailofbits/manticore/badge.svg)](https://coveralls.io/github/trailofbits/manticore) [![PyPI Version](https://badge.fury.io/py/manticore.svg)](https://badge.fury.io/py/manticore) [![Slack Status](https://empireslacking.herokuapp.com/badge.svg)](https://empireslacking.herokuapp.com) [![Documentation Status](https://readthedocs.org/projects/manticore/badge/?version=latest)](http://manticore.readthedocs.io/en/latest/?badge=latest) @@ -78,7 +78,8 @@ Manticore has a command line interface which can perform a basic symbolic analys Analysis results will be placed into a workspace directory beginning with `mcore_`. For information about the workspace, see the [wiki](https://github.com/trailofbits/manticore/wiki/What's-in-the-workspace%3F). #### EVM -Solidity smart contracts must have a `.sol` extension for analysis by Manticore. See a [demo](https://asciinema.org/a/154012). +Manticore CLI automatically detects you are trying to test a contract if (for ex.) + the contract has a `.sol` or a `.vy` extension. See a [demo](https://asciinema.org/a/154012).
Click to expand: @@ -99,6 +100,12 @@ $ manticore examples/evm/umd_example.sol ```
+##### Manticore-verifier + +An alternative CLI tool is provided that simplifys contract testing and +allows writing properties methods in the same high-level language the contract uses. +Checkout manticore-verifier [documentation](http://manticore.readthedocs.io/en/latest/verifier.html). +See a [demo](https://asciinema.org/a/xd0XYe6EqHCibae0RP6c7sJVE) #### Native
diff --git a/codecov.yml b/codecov.yml deleted file mode 100644 index bb6dccece..000000000 --- a/codecov.yml +++ /dev/null @@ -1,12 +0,0 @@ -comment: false - -codecov: - notify: - # We have 9 test steps that produce coverage data. - # If we add or remove any, we need to change this number. - after_n_builds: 9 - wait_for_ci: yes - status: - project: - default: - threshold: 0.2% diff --git a/docs/index.rst b/docs/index.rst index 049b77883..57bd7e570 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -9,6 +9,7 @@ Manticore is a symbolic execution tool for analysis of binaries and smart contra :maxdepth: 2 :caption: Contents: + verifier base worker states diff --git a/docs/verifier.rst b/docs/verifier.rst new file mode 100644 index 000000000..67e3c7771 --- /dev/null +++ b/docs/verifier.rst @@ -0,0 +1,172 @@ +Property based symbolic executor: manticore-verifier +==================================================== +Manticore installs a separated CLI tool to do property based symbolic execution of smart contracts. :: + + $ manticore-verifier your_contract.sol + +**manticore-verifier** initializes an emulated blockchain environment with a configurable set of +accounts and then sends various symbolic transactions to the target contract containing property methods. +If a way to break a property is found the full transaction trace to reproduce the behaivor is provided. +A configurable stopping condition bounds the exploration, properties not failing are considered to pass. + + +Writing properties in {Solidity/ Vyper} +--------------------------------------- +**manticore-verifier** will detect and test property methods written in the +original contract language. A property can be written in the original language +by simply naming a method in a specific way. For example methods names starting with ```crytic_```. + +.. code-block:: javascript + + function crytic_test_true_property() view public returns (bool){ + return true; + } + +You can select your own way to name property methods using the ``--propre`` commandline argument. :: + + --propre PROPRE A regular expression for selecting properties + +Normal properties +^^^^^^^^^^^^^^^^^ +In the most common case after some precondition is met some logic property must always be true. +Normal properties are property methods that must always return true (or REVERT). + + +Reverting properties +^^^^^^^^^^^^^^^^^^^^ +Sometimes it is difficult to detect that a revert has happened in an internal transaction. +manticore-verifier allows to test for ALWAYS REVERTing property methods. +Revert properties are property methods that must always REVERT. +Reverting property are any property method that contains "revert". For example: + +.. code-block:: javascript + + function crytic_test_must_always_revert() view public returns (bool){ + return true; + } + + +Selecting a target contract +=========================== +**manticore-verifier** needs to be pointed to a the target contract containing any number of property methods. +The target contract is the entry point of the exploration. It needs to initilize any internal structure or external contracts to a correct initial state. All methods of this contract matching the property name criteria will be tested. :: + + --contract_name CONTRACT_NAME The target contract name defined in the source code + + +User accounts +============= +You can specify what are the accounts used in the exploration. +Normaly you do not want the owner or deployer of the contract to send the symbolic transaction and to use a separate unused account to actually check the property methods. +There are 3 types of user accounts: + + - deployer: The account used to create the target contract + - senders: A set of accounts used to send symbolic transactions. Think that these transactions are the ones trying to put the contract in a state that makes the property fail. + - psender: The account used as caller to test the actual property methods + + +You can specify those via command line arguments :: + + --deployer DEPLOYER (optional) address of account used to deploy the contract + --senders SENDERS (optional) a comma separated list of sender addresses. + The properties are going to be tested sending + transactions from these addresses. + --psender PSENDER (optional) address from where the property is tested + + +Or, if you prefer, you can specify a yaml file like this :: + + deployer: "0x41414141414141414141" + sender: ["0x51515151515151515151", "0x52525252525252525252"] + psender: "0x616161616161616161" + +If you specify the accounts both ways the commandline takes precedence over the yaml file. +If you do not provide specific accounts **manticore-verifier** will choose them for you. + + +Stopping condition +================== +The exploration will continue to send symbolic transactions until one of the stopping criteria is met. + +Maximum number of transactions +----------------------------- +You can be interested only in what could happen under a number of transactions. After a maximun number of transactions is reached the explorations ends. Properties that had not be found to be breakable are considered a pass. +You can modify the max number of transactions to test vis a command line argument, otherwise it will stop at 3 transactions. :: + + --maxt MAXT Max transaction count to explore + +Maximun coverage % attained +--------------------------- +By default, if a transaction does not produce new coverage, the exploration is stopped. But you can add a further constraint so that if the provided coverage percentage is obtained, stop. Note that this is the total % of runtime bytecode covered. By default, compilers add dead code, and also in this case the runtime contains the code of the properties methods. So use with care. :: + + --maxcov MAXCOV Stop after maxcov % coverage is obtained in the main + contract + + +Timeout +------- +Exploration will stop after the timeout seconds have pass. :: + + --timeout TIMEOUT Exploration timeout in seconds + + +Walkthrough +----------- +Consider this little contract containing a bug: + +.. code-block:: javascript + + contract Ownership{ // It can have an owner! + address owner = msg.sender; + function Onwer() public{ + owner = msg.sender; + } + modifier isOwner(){ + require(owner == msg.sender); + _; + } + } + contract Pausable is Ownership{ //It is also pausable. You can pause it. You can resume it. + bool is_paused; + modifier ifNotPaused(){ + require(!is_paused); + _; + } + function paused() isOwner public{ + is_paused = true; + } + function resume() isOwner public{ + is_paused = false; + } + } + contract Token is Pausable{ //<< HERE it is. + mapping(address => uint) public balances; // It maintains a balance sheet + function transfer(address to, uint value) ifNotPaused public{ //and can transfer value + balances[msg.sender] -= value; // from one account + balances[to] += value; // to the other + } + } + +Assuming the programmer did not want to allow the magic creation of tokens. +We can design a property around the fact that the initial token count can not be increased over time. Even more relaxed, after the contract creation any account must have less that total count of tokens. The property looks like this : + +.. code-block:: javascript + + contract TestToken is Token{ + constructor() public{ + //here lets initialize the thing + balances[msg.sender] = 10000; //deployer account owns it all! + } + + function crytic_test_balance() view public returns (bool){ + return balances[msg.sender] <= 10000; //nobody can have more than 100% of the tokens + } + + } + +And you can unleash the verifier like this:: + + $manticore-verifier testtoken.sol --contract TestToken + + +f/ diff --git a/manticore/core/manticore.py b/manticore/core/manticore.py index f924008ce..321071c16 100644 --- a/manticore/core/manticore.py +++ b/manticore/core/manticore.py @@ -62,7 +62,7 @@ def to_class(self): ) consts.add("procs", default=10, description="Number of parallel processes to spawn") -proc_type = MProcessingType.multiprocessing +proc_type = MProcessingType.threading if sys.platform != "linux": logger.warning("Manticore is only supported on Linux. Proceed at your own risk!") proc_type = MProcessingType.threading diff --git a/manticore/ethereum/verifier.py b/manticore/ethereum/verifier.py index d156ac911..dd9e0b859 100644 --- a/manticore/ethereum/verifier.py +++ b/manticore/ethereum/verifier.py @@ -167,7 +167,7 @@ def manticore_verifier( print(f"# Owner account: 0x{int(owner_account):x}") print(f"# Contract account: 0x{int(contract_account):x}") for n, user_account in enumerate(user_accounts): - print(f"# Sender_{n} account: 0x{int(checker_account):x}") + print(f"# Sender_{n} account: 0x{int(user_account):x}") print(f"# PSender account: 0x{int(checker_account):x}") properties = {} @@ -200,7 +200,7 @@ def manticore_verifier( f"Failing properties: 0/{len(properties)}" ) with m.kill_timeout(timeout=timeout): - while True: + while not m.is_killed(): # check if we found a way to break more than MAXFAIL properties broken_properties = sum(int(len(x) != 0) for x in properties.values()) if broken_properties >= MAXFAIL: @@ -211,7 +211,7 @@ def manticore_verifier( # check if we sent more than MAXTX transaction if tx_num >= MAXTX: - print("Max numbr of transactions reached({tx_num})") + print(f"Max number of transactions reached ({tx_num})") break tx_num += 1 @@ -219,7 +219,7 @@ def manticore_verifier( new_coverage = m.global_coverage(contract_account) if new_coverage >= MAXCOV: print( - "Current coverage({new_coverage}%) is greater than max allowed({MAXCOV}%).Stopping exploration." + f"Current coverage({new_coverage}%) is greater than max allowed ({MAXCOV}%). Stopping exploration." ) break @@ -229,7 +229,7 @@ def manticore_verifier( break current_coverage = new_coverage - # check if timeout was requested + # Make sure we didn't time out before starting first transaction if m.is_killed(): print("Cancelled or timeout.") break @@ -256,6 +256,11 @@ def manticore_verifier( data=symbolic_data, ) + # check if timeout was requested during the previous transaction + if m.is_killed(): + print("Cancelled or timeout.") + break + m.clear_terminated_states() # no interest in reverted states m.take_snapshot() # make a copy of all ready states print( @@ -264,6 +269,11 @@ def manticore_verifier( f"Failing properties: {broken_properties}/{len(properties)}" ) + # check if timeout was requested while we were taking the snapshot + if m.is_killed(): + print("Cancelled or timeout.") + break + # And now explore all properties (and only the properties) filter_no_crytic.disable() # Allow crytic_porperties filter_out_human_constants.disable() # Allow them to be marked as constants @@ -315,6 +325,8 @@ def manticore_verifier( m.clear_terminated_states() # no interest in reverted states for now! m.goto_snapshot() + else: + print("Cancelled or timeout.") m.clear_terminated_states() m.clear_ready_states() @@ -410,7 +422,10 @@ def main(): "--psender", type=str, help="(optional) address from where the property is tested" ) eth_flags.add_argument( - "--propre", type=str, help="A regular expression for selecting properties" + "--propre", + default=r"crytic_.*", + type=str, + help="A regular expression for selecting properties", ) eth_flags.add_argument( "--timeout", default=240, type=int, help="Exploration timeout in seconds" @@ -484,4 +499,5 @@ def main(): deployer=deployer, psender=psender, timeout=args.timeout, + propre=args.propre, ) diff --git a/manticore/native/models.py b/manticore/native/models.py index 6f5a67407..cc9c76dcb 100644 --- a/manticore/native/models.py +++ b/manticore/native/models.py @@ -199,6 +199,7 @@ def strlen_approx(state: State, s: Union[int, BitVec]) -> Union[int, BitVec]: Strategy: build a result tree to limit state explosion results approximate Algorithm: Walks from end of string not including NULL building ITE tree when current byte is symbolic. + :param state: current program state :param s: Address of string :return: Symbolic strlen result @@ -268,3 +269,59 @@ def strcpy(state: State, dst: Union[int, BitVec], src: Union[int, BitVec]) -> Un if "strcpy" in state.context: del state.context["strcpy"] return ret + + +def strncpy( + state: State, dst: Union[int, BitVec], src: Union[int, BitVec], n: Union[int, BitVec] +) -> Union[int, BitVec]: + """ + strncpy symbolic model + + Algorithm: Copy n bytes from src to dst. If the length of the src string is less than n pad the difference + with NULL bytes. If a symbolic byte is found that can be NULL but is not definitely NULL fork and concretize states. + + :param state: current program state + :param dst: destination string address + :param src: source string address + :param n: number of bytes to copy + :return: pointer to the dst + """ + + if issymbolic(dst): + raise ConcretizeArgument(state.cpu, 1) + if issymbolic(src): + raise ConcretizeArgument(state.cpu, 2) + if issymbolic(n): + raise ConcretizeArgument(state.cpu, 3) + + cpu = state.cpu + constrs = state.constraints + ret = dst + + # Initialize offset based on whether state has been forked in strncpy + if "strncpy" not in state.context: + offset = 0 + else: + offset = state.context["strncpy"] + + # Copy until a src_byte is symbolic and constrained to '\000', or is concrete and '\000' + src_val = cpu.read_int(src + offset, 8) + while offset < n and not is_definitely_NULL(src_val, constrs): + cpu.write_int(dst + offset, src_val, 8) + + # If a src byte can be NULL concretize and fork states + if can_be_NULL(src_val, constrs): + state.context["strncpy"] = offset + raise Concretize("Forking on NULL strncpy", expression=(src_val == 0), policy="ALL") + offset += 1 + + src_val = cpu.read_int(src + offset, 8) + + # Pad the distance between length of src and n with NULL bytes + while offset < n: + cpu.write_int(dst + offset, 0, 8) + offset += 1 + + if "strncpy" in state.context: + del state.context["strncpy"] + return ret diff --git a/scripts/run_tests.sh b/scripts/run_tests.sh index 97b71452f..03aed07bb 100755 --- a/scripts/run_tests.sh +++ b/scripts/run_tests.sh @@ -116,7 +116,9 @@ run_tests_from_dir() { COVERAGE_RCFILE=$GITHUB_WORKSPACE/.coveragerc echo "Running only the tests from 'tests/$DIR' directory" pytest --durations=100 --cov=manticore --cov-config=$GITHUB_WORKSPACE/.coveragerc -n auto "tests/$DIR" + RESULT=$? coverage xml + return $RESULT } run_examples() { diff --git a/tests/ethereum/test_general.py b/tests/ethereum/test_general.py index c09331a76..0aa4bee35 100644 --- a/tests/ethereum/test_general.py +++ b/tests/ethereum/test_general.py @@ -72,7 +72,6 @@ def test_int_ovf(self): class EthVerifierIntegrationTest(unittest.TestCase): def test_propverif(self): smtcfg = config.get_group("smt") - smtcfg.solver = smtcfg.solver.yices with smtcfg.temp_vals(): smtcfg.solver = smtcfg.solver.yices diff --git a/tests/native/binaries/sym_strcpy_test b/tests/native/binaries/str_model_tests/sym_strcpy_test similarity index 100% rename from tests/native/binaries/sym_strcpy_test rename to tests/native/binaries/str_model_tests/sym_strcpy_test diff --git a/tests/native/binaries/sym_strcpy_test.c b/tests/native/binaries/str_model_tests/sym_strcpy_test.c similarity index 100% rename from tests/native/binaries/sym_strcpy_test.c rename to tests/native/binaries/str_model_tests/sym_strcpy_test.c diff --git a/tests/native/binaries/sym_strlen_test b/tests/native/binaries/str_model_tests/sym_strlen_test similarity index 100% rename from tests/native/binaries/sym_strlen_test rename to tests/native/binaries/str_model_tests/sym_strlen_test diff --git a/tests/native/binaries/sym_strlen_test.c b/tests/native/binaries/str_model_tests/sym_strlen_test.c similarity index 100% rename from tests/native/binaries/sym_strlen_test.c rename to tests/native/binaries/str_model_tests/sym_strlen_test.c diff --git a/tests/native/binaries/str_model_tests/sym_strncpy_test b/tests/native/binaries/str_model_tests/sym_strncpy_test new file mode 100755 index 000000000..ad8a35f5f Binary files /dev/null and b/tests/native/binaries/str_model_tests/sym_strncpy_test differ diff --git a/tests/native/binaries/str_model_tests/sym_strncpy_test.c b/tests/native/binaries/str_model_tests/sym_strncpy_test.c new file mode 100644 index 000000000..09d5dab51 --- /dev/null +++ b/tests/native/binaries/str_model_tests/sym_strncpy_test.c @@ -0,0 +1,14 @@ +#include +#include +#include +#include +#define LEN 5 + +int main() { + char src[LEN]; + char dst[LEN]; + read(0, src, LEN); + + strncpy(dst, src, LEN - 2); + return 0; +} diff --git a/tests/native/test_models.py b/tests/native/test_models.py index ae718c7f7..a3e5f498c 100644 --- a/tests/native/test_models.py +++ b/tests/native/test_models.py @@ -23,6 +23,7 @@ strlen_exact, strlen_approx, strcpy, + strncpy, is_definitely_NULL, cannot_be_NULL, ) @@ -226,7 +227,9 @@ def test_symbolic_no_fork(self): def test_symbolic_fork(self): # This binary is compiled using gcc (Ubuntu 7.5.0-3ubuntu1~18.04) 7.5.0 # with flags: -g -static -fno-builtin - BIN_PATH = os.path.join(os.path.dirname(__file__), "binaries", "sym_strlen_test") + BIN_PATH = os.path.join( + os.path.dirname(__file__), "binaries/str_model_tests", "sym_strlen_test" + ) tmp_dir = tempfile.TemporaryDirectory(prefix="mcore_test_sym_") m = Manticore(BIN_PATH, stdin_size=10, workspace_url=str(tmp_dir.name)) @@ -294,7 +297,6 @@ def _assert_concrete(self, s, d): dst = cpu.read_int(d, 8) offset = 0 while cannot_be_NULL(src, self.state.constraints): - self.assertTrue(not issymbolic(dst)) self.assertEqual(src, dst) offset += 1 src = cpu.read_int(s + offset, 8) @@ -303,7 +305,6 @@ def _assert_concrete(self, s, d): # Assert final NULL byte self.assertTrue(is_definitely_NULL(src, self.state.constraints)) self.assertEqual(0, dst) - return offset def _test_strcpy(self, string, dst_len=None): """ @@ -312,7 +313,7 @@ def _test_strcpy(self, string, dst_len=None): to dst until the NULL byte, and asserts the memory address returned by strcpy is equal to the given dst address. """ - # Create src and dsty strings + # Create src and dst strings if dst_len is None: dst_len = len(string) cpu = self.state.cpu @@ -330,7 +331,7 @@ def _test_strcpy(self, string, dst_len=None): # addresses should match self.assertEqual(ret, d) # assert everything is copied up to the 1st possible 0 is copied - offset = self._assert_concrete(s, d) + self._assert_concrete(s, d) # Delete stack space created self._pop_string_space(dst_len + len(string)) @@ -348,14 +349,16 @@ def test_concrete_empty(self): def test_symbolic(self): # This binary is compiled using gcc (Ubuntu 7.5.0-3ubuntu1~18.04) 7.5.0 # with flags: -g -static -fno-builtin - BIN_PATH = os.path.join(os.path.dirname(__file__), "binaries", "sym_strcpy_test") + BIN_PATH = os.path.join( + os.path.dirname(__file__), "binaries/str_model_tests", "sym_strcpy_test" + ) tmp_dir = tempfile.TemporaryDirectory(prefix="mcore_test_sym_") m = Manticore(BIN_PATH, stdin_size=10, workspace_url=str(tmp_dir.name)) addr_of_strcpy = 0x400418 @m.hook(addr_of_strcpy) - def strlen_model(state): + def strcpy_model(state): state.invoke_model(strcpy) m.run() @@ -406,3 +409,120 @@ def strlen_model(state): match = True break self.assertTrue(match) + + +class StrncpyTest(ModelTest): + def _assert_concrete(self, s, d, n): + # Checks that n characters are copied until a NULL in the src + # and that NULL is written for the distance between src and NULL + cpu = self.state.cpu + src = cpu.read_int(s, 8) + dst = cpu.read_int(d, 8) + offset = 0 + + # Check that min(n, length of src) characters are copied from src to dst + while not is_definitely_NULL(src, self.state.constraints) and offset < n: + self.assertEqual(src, dst) + offset += 1 + src = cpu.read_int(s + offset, 8) + dst = cpu.read_int(d + offset, 8) + + # Check that N - length of src characters are NULL padded + while offset < n: + self.assertEqual(0, dst) + offset += 1 + dst = cpu.read_int(d + offset, 8) + + def _test_strncpy(self, string, n): + """ + This method creates memory for a given src (with no possible NULL bytes but and a + final NULL byte) and dst string pointers, asserts that everything is copied from src + to dst until the NULL byte, and asserts the memory address returned by strcpy is + equal to the given dst address. + """ + dst_len = n + 1 + cpu = self.state.cpu + s = self._push_string(string) + d = self._push_string_space(dst_len) + dst_vals = [None] * dst_len + for i in range(dst_len): + # Set each dst byte to a random char to simplify equal comparisons + c = random.randrange(1, 255) + cpu.write_int(d + i, c, 8) + dst_vals[i] = c + + ret = strncpy(self.state, d, s, n) + + # addresses should match + self.assertEqual(ret, d) + # assert everything is copied up to the 1st possible 0 is copied + self._assert_concrete(s, d, n) + + # Delete stack space created + self._pop_string_space(dst_len + len(string)) + + def test_concrete(self): + self._test_strncpy("abc\0", n=4) + self._test_strncpy("abcdefghijklm\0", n=20) + self._test_strncpy("a\0", n=10) + + def test_small_n(self): + self._test_strncpy("a\0", n=1) + self._test_strncpy("abcdefghijklm\0", n=0) + + def test_concrete_empty(self): + self._test_strncpy("\0", n=1) + self._test_strncpy("\0", n=10) + + def test_symbolic(self): + # Create src and dst strings + # This binary is compiled using gcc (Ubuntu 7.5.0-3ubuntu1~18.04) 7.5.0 + # with flags: -g -static -fno-builtin + BIN_PATH = os.path.join( + os.path.dirname(__file__), "binaries/str_model_tests", "sym_strncpy_test" + ) + tmp_dir = tempfile.TemporaryDirectory(prefix="mcore_test_sym_") + m = Manticore(BIN_PATH, stdin_size=10, workspace_url=str(tmp_dir.name)) + + addr_of_strncpy = 0x0400490 + + @m.hook(addr_of_strncpy) + def strncpy_model(state): + state.invoke_model(strncpy) + + m.run() + m.finalize() + + # Approximate regexes for expected testcase output + # Example Match above each regex + # Manticore varies the hex output slightly per run + expected = [ + # STDIN: b'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00' + r"STDIN: b\'\\x00(\\x([0-9a-f]{2})){9}\'", + # STDIN: b'\xff\x00\xff\xff\xff\xff\xff\xff\xff\xff' + r"STDIN: b\'(\\x((?!(00))([0-9a-f]{2}))){1}\\x00(\\x([0-9a-f]{2})){8}\'", + # STDIN: b'\xff\xff\x00\xff\xff\xff\xff\xff\xff\xff' + r"STDIN: b\'(\\x((?!(00))([0-9a-f]{2}))){2}\\x00(\\x([0-9a-f]{2})){7}\'", + # STDIN: b'\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff' + r"STDIN: b\'(\\x((?!(00))([0-9a-f]{2}))){10}\'", + ] + + inputs = f"{str(m.workspace)}/test_*.input" + + # Make a list of the generated input states + stdins = [] + for inpt in glob(inputs): + with open(inpt) as f: + stdins.append(f.read()) + + # Check the number of input states matches the number of regexes + self.assertEqual(len(stdins), len(expected)) + + # Assert that every regex has a matching input + for e in expected: + match = False + for s in stdins: + if re.fullmatch(e, s) == None: + match = True + break + self.assertTrue(match)