Symbolic model for strcpy

manticore/core/smtlib/expression.py

@@ -1263,6 +1263,18 @@ def __init__(
         assert false_value.size == size
         super().__init__(size, condition, true_value, false_value, *args, **kwargs)
 
+    @property
+    def condition(self):
+        return self.operands[0]
+
+    @property
+    def true_value(self):
+        return self.operands[1]
+
+    @property
+    def false_value(self):
+        return self.operands[2]
+
 
 Constant = (BitVecConstant, BoolConstant)
 Variable = (BitVecVariable, BoolVariable, ArrayVariable)

manticore/native/models.py

@@ -2,10 +2,12 @@
 Models here are intended to be passed to :meth:`~manticore.native.state.State.invoke_model`, not invoked directly.
 """
 
-from .cpu.abstractcpu import ConcretizeArgument
-from ..core.smtlib import issymbolic
+from .cpu.abstractcpu import Cpu, ConcretizeArgument
+from .state import State
+from ..core.smtlib import issymbolic, BitVec
 from ..core.smtlib.solver import Z3Solver
 from ..core.smtlib.operators import ITEBV, ZEXTEND
+from typing import Union, List
 
 VARIADIC_FUNC_ATTR = "_variadic"
 
@@ -57,7 +59,7 @@ def _find_zero(cpu, constrs, ptr):
     return offset
 
 
-def strcmp(state, s1, s2):
+def strcmp(state: State, s1: Union[int, BitVec], s2: Union[int, BitVec]):
     """
     strcmp symbolic model.
 
@@ -113,7 +115,7 @@ def strcmp(state, s1, s2):
     return ret
 
 
-def strlen(state, s):
+def strlen(state: State, s: Union[int, BitVec]):
     """
     strlen symbolic model.
 
@@ -140,3 +142,123 @@ def strlen(state, s):
             ret = ITEBV(cpu.address_bit_size, byt == 0, offset, ret)
 
     return ret
+
+
+def is_NULL(byte, constrs) -> bool:
+    """
+    Checks if a given byte read from memory is NULL or effectively NULL
+
+    :param byte: byte read from memory to be examined
+    :param constrs: state constraints
+    :return: whether a given byte is NULL or constrained to NULL
+    """
+    if issymbolic(byte):
+        return not Z3Solver.instance().can_be_true(constrs, byte != 0)
+    else:
+        return byte == 0
+
+
+def cant_be_NULL(byte, constrs) -> bool:
+    """
+    Checks if a given byte read from memory is not NULL or cannot be NULL
+
+    :param byte: byte read from memory to be examined
+    :param constrs: state constraints
+    :return: whether a given byte is not NULL or cannot be NULL
+    """
+    if issymbolic(byte):
+        return not Z3Solver.instance().can_be_true(constrs, byte == 0)
+    else:
+        return byte != 0
+
+
+def can_be_NULL(byte, constrs) -> bool:
+    """
+    Checks if a given byte read from memory can be NULL
+
+    :param byte: byte read from memory to be examined
+    :param constrs: state constraints
+    :return: whether a given byte is NULL or can be NULL
+    """
+    if issymbolic(byte):
+        return Z3Solver.instance().can_be_true(constrs, byte == 0)
+    else:
+        return byte == 0
+
+
+def strcpy(state: State, dst: Union[int, BitVec], src: Union[int, BitVec]) -> Union[int, BitVec]:
+    """
+    strcpy symbolic model
+
+    Algorithm: Copy every byte from the src to dst until finding a byte that can be or is NULL.
+    If the byte is NULL or is constrained to only the NULL value, append the NULL value to dst
+    and return. If the value can be NULL or another value write an `Expression` for every following
+    byte that sets a value to the src or dst byte according to the preceding bytes until a NULL
+    byte or effectively NULL byte is found.
+
+    :param state: current program state
+    :param dst: destination string address
+    :param src: source string address
+    :return: pointer to the dst
+    """
+    if issymbolic(src):
+        raise ConcretizeArgument(state.cpu, 1)
+
+    if issymbolic(dst):
+        raise ConcretizeArgument(state.cpu, 2)
+
+    cpu = state.cpu
+    constrs = state.constraints
+    ret = dst
+
+    # Copy until '\000' is reached or symbolic memory that can be '\000'
+    c = cpu.read_int(src, 8)
+    while cant_be_NULL(c, constrs):
+        cpu.write_int(dst, c, 8)
+        src += 1
+        dst += 1
+        c = cpu.read_int(src, 8)
+
+    # If the byte is symbolic and constrained to '\000' or is '\000' write concrete val and return
+    if is_NULL(c, constrs):
+        cpu.write_int(dst, 0, 8)
+        return ret
+
+    offset = 0
+    zeros: List[int] = []
+    src_val = cpu.read_int(src, 8)
+    while not is_NULL(src_val, constrs):
+        if can_be_NULL(c, constrs):
+            # If a byte can be NULL set the src_val for NULL, build the ITE, & add to the list of nulls
+            src_val = ITEBV(8, src_val != 0, src_val, 0)
+            _build_ITE(zeros, cpu, src, dst, offset, src_val)
+            zeros.append(offset)
+        else:
+            # If it can't be NULL just build the ITE
+            _build_ITE(zeros, cpu, src, dst, offset, src_val)
+        offset += 1
+        src_val = cpu.read_int(src + offset, 8)
+
+    # Build ITE Tree for NULL byte
+    src_val = 0
+    _build_ITE(zeros, cpu, src, dst, offset, src_val)
+
+    return ret
+
+
+def _build_ITE(
+    zeros: List[int],
+    cpu: Cpu,
+    src: Union[int, BitVec],
+    dst: Union[int, BitVec],
+    offset: int,
+    src_val: Union[int, BitVec],
+) -> None:
+    """
+    Builds ITE tree for each symbolic dst byte
+    """
+    dst_val = cpu.read_int(dst + offset, 8)
+    for zero in reversed(zeros):
+        c = cpu.read_int(src + zero, 8)
+        src_val = ITEBV(8, c != 0, src_val, dst_val)
+    cpu.write_int(dst + offset, src_val, 8)

tests/native/test_models.py

@@ -1,11 +1,28 @@
 import unittest
 import os
-
-from manticore.core.smtlib import ConstraintSet, Z3Solver
+import random
+
+from manticore.core.smtlib import (
+    ConstraintSet,
+    Operators,
+    Z3Solver,
+    issymbolic,
+    ArraySelect,
+    BitVecITE,
+)
 from manticore.native.state import State
 from manticore.platforms import linux
 
-from manticore.native.models import variadic, isvariadic, strcmp, strlen
+from manticore.native.models import (
+    variadic,
+    isvariadic,
+    strcmp,
+    strlen,
+    strcpy,
+    is_NULL,
+    can_be_NULL,
+    cant_be_NULL,
+)
 
 
 class ModelMiscTest(unittest.TestCase):
@@ -43,6 +60,16 @@ def _push_string(self, s):
         cpu.write_bytes(cpu.RSP, s)
         return cpu.RSP
 
+    def _push_string_space(self, l):
+        cpu = self.state.cpu
+        cpu.RSP -= l
+        return cpu.RSP
+
+    def _pop_string_space(self, l):
+        cpu = self.state.cpu
+        cpu.RSP += l
+        return cpu.RSP
+
     def assertItemsEqual(self, a, b):
         # Required for Python3 compatibility
         self.assertEqual(sorted(a), sorted(b))
@@ -198,3 +225,125 @@ def test_symbolic_mixed(self):
         self.state.constrain(sy[3] != 0)
         ret = strlen(self.state, s)
         self.assertTrue(self.state.must_be_true(ret == 4))
+
+
+class StrcpyTest(ModelTest):
+    def _check_BitVecITE(self, dst, dst_val):
+        # Iterate and check the nested ITE tree for a symbolic byte
+        self.assertTrue(issymbolic(dst))
+        while type(dst.true_value) is BitVecITE:  # check each if/else in dst
+            self.assertEqual(dst.false_value, dst_val)  # dst = false_val
+            dst = dst.true_value
+        return dst
+
+    def _assert_start(self, s, d):
+        # Checks all characters are copied until the 1st that could be NULL
+        cpu = self.state.cpu
+        src = cpu.read_int(s, 8)
+        dst = cpu.read_int(d, 8)
+        offset = 0
+        while cant_be_NULL(src, self.state.constraints):
+            self.assertTrue(not issymbolic(dst))
+            self.assertEqual(src, dst)
+            offset += 1
+            src = cpu.read_int(s + offset, 8)
+            dst = cpu.read_int(d + offset, 8)
+        return offset
+
+    def _assert_end(self, s, d, offset, org_dest_val):
+        cpu = self.state.cpu
+        src = cpu.read_int(s + offset, 8)
+        dst = cpu.read_int(d + offset, 8)
+
+        # src string was entirely symbolic
+        if not issymbolic(dst):
+            self.assertTrue(is_NULL(src, self.state.constraints))
+            self.assertEqual(0, dst)
+
+        # Check each symbolic byte in the dst
+        else:
+            # Loop till src must be NULL or assumed dst space allowed is gone
+            while not is_NULL(src, self.state.constraints) and offset < len(org_dest_val):
+                # Check ITE tree in symbolic dst
+                dst = self._check_BitVecITE(dst, org_dest_val[offset])
+
+                # Check that true value is src
+                if type(dst.true_value) is ArraySelect:
+                    self.assertEqual(type(src), ArraySelect)
+                    self.assertEqual(src.index, dst.true_value.index)
+                    self.assertTrue(src.array is dst.true_value.array)
+                else:
+                    self.assertTrue(Operators.ITE(dst.true_value == src, True, False))
+
+                # Check the false value is dst or offset
+                if issymbolic(src) and can_be_NULL(src, self.state.constraints):
+                    self.assertEqual(dst.false_value, 0)
+                else:
+                    self.assertEqual(dst.false_value, org_dest_val[offset])  # dst = false_val
+
+                offset += 1
+                src = cpu.read_int(s + offset, 8)
+                dst = cpu.read_int(d + offset, 8)
+
+            # Check last sym dst byte
+            dst = self._check_BitVecITE(dst, org_dest_val[offset])
+            self.assertEqual(dst.true_value, 0)
+
+    def _test_strcpy(self, string, dst_len=None):
+        # Create src and dsty strings
+        if dst_len is None:
+            dst_len = len(string)
+        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 compairisons
+            c = random.randrange(255)
+            cpu.write_int(d + i, c, 8)
+            dst_vals[i] = c
+
+        ret = strcpy(self.state, d, s)
+
+        # addresses should match
+        self.assertEqual(ret, d)
+        # assert everything is copied up to the 1st possible 0 is copied
+        offset = self._assert_start(s, d)
+        # check all symbolic values created until a value that must be 0 is found
+        self._assert_end(s, d, offset, dst_vals)
+
+        # Delete stack space created
+        self._pop_string_space(dst_len + len(string))
+
+    def test_concrete(self):
+        self._test_strcpy("abc\0")
+        self._test_strcpy("a\0", dst_len=10)
+        self._test_strcpy("abcdefghijklm\0")
+        self._test_strcpy("a\0", dst_len=5)
+
+    def test_concrete_empty(self):
+        self._test_strcpy("\0")
+        self._test_strcpy("\0", dst_len=10)
+
+    def test_symbolic_mixed(self):
+        src = self.state.symbolicate_buffer("++\0")
+        self._test_strcpy(src, dst_len=4)
+
+        src = self.state.symbolicate_buffer("xy++\0")
+        self._test_strcpy(src, dst_len=6)
+
+        src = self.state.symbolicate_buffer("iv+++")
+        self.state.constraints.add(src[-1] == 0)
+        self._test_strcpy(src, dst_len=6)
+
+        src = self.state.symbolicate_buffer("+++jl\0")
+        self._test_strcpy(src, dst_len=6)
+
+        src = self.state.symbolicate_buffer("+++df+++")
+        self.state.constraints.add(src[-1] == 0)
+        self._test_strcpy(src, dst_len=12)
+
+    def test_only_symbolic(self):
+        src = self.state.symbolicate_buffer("++++++++++++")
+        self.state.constraints.add(src[-1] == 0)
+        self._test_strcpy(src, dst_len=15)