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/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)