Create a model for strncpy (#1770)

* Add strncpy model

* Forgot to remove an edit

* Adding model tests

* Added strncpy c file and created a directory for all string modeling binaries

* Update to argument ordering in manticore/native/models.py

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

* Removed dead code

Co-authored-by: Eric Kilmer <eric.d.kilmer@gmail.com>

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

tests/native/binaries/str_model_tests/sym_strncpy_test.c

@@ -0,0 +1,14 @@
+#include <stdio.h>
+#include <string.h>
+#include <stdlib.h>
+#include <unistd.h>
+#define LEN 5
+
+int main() {
+	char src[LEN];
+	char dst[LEN];
+	read(0, src, LEN);
+
+	strncpy(dst, src, LEN - 2);
+	return 0;	
+}

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)