mirror of
https://github.com/angr/angr
synced 2026-08-17 12:23:11 -04:00
f939c5b88c
* Enable ruff isort rule * [pre-commit.ci] auto fixes from pre-commit.com hooks for more information, see https://pre-commit.ci --------- Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com>
1106 lines
44 KiB
Python
Executable file
1106 lines
44 KiB
Python
Executable file
#!/usr/bin/env python3
|
|
# pylint: disable=missing-class-docstring,no-self-use,line-too-long
|
|
from __future__ import annotations
|
|
|
|
__package__ = __package__ or "tests.procedures.libc" # pylint:disable=redefined-builtin
|
|
|
|
import logging
|
|
import random
|
|
import unittest
|
|
from itertools import combinations
|
|
|
|
import claripy
|
|
|
|
import angr
|
|
from angr import SIM_LIBRARIES, SimState
|
|
from tests.common import broken
|
|
|
|
log = logging.getLogger("angr.tests.string")
|
|
|
|
|
|
def make_state_with_stdin(content):
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
stdin_storage = angr.storage.file.SimFile("stdin", content=content)
|
|
stdin = angr.storage.file.SimFileDescriptor(stdin_storage)
|
|
s.register_plugin("posix", angr.state_plugins.SimSystemPosix(stdin=stdin_storage, fd={0: stdin}))
|
|
return s
|
|
|
|
|
|
def make_func(name):
|
|
return lambda state, arguments: (
|
|
SIM_LIBRARIES["libc.so.6"][0].get(name, "AMD64").execute(state, arguments=arguments).ret_expr
|
|
)
|
|
|
|
|
|
strstr = make_func("strstr")
|
|
strtok_r = make_func("strtok_r")
|
|
strcmp = make_func("strcmp")
|
|
strchr = make_func("strchr")
|
|
strncmp = make_func("strncmp")
|
|
strlen = make_func("strlen")
|
|
strncpy = make_func("strncpy")
|
|
strcpy = make_func("strcpy")
|
|
memset = make_func("memset")
|
|
memcpy = make_func("memcpy")
|
|
memcmp = make_func("memcmp")
|
|
sprintf = make_func("sprintf")
|
|
getc = make_func("_IO_getc")
|
|
fgetc = make_func("fgetc")
|
|
getchar = make_func("getchar")
|
|
scanf = make_func("scanf")
|
|
wcscmp = make_func("wcscmp")
|
|
|
|
|
|
class TestStringSimProcedures(unittest.TestCase):
|
|
def test_strlen(self):
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
|
|
log.info("fully concrete string")
|
|
a_str = claripy.BVV(0x41414100, 32)
|
|
a_addr = claripy.BVV(0x10, 64)
|
|
s.memory.store(a_addr, a_str, endness="Iend_BE")
|
|
a_len = strlen(s, arguments=[a_addr])
|
|
assert s.solver.unique(a_len)
|
|
assert s.solver.eval(a_len) == 3
|
|
|
|
log.info("concrete-terminated string")
|
|
b_str = claripy.Concat(claripy.BVS("mystring", 24), claripy.BVV(0, 8))
|
|
b_addr = claripy.BVV(0x20, 64)
|
|
s.memory.store(b_addr, b_str, endness="Iend_BE")
|
|
b_len = strlen(s, arguments=[b_addr])
|
|
assert s.solver.max_int(b_len) == 3
|
|
assert tuple(sorted(s.solver.eval_upto(b_len, 10))) == (0, 1, 2, 3)
|
|
|
|
log.info("fully unconstrained")
|
|
u_addr = claripy.BVV(0x50, 64)
|
|
u_len_sp = strlen(s, arguments=[u_addr])
|
|
u_len = u_len_sp
|
|
assert len(s.solver.eval_upto(u_len, 100)) == s.libc.buf_symbolic_bytes
|
|
assert s.solver.max_int(u_len) == s.libc.buf_symbolic_bytes - 1
|
|
# print u_len_sp.solver.maximum_null
|
|
|
|
# s.add_constraints(u_len < 16)
|
|
|
|
assert s.solver.eval_upto(s.memory.load(0x50 + u_len, 1), 300) == [0]
|
|
#
|
|
# This tests if a strlen can influence a symbolic str.
|
|
#
|
|
log.info("Trying to influence length.")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_c = claripy.BVS("some_string", 8 * 16)
|
|
c_addr = claripy.BVV(0x10, 64)
|
|
s.memory.store(c_addr, str_c, endness="Iend_BE")
|
|
c_len = strlen(s, arguments=[c_addr])
|
|
assert len(s.solver.eval_upto(c_len, 100)) == s.libc.buf_symbolic_bytes
|
|
assert s.solver.max_int(c_len) == s.libc.buf_symbolic_bytes - 1
|
|
|
|
one_s = s.copy()
|
|
one_s.add_constraints(c_len == 1)
|
|
assert one_s.solver.eval(str_c, cast_to=bytes).index(b"\x00") == 1
|
|
str_test = one_s.memory.load(c_addr, 2, endness="Iend_BE")
|
|
assert len(one_s.solver.eval_upto(str_test, 300, cast_to=bytes)) == 255
|
|
|
|
for i in range(16):
|
|
test_s = s.copy()
|
|
test_s.add_constraints(c_len == i)
|
|
str_test = test_s.memory.load(c_addr, i + 1, endness="Iend_BE")
|
|
assert test_s.solver.eval(str_test, cast_to=bytes).index(b"\x00") == i
|
|
for j in range(i):
|
|
assert not test_s.solver.unique(test_s.memory.load(c_addr + j, 1))
|
|
|
|
def test_strcmp(self):
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_a = claripy.BVV(0x41414100, 32)
|
|
str_b = claripy.BVS("mystring", 32)
|
|
|
|
a_addr = claripy.BVV(0x10, 64)
|
|
b_addr = claripy.BVV(0xB0, 64)
|
|
|
|
s.memory.store(a_addr, str_a, endness="Iend_BE")
|
|
s.memory.store(b_addr, str_b, endness="Iend_BE")
|
|
|
|
s_cmp = s.copy()
|
|
cmpres = strcmp(s_cmp, arguments=[a_addr, b_addr])
|
|
s_match = s_cmp.copy()
|
|
s_nomatch = s_cmp.copy()
|
|
s_match.add_constraints(cmpres == 0)
|
|
s_nomatch.add_constraints(cmpres != 0)
|
|
|
|
assert s_match.solver.unique(str_b)
|
|
assert not s_nomatch.solver.unique(str_b)
|
|
assert s_match.solver.eval(str_b, cast_to=bytes) == b"AAA\x00"
|
|
|
|
s_ncmp = s.copy()
|
|
ncmpres = strncmp(s_ncmp, arguments=[a_addr, b_addr, claripy.BVV(2, s.arch.bits)])
|
|
s_match = s_ncmp.copy()
|
|
s_nomatch = s_ncmp.copy()
|
|
s_match.add_constraints(ncmpres == 0)
|
|
s_nomatch.add_constraints(ncmpres != 0)
|
|
|
|
assert not s_match.solver.unique(str_b)
|
|
assert s_match.solver.unique(s_match.memory.load(b_addr, 2))
|
|
assert len(s_match.solver.eval_upto(s_match.memory.load(b_addr, 3), 300)) == 256
|
|
assert not s_nomatch.solver.unique(str_b)
|
|
|
|
log.info("concrete a, symbolic b")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_a = claripy.BVV(0x41424300, 32)
|
|
str_b = claripy.BVS("mystring", 32)
|
|
a_addr = claripy.BVV(0x10, 64)
|
|
b_addr = claripy.BVV(0xB0, 64)
|
|
s.memory.store(a_addr, str_a, endness="Iend_BE")
|
|
s.memory.store(b_addr, str_b, endness="Iend_BE")
|
|
|
|
s_cmp = s.copy()
|
|
cmpres = strncmp(s_cmp, arguments=[a_addr, b_addr, claripy.BVV(2, s_cmp.arch.bits)])
|
|
s_match = s_cmp.copy()
|
|
s_nomatch = s_cmp.copy()
|
|
s_match.add_constraints(cmpres == 0)
|
|
s_nomatch.add_constraints(cmpres != 0)
|
|
|
|
assert s_match.solver.solution(str_b, 0x41420000)
|
|
assert s_match.solver.solution(str_b, 0x41421234)
|
|
assert s_match.solver.solution(str_b, 0x41424300)
|
|
assert not s_nomatch.solver.solution(str_b, 0x41420000)
|
|
assert not s_nomatch.solver.solution(str_b, 0x41421234)
|
|
assert not s_nomatch.solver.solution(str_b, 0x41424300)
|
|
|
|
log.info("symbolic a, symbolic b")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
a_addr = claripy.BVV(0x10, 64)
|
|
b_addr = claripy.BVV(0xB0, 64)
|
|
|
|
s_cmp = s.copy()
|
|
cmpres = strcmp(s_cmp, arguments=[a_addr, b_addr])
|
|
s_match = s_cmp.copy()
|
|
s_nomatch = s_cmp.copy()
|
|
s_match.add_constraints(cmpres == 0)
|
|
s_nomatch.add_constraints(cmpres != 0)
|
|
|
|
m_res = strcmp(s_match, arguments=[a_addr, b_addr])
|
|
s_match.add_constraints(m_res != 0)
|
|
nm_res = strcmp(s_nomatch, arguments=[a_addr, b_addr])
|
|
s_nomatch.add_constraints(nm_res == 0)
|
|
|
|
assert not s_match.satisfiable()
|
|
assert not s_match.satisfiable()
|
|
|
|
def test_strncmp(self):
|
|
log.info("symbolic left, symbolic right, symbolic len")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
left = claripy.BVS("left", 32)
|
|
left_addr = claripy.BVV(0x1000, 64)
|
|
right = claripy.BVS("right", 32)
|
|
right_addr = claripy.BVV(0x2000, 64)
|
|
maxlen = claripy.BVS("len", 64)
|
|
|
|
s.memory.store(left_addr, left)
|
|
s.memory.store(right_addr, right)
|
|
|
|
s.add_constraints(strlen(s, arguments=[left_addr]) == 3)
|
|
s.add_constraints(strlen(s, arguments=[right_addr]) == 0)
|
|
|
|
s.add_constraints(maxlen != 0)
|
|
c = strncmp(s, arguments=[left_addr, right_addr, maxlen])
|
|
|
|
s_match = s.copy()
|
|
s_match.add_constraints(c == 0)
|
|
assert not s_match.satisfiable()
|
|
# assert s_match.solver.min_int(maxlen) == 3
|
|
|
|
s_nomatch = s.copy()
|
|
s_nomatch.add_constraints(c != 0)
|
|
assert s_nomatch.satisfiable()
|
|
# assert s_nomatch.solver.max_int(maxlen) == 2
|
|
|
|
log.info("zero-length")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
left = claripy.BVS("left", 32)
|
|
left_addr = claripy.BVV(0x1000, 64)
|
|
right = claripy.BVS("right", 32)
|
|
right_addr = claripy.BVV(0x2000, 64)
|
|
maxlen = claripy.BVS("len", 64)
|
|
left_len = strlen(s, arguments=[left_addr])
|
|
right_len = strlen(s, arguments=[right_addr])
|
|
c = strncmp(s, arguments=[left_addr, right_addr, maxlen])
|
|
|
|
s.add_constraints(right_len == 0)
|
|
s.add_constraints(left_len == 0)
|
|
# s.add_constraints(c == 0)
|
|
s.add_constraints(maxlen == 0)
|
|
assert s.satisfiable()
|
|
|
|
def test_strncmp_longer_limit(self):
|
|
log.info("concrete a, concrete b, concrete n")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_a = claripy.BVV(b"ABC\0")
|
|
str_b = claripy.BVV(b"AB\0")
|
|
addr_a = claripy.BVV(0x10, 64)
|
|
addr_b = claripy.BVV(0xB0, 64)
|
|
s.memory.store(addr_a, str_a, endness="Iend_BE")
|
|
s.memory.store(addr_b, str_b, endness="Iend_BE")
|
|
|
|
ss_res = strncmp(s, arguments=[addr_a, addr_b, claripy.BVV(3, 64)])
|
|
assert s.solver.unique(ss_res)
|
|
assert s.solver.eval(ss_res) != 0
|
|
|
|
def test_strncmp_find_limits(self):
|
|
log.info("concrete a, concrete b, symbolic n")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_a = claripy.BVV(b"ABCD\0")
|
|
str_b = claripy.BVV(b"ABCE\0")
|
|
addr_a = claripy.BVV(0x10, 64)
|
|
addr_b = claripy.BVV(0xB0, 64)
|
|
s.memory.store(addr_a, str_a, endness="Iend_BE")
|
|
s.memory.store(addr_b, str_b, endness="Iend_BE")
|
|
|
|
n = claripy.BVS("n", 64)
|
|
ss_res = strncmp(s, arguments=[addr_a, addr_b, n])
|
|
s.add_constraints(ss_res == 0)
|
|
assert set(s.solver.eval_upto(n, 10)) == {0, 1, 2, 3}
|
|
|
|
def test_strncmp_find_prefix(self):
|
|
log.info("concrete a, symbolic b, symbolic n")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_a = claripy.BVV(b"ABCD\0")
|
|
str_b = claripy.BVS("str_b", len(str_a))
|
|
addr_a = claripy.BVV(0x10, 64)
|
|
addr_b = claripy.BVV(0xB0, 64)
|
|
s.memory.store(addr_a, str_a, endness="Iend_BE")
|
|
s.memory.store(addr_b, str_b, endness="Iend_BE")
|
|
|
|
# All prefixes should be valid
|
|
n = strlen(s, arguments=[addr_b])
|
|
ss_res = strncmp(s, arguments=[addr_a, addr_b, n])
|
|
s.add_constraints(ss_res == 0)
|
|
assert set(s.solver.eval_upto(n, 10)) == {0, 1, 2, 3, 4}
|
|
|
|
def test_strncmp_find_prefix_unsat(self):
|
|
log.info("concrete a, concrete b, symbolic n")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_a = claripy.BVV(b"\0\0\0\0\0")
|
|
str_b = claripy.BVV(b"ABCE\0")
|
|
addr_a = claripy.BVV(0x10, 64)
|
|
addr_b = claripy.BVV(0xB0, 64)
|
|
s.memory.store(addr_a, str_a, endness="Iend_BE")
|
|
s.memory.store(addr_b, str_b, endness="Iend_BE")
|
|
|
|
# No prefix should be valid
|
|
n = strlen(s, arguments=[addr_b])
|
|
ss_res = strncmp(s, arguments=[addr_a, addr_b, n])
|
|
s.add_constraints(ss_res == 0)
|
|
assert not s.satisfiable()
|
|
|
|
def test_strncmp_find_input_for_limit(self):
|
|
log.info("concrete a, symbolic b, symbolic n")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_a = claripy.BVV(b"ABCD\0")
|
|
str_b = claripy.BVS("str_b", len(str_a))
|
|
addr_a = claripy.BVV(0x10, 64)
|
|
addr_b = claripy.BVV(0xB0, 64)
|
|
s.memory.store(addr_a, str_a, endness="Iend_BE")
|
|
s.memory.store(addr_b, str_b, endness="Iend_BE")
|
|
|
|
n = claripy.BVS("n", 64)
|
|
ss_res = strncmp(s, arguments=[addr_a, addr_b, n])
|
|
s.add_constraints(ss_res == 0)
|
|
|
|
# Check constrained limit produces only expected input
|
|
for i in range(1, len(str_b) // 8):
|
|
s2 = s.copy()
|
|
s2.add_constraints(n == i)
|
|
hi, lo = 5 * 8 - 1, (5 - i) * 8
|
|
substr_a, substr_b = str_a[hi:lo], str_b[hi:lo]
|
|
assert s2.solver.unique(substr_b)
|
|
assert s2.solver.solution(substr_b, substr_a)
|
|
|
|
def test_strstr_conc_haystack_conc_needle(self):
|
|
log.info("concrete haystack and needle")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_haystack = claripy.BVV(0x41424300, 32)
|
|
str_needle = claripy.BVV(0x42430000, 32)
|
|
addr_haystack = claripy.BVV(0x10, 64)
|
|
addr_needle = claripy.BVV(0xB0, 64)
|
|
s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")
|
|
s.memory.store(addr_needle, str_needle, endness="Iend_BE")
|
|
|
|
ss_res = strstr(s, arguments=[addr_haystack, addr_needle])
|
|
assert s.solver.unique(ss_res)
|
|
assert s.solver.eval(ss_res) == 0x11
|
|
|
|
def test_strstr_conc_haystack_sym_needle(self):
|
|
log.info("concrete haystack, symbolic needle")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.libc.max_symbolic_strstr = 20
|
|
haystack = b"ABCD"
|
|
str_haystack = claripy.BVV(haystack + b"\0")
|
|
str_needle = claripy.BVS("needle", 32)
|
|
addr_haystack = claripy.BVV(0x10, 64)
|
|
addr_needle = claripy.BVV(0xB0, 64)
|
|
s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")
|
|
s.memory.store(addr_needle, str_needle, endness="Iend_BE")
|
|
s.memory.store(addr_needle + 4, claripy.BVV(0, 8))
|
|
|
|
ss_res = strstr(s, arguments=[addr_haystack, addr_needle])
|
|
results = set(s.solver.eval_upto(ss_res, len(haystack) * 2))
|
|
expected = {(addr_haystack.concrete_value + i) for i in range(len(haystack))} | {0}
|
|
assert results == expected
|
|
|
|
s_match = s.copy()
|
|
s_nomatch = s.copy()
|
|
s_match.add_constraints(ss_res != 0)
|
|
s_nomatch.add_constraints(ss_res == 0)
|
|
|
|
# Check all substrings
|
|
substrings = [haystack[l:h] for l, h in combinations(range(len(haystack) + 1), 2)]
|
|
needle_len = len(str_needle) // 8
|
|
for substring in substrings:
|
|
solution = claripy.BVV(substring.ljust(needle_len, b"\0"))
|
|
assert s_match.solver.solution(str_needle, solution)
|
|
assert not s_match.solver.solution(str_needle, claripy.BVV(b"AC\0\0"))
|
|
assert not s_match.solver.solution(str_needle, claripy.BVV(b"AD\0\0"))
|
|
assert s_nomatch.solver.satisfiable()
|
|
|
|
def test_strstr_sym_haystack_conc_needle(self):
|
|
log.info("symbolic haystack, concrete needle")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.libc.max_symbolic_strstr = 20
|
|
str_haystack = claripy.BVS("haystack", 5 * 8).concat(claripy.BVV(0, 8))
|
|
str_needle = claripy.BVV(b"ABC\0")
|
|
addr_haystack = claripy.BVV(0x10, 64)
|
|
addr_needle = claripy.BVV(0xB0, 64)
|
|
s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")
|
|
s.memory.store(addr_needle, str_needle, endness="Iend_BE")
|
|
|
|
ss_res = strstr(s, arguments=[addr_haystack, addr_needle])
|
|
|
|
s_match = s.copy()
|
|
s_match.add_constraints(ss_res != 0)
|
|
s_nomatch = s.copy()
|
|
s_nomatch.add_constraints(ss_res == 0)
|
|
|
|
num_possible = min(s.libc.max_symbolic_strstr, 1 + (len(str_haystack) - len(str_needle)) // 8)
|
|
expected = set(
|
|
range(
|
|
addr_haystack.concrete_value,
|
|
addr_haystack.concrete_value + num_possible,
|
|
)
|
|
)
|
|
results = set(s_match.solver.eval_exact(ss_res, num_possible))
|
|
assert results == expected
|
|
assert s_nomatch.solver.satisfiable()
|
|
|
|
def test_strstr_sym_haystack_sym_needle(self):
|
|
log.info("symbolic haystack, symbolic needle")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.libc.max_symbolic_strstr = 20
|
|
s.libc.buf_symbolic_bytes = 10
|
|
str_haystack = claripy.BVS("haystack", s.libc.buf_symbolic_bytes * 8)
|
|
str_needle = claripy.BVS("needle", s.libc.buf_symbolic_bytes * 8)
|
|
addr_haystack = claripy.BVV(0x10, 64)
|
|
addr_needle = claripy.BVV(0xB0, 64)
|
|
s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")
|
|
s.memory.store(addr_needle, str_needle, endness="Iend_BE")
|
|
|
|
ss_res = strstr(s, arguments=[addr_haystack, addr_needle])
|
|
|
|
s_match = s.copy()
|
|
s_nomatch = s.copy()
|
|
s_match.add_constraints(ss_res != 0)
|
|
s_nomatch.add_constraints(ss_res == 0)
|
|
|
|
s_i = s_match.copy()
|
|
s_i.add_constraints(str_needle == claripy.BVV(b"123".ljust(s.libc.buf_symbolic_bytes, b"\0")))
|
|
|
|
# Check needle is not found after end of haystack
|
|
s_ez = s_i.copy()
|
|
s_ez.add_constraints(str_haystack[len(str_haystack) - 1 : len(str_haystack) - 8] == 0)
|
|
assert not s_ez.satisfiable()
|
|
|
|
# Check target of specific offset
|
|
for i in range(5):
|
|
s_n = s_i.copy()
|
|
s_n.add_constraints(ss_res == addr_haystack + i)
|
|
h = s_n.solver.eval(str_haystack, cast_to=bytes)
|
|
assert h.find(b"123") == i
|
|
|
|
len_needle = strlen(s_match, arguments=[addr_needle])
|
|
match_cmp = strncmp(s_match, arguments=[ss_res, addr_needle, len_needle])
|
|
assert s_match.solver.eval_upto(match_cmp, 10) == [0]
|
|
|
|
r_mm = strstr(s_match, arguments=[addr_haystack, addr_needle])
|
|
s_match.add_constraints(r_mm == 0)
|
|
assert not s_match.satisfiable()
|
|
|
|
assert s_nomatch.satisfiable()
|
|
s_nss = s_nomatch.copy()
|
|
nomatch_ss = strstr(s_nss, arguments=[addr_haystack, addr_needle])
|
|
s_nss.add_constraints(nomatch_ss != 0)
|
|
assert not s_nss.satisfiable()
|
|
|
|
def test_strstr_inconsistency(self):
|
|
log.info("symbolic haystack, symbolic needle")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.libc.buf_symbolic_bytes = 2
|
|
addr_haystack = claripy.BVV(0x10, 64)
|
|
addr_needle = claripy.BVV(0xB0, 64)
|
|
# len_needle = strlen(s, inline=True, arguments=[addr_needle])
|
|
|
|
ss_res = strstr(s, arguments=[addr_haystack, addr_needle])
|
|
|
|
# slh_res = strlen(s, inline=True, arguments=[addr_haystack])
|
|
# sln_res = strlen(s, inline=True, arguments=[addr_needle])
|
|
# print "LENH:", s.solver.eval_upto(slh_res, 100)
|
|
# print "LENN:", s.solver.eval_upto(sln_res, 100)
|
|
|
|
assert not s.solver.unique(ss_res)
|
|
assert sorted(s.solver.eval_upto(ss_res, 100)) == [0, *list(range(16, 16 + s.libc.buf_symbolic_bytes - 1))]
|
|
|
|
s.add_constraints(ss_res != 0)
|
|
ss2 = strstr(s, arguments=[addr_haystack, addr_needle])
|
|
s.add_constraints(ss2 == 0)
|
|
assert not s.satisfiable()
|
|
|
|
def test_memcpy(self):
|
|
log.info("concrete src, concrete dst, concrete len")
|
|
log.debug("... full copy")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414141, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVV(0x42424242, 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
memcpy(s, arguments=[dst_addr, src_addr, claripy.BVV(4, 64)])
|
|
new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
|
|
assert s.solver.eval_upto(new_dst, 2, cast_to=bytes) == [b"BBBB"]
|
|
|
|
log.info("giant copy")
|
|
s = SimState(arch="AMD64", mode="symbolic", remove_options=angr.options.simplification)
|
|
s.memory._maximum_symbolic_size = 0x2000000
|
|
size = claripy.BVV(0x1000000, 64)
|
|
data = claripy.BVS("giant", 8 * 0x1_000_000)
|
|
dst_addr = claripy.BVV(0x2000000, 64)
|
|
src_addr = claripy.BVV(0x4000000, 64)
|
|
s.memory.store(src_addr, data)
|
|
|
|
memcpy(s, arguments=[dst_addr, src_addr, size])
|
|
assert s.memory.load(dst_addr, size) is s.memory.load(src_addr, size)
|
|
|
|
log.debug("... partial copy")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
memcpy(s, arguments=[dst_addr, src_addr, claripy.BVV(2, 64)])
|
|
new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
|
|
assert s.solver.eval_upto(new_dst, 2, cast_to=bytes) == [b"BBAA"]
|
|
|
|
log.info("symbolic src, concrete dst, concrete len")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414141, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVS("src", 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
|
|
# make sure it copies it all
|
|
memcpy(s, arguments=[dst_addr, src_addr, claripy.BVV(4, 64)])
|
|
assert s.satisfiable()
|
|
s.add_constraints(src != s.memory.load(dst_addr, 4))
|
|
assert not s.satisfiable()
|
|
|
|
log.info("symbolic src, concrete dst, symbolic len")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414141, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVS("src", 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
cpylen = claripy.BVS("len", 64)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
s.add_constraints(cpylen < 10)
|
|
memcpy(s, arguments=[dst_addr, src_addr, cpylen])
|
|
result = s.memory.load(dst_addr, 4, endness="Iend_BE")
|
|
|
|
# make sure it copies it all
|
|
s1 = s.copy()
|
|
s1.add_constraints(cpylen == 1)
|
|
assert s1.solver.unique(s1.memory.load(dst_addr + 1, 3))
|
|
assert len(s1.solver.eval_upto(s1.memory.load(dst_addr, 1), 300)) == 256
|
|
|
|
s2 = s.copy()
|
|
s2.add_constraints(cpylen == 2)
|
|
assert len(s2.solver.eval_upto(result[31:24], 300)) == 256
|
|
assert len(s2.solver.eval_upto(result[23:16], 300)) == 256
|
|
assert s2.solver.eval_upto(result[15:0], 300, cast_to=bytes) == [b"AA"]
|
|
|
|
log.info("concrete src, concrete dst, symbolic len")
|
|
dst = claripy.BVV(0x41414141, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVV(0x42424242, 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
cpylen = claripy.BVS("len", 64)
|
|
|
|
s.add_constraints(claripy.ULE(cpylen, 4))
|
|
memcpy(s, arguments=[dst_addr, src_addr, cpylen])
|
|
new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
|
|
assert sorted(s.solver.eval_upto(new_dst, 300, cast_to=bytes)) == [b"AAAA", b"BAAA", b"BBAA", b"BBBA", b"BBBB"]
|
|
|
|
def test_memcmp(self):
|
|
log.info("concrete src, concrete dst, concrete len")
|
|
|
|
log.debug("... full cmp")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414141, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVV(0x42424242, 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
r = memcmp(s, arguments=[dst_addr, src_addr, claripy.BVV(4, 64)])
|
|
assert s.satisfiable()
|
|
|
|
s_pos = s.copy()
|
|
s_pos.add_constraints(r.SGE(0))
|
|
assert not s_pos.satisfiable()
|
|
|
|
s_neg = s.copy()
|
|
s_neg.add_constraints(r.SLT(0))
|
|
assert s_neg.satisfiable()
|
|
|
|
log.debug("... zero cmp")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
r = memcmp(s, arguments=[dst_addr, src_addr, claripy.BVV(0, 64)])
|
|
assert s.solver.eval_upto(r, 2) == [0]
|
|
|
|
log.info("symbolic src, concrete dst, concrete len")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414141, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVS("src", 32)
|
|
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
|
|
# make sure it copies it all
|
|
r = memcmp(s, arguments=[dst_addr, src_addr, claripy.BVV(4, 64)])
|
|
|
|
s_match = s.copy()
|
|
s_match.add_constraints(r == 0)
|
|
m = s_match.memory.load(src_addr, 4)
|
|
assert s_match.solver.eval_upto(m, 2) == [0x41414141]
|
|
|
|
s_nomatch = s.copy()
|
|
s_nomatch.add_constraints(r != 0)
|
|
m = s_nomatch.memory.load(src_addr, 4)
|
|
assert not s_nomatch.solver.solution(m, 0x41414141)
|
|
|
|
log.info("symbolic src, concrete dst, symbolic len")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414141, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVS("src", 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
cmplen = claripy.BVS("len", 64)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
r = memcmp(s, arguments=[dst_addr, src_addr, cmplen])
|
|
|
|
# look at effects of different lengths
|
|
s1 = s.copy()
|
|
s1.add_constraints(cmplen == 1)
|
|
s1.add_constraints(r == 0)
|
|
log.debug("... simplifying")
|
|
s1.solver._solver.simplify()
|
|
log.debug("... solving")
|
|
assert s1.solver.eval_upto(src[31:24], 2) == [0x41]
|
|
assert not s1.solver.unique(src[31:16])
|
|
log.debug("... solved")
|
|
|
|
s2 = s.copy()
|
|
s2.add_constraints(cmplen == 2)
|
|
s2.add_constraints(r == 0)
|
|
assert s2.solver.eval_upto(s2.memory.load(src_addr, 2), 2) == [0x4141]
|
|
assert not s2.solver.unique(s2.memory.load(src_addr, 3))
|
|
|
|
s2u = s.copy()
|
|
s2u.add_constraints(cmplen == 2)
|
|
s2u.add_constraints(r == 1)
|
|
assert not s2u.solver.solution(s2u.memory.load(src_addr, 2), 0x4141)
|
|
|
|
def test_strncpy(self):
|
|
log.info("concrete src, concrete dst, concrete len")
|
|
log.debug("... full copy")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414100, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVV(0x42420000, 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
strncpy(s, arguments=[dst_addr, src_addr, claripy.BVV(3, 64)])
|
|
new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
|
|
assert s.solver.eval(new_dst, cast_to=bytes) == b"BB\x00\x00"
|
|
|
|
log.debug("... partial copy")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
strncpy(s, arguments=[dst_addr, src_addr, claripy.BVV(2, 64)])
|
|
new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
|
|
assert s.solver.eval_upto(new_dst, 2, cast_to=bytes) == [b"BBA\x00"]
|
|
|
|
log.info("symbolic src, concrete dst, concrete len")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414100, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVS("src", 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
|
|
# make sure it copies it all
|
|
s.add_constraints(strlen(s, arguments=[src_addr]) == 2)
|
|
|
|
# sanity check
|
|
s_false = s.copy()
|
|
s_false.add_constraints(strlen(s_false, arguments=[src_addr]) == 3)
|
|
assert not s_false.satisfiable()
|
|
|
|
strncpy(s, arguments=[dst_addr, src_addr, 3])
|
|
assert s.satisfiable()
|
|
c = strcmp(s, arguments=[dst_addr, src_addr])
|
|
|
|
assert s.solver.eval_upto(c, 10) == [0]
|
|
|
|
log.info("symbolic src, concrete dst, symbolic len")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414100, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVS("src", 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
maxlen = claripy.BVS("len", 64)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
|
|
# make sure it copies it all
|
|
s.add_constraints(strlen(s, arguments=[src_addr]) == 2)
|
|
strncpy(s, arguments=[dst_addr, src_addr, maxlen])
|
|
c = strcmp(s, arguments=[dst_addr, src_addr])
|
|
|
|
s_match = s.copy()
|
|
s_match.add_constraints(c == 0)
|
|
assert s_match.solver.min_int(maxlen) == 3
|
|
|
|
s_nomatch = s.copy()
|
|
s_nomatch.add_constraints(c != 0)
|
|
assert s_nomatch.solver.max_int(maxlen) == 2
|
|
|
|
log.info("concrete src, concrete dst, symbolic len")
|
|
log.debug("... full copy")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
|
|
dst = claripy.BVV(0x41414100, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVV(0x42420000, 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
maxlen = claripy.BVS("len", 64)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
strncpy(s, arguments=[dst_addr, src_addr, maxlen])
|
|
r = s.memory.load(dst_addr, 4, endness="Iend_BE")
|
|
# print repr(r.solver.eval_upto(r, 10, cast_to=bytes))
|
|
assert sorted(s.solver.eval_upto(r, 10, cast_to=bytes)) == [b"AAA\x00", b"BAA\x00", b"BB\x00\x00", b"BBA\x00"]
|
|
|
|
def test_strcpy(self):
|
|
log.info("concrete src, concrete dst")
|
|
|
|
log.debug("... full copy")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
dst = claripy.BVV(0x41414100, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVV(0x42420000, 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
strcpy(s, arguments=[dst_addr, src_addr])
|
|
new_dst = s.memory.load(dst_addr, 4, endness="Iend_BE")
|
|
assert s.solver.eval(new_dst, cast_to=bytes) == b"BB\x00\x00"
|
|
|
|
log.info("symbolic src, concrete dst")
|
|
dst = claripy.BVV(0x41414100, 32)
|
|
dst_addr = claripy.BVV(0x1000, 64)
|
|
src = claripy.BVS("src", 32)
|
|
src_addr = claripy.BVV(0x2000, 64)
|
|
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.memory.store(dst_addr, dst)
|
|
s.memory.store(src_addr, src)
|
|
|
|
ln = strlen(s, arguments=[src_addr])
|
|
|
|
strcpy(s, arguments=[dst_addr, src_addr])
|
|
|
|
cm = strcmp(s, arguments=[dst_addr, src_addr])
|
|
|
|
s.add_constraints(cm == 0)
|
|
|
|
s.add_constraints(ln == 15)
|
|
# readsize = 16
|
|
# both_strs = claripy.Concat(
|
|
# *[
|
|
# s.memory.load(dst_addr, readsize, endness="Iend_BE"),
|
|
# s.memory.load(src_addr, readsize, endness="Iend_BE"),
|
|
# ]
|
|
# )
|
|
# for i in s.solver.eval_upto(both_strs, 50, cast_to=bytes):
|
|
# assert s.solver.eval_upto(10) == [0]
|
|
# assert s.solver.solution(s.memory.load(dst_addr, 4, endness="Iend_BE"), 0x42434400)
|
|
# assert s.solver.solution(s.memory.load(dst_addr, 4, endness="Iend_BE"), 0x42434445)
|
|
# assert s.solver.solution(s.memory.load(dst_addr, 4, endness="Iend_BE"), 0x00414100)
|
|
# assert not s.solver.solution(s.memory.load(dst_addr, 4, endness="Iend_BE"), 0x00010203)
|
|
|
|
@broken
|
|
def test_sprintf(self):
|
|
log.info("concrete src, concrete dst, concrete len")
|
|
s = SimState(mode="symbolic", arch="PPC32")
|
|
format_str = claripy.BVV(0x25640000, 32)
|
|
format_addr = claripy.BVV(0x2000, 32)
|
|
# dst = claripy.BVV("destination", 128)
|
|
dst_addr = claripy.BVV(0x1000, 32)
|
|
arg = claripy.BVS("some_number", 32)
|
|
|
|
s.memory.store(format_addr, format_str)
|
|
|
|
sprintf(s, arguments=[dst_addr, format_addr, arg])
|
|
|
|
for i in range(9):
|
|
j = random.randint(10**i, 10 ** (i + 1))
|
|
s2 = s.copy()
|
|
s2.add_constraints(arg == j)
|
|
# print s2.solver.eval_upto(s2.memory.load(dst_addr, i+2), 2, cast_to=bytes), repr(b"%d\x00" % j)
|
|
assert s2.solver.eval_upto(s2.memory.load(dst_addr, i + 2), 2, cast_to=bytes) == [b"%d\x00" % j]
|
|
|
|
s2 = s.copy()
|
|
s2.add_constraints(arg == 0)
|
|
# print s2.solver.eval_upto(s2.memory.load(dst_addr, 2), 2, cast_to=bytes), repr(b"%d\x00" % 0)
|
|
assert s2.solver.eval_upto(s2.memory.load(dst_addr, 2), 2, cast_to=bytes) == [b"%d\x00" % 0]
|
|
|
|
def test_memset(self):
|
|
log.info("concrete src, concrete dst, concrete len")
|
|
s = SimState(arch="PPC32", mode="symbolic")
|
|
dst = claripy.BVV(0, 128)
|
|
dst_addr = claripy.BVV(0x1000, 32)
|
|
char = claripy.BVV(0x00000041, 32)
|
|
char2 = claripy.BVV(0x50505050, 32)
|
|
length = claripy.BVS("some_length", 32)
|
|
|
|
s.memory.store(dst_addr, dst)
|
|
memset(s, arguments=[dst_addr, char, claripy.BVV(3, 32)])
|
|
assert s.solver.eval(s.memory.load(dst_addr, 4)) == 0x41414100
|
|
|
|
log.debug("Symbolic length")
|
|
s = SimState(arch="PPC32", mode="symbolic")
|
|
s.memory.store(dst_addr, dst)
|
|
length = claripy.BVS("some_length", 32)
|
|
s.add_constraints(length < 10)
|
|
memset(s, arguments=[dst_addr, char2, length])
|
|
|
|
log.debug("Trying 2")
|
|
s_two = s.copy()
|
|
s_two.add_constraints(length == 2)
|
|
assert s_two.solver.eval(s_two.memory.load(dst_addr, 4)) == 0x50500000
|
|
|
|
log.debug("Trying 0")
|
|
s_zero = s.copy()
|
|
s_zero.add_constraints(length == 0)
|
|
assert s_zero.solver.eval(s_zero.memory.load(dst_addr, 4)) == 0x00000000
|
|
|
|
log.debug("Trying 5")
|
|
s_five = s.copy()
|
|
s_five.add_constraints(length == 5)
|
|
assert s_five.solver.eval(s_five.memory.load(dst_addr, 6)) == 0x505050505000
|
|
|
|
def test_strchr(self):
|
|
log.info("concrete haystack and needle")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_haystack = claripy.BVV(0x41424300, 32)
|
|
str_needle = claripy.BVV(0x42, 64)
|
|
addr_haystack = claripy.BVV(0x10, 64)
|
|
s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")
|
|
|
|
ss_res = strchr(s, arguments=[addr_haystack, str_needle])
|
|
assert s.solver.unique(ss_res)
|
|
assert s.solver.eval(ss_res) == 0x11
|
|
|
|
log.info("concrete haystack, symbolic needle")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_haystack = claripy.BVV(0x41424300, 32)
|
|
str_needle = claripy.BVS("wtf", 64)
|
|
chr_needle = str_needle[7:0]
|
|
addr_haystack = claripy.BVV(0x10, 64)
|
|
s.memory.store(addr_haystack, str_haystack, endness="Iend_BE")
|
|
|
|
ss_res = strchr(s, arguments=[addr_haystack, str_needle])
|
|
assert not s.solver.unique(ss_res)
|
|
assert len(s.solver.eval_upto(ss_res, 10)) == 5
|
|
|
|
s_match = s.copy()
|
|
s_nomatch = s.copy()
|
|
s_match.add_constraints(ss_res != 0)
|
|
s_nomatch.add_constraints(ss_res == 0)
|
|
|
|
assert s_match.satisfiable()
|
|
assert s_nomatch.satisfiable()
|
|
assert len(s_match.solver.eval_upto(chr_needle, 300)) == 4
|
|
assert len(s_nomatch.solver.eval_upto(chr_needle, 300)) == 252
|
|
assert sorted(s_match.solver.eval_upto(ss_res, 300)) == [0x10, 0x11, 0x12, 0x13]
|
|
assert sorted(s_match.solver.eval_upto(chr_needle, 300)) == [0x00, 0x41, 0x42, 0x43]
|
|
|
|
s_match.memory.store(ss_res, claripy.BVV(0x44, 8))
|
|
assert sorted(s_match.solver.eval_upto(s_match.memory.load(0x10, 1), 300)) == [0x41, 0x44]
|
|
assert sorted(s_match.solver.eval_upto(s_match.memory.load(0x11, 1), 300)) == [0x42, 0x44]
|
|
assert sorted(s_match.solver.eval_upto(s_match.memory.load(0x12, 1), 300)) == [0x43, 0x44]
|
|
assert sorted(s_match.solver.eval_upto(s_match.memory.load(0x13, 1), 300)) == [0x00, 0x44]
|
|
|
|
# l.info("symbolic haystack, symbolic needle")
|
|
# s = SimState(arch="AMD64", mode="symbolic")
|
|
# s.libc.buf_symbolic_bytes = 5
|
|
# addr_haystack = claripy.BVV(0x10, 64)
|
|
# addr_needle = claripy.BVV(0xb0, 64)
|
|
# len_needle = strlen(s, inline=True, arguments=[addr_needle])
|
|
|
|
# ss_res = strstr(s, inline=True, arguments=[addr_haystack, addr_needle])
|
|
# ss_val = s.expr_value(ss_res)
|
|
|
|
# assert not ss_val.is_unique()
|
|
# assert len(ss_val.solver.eval_upto(100)) == s.libc.buf_symbolic_bytes
|
|
|
|
# s_match = s.copy()
|
|
# s_nomatch = s.copy()
|
|
# s_match.add_constraints(ss_res != 0)
|
|
# s_nomatch.add_constraints(ss_res == 0)
|
|
|
|
# match_cmp = strncmp(s_match, inline=True, arguments=[ss_res, addr_needle, len_needle])
|
|
# match_cmp_val = s_match.expr_value(match_cmp)
|
|
# assert match_cmp_val.solver.eval_upto(10) == [0]
|
|
|
|
# r_mm = strstr(s_match, inline=True, arguments=[addr_haystack, addr_needle])
|
|
# s_match.add_constraints(r_mm == 0)
|
|
# assert not s_match.satisfiable()
|
|
|
|
# assert s_nomatch.satisfiable()
|
|
# s_nss = s_nomatch.copy()
|
|
# nomatch_ss = strstr(s_nss, inline=True, arguments=[addr_haystack, addr_needle])
|
|
# s_nss.add_constraints(nomatch_ss != 0)
|
|
# assert not s_nss.satisfiable()
|
|
|
|
@broken
|
|
def test_strtok_r(self):
|
|
log.debug("CONCRETE MODE")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
s.memory.store(100, claripy.BVV(0x4141414241414241424300, 88), endness="Iend_BE")
|
|
s.memory.store(200, claripy.BVV(0x4200, 16), endness="Iend_BE")
|
|
str_ptr = claripy.BVV(100, s.arch.bits)
|
|
delim_ptr = claripy.BVV(200, s.arch.bits)
|
|
state_ptr = claripy.BVV(300, s.arch.bits)
|
|
|
|
st1 = strtok_r(s, arguments=[str_ptr, delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st1, 10) == [104]
|
|
assert s.solver.eval_upto(s.memory.load(st1 - 1, 1), 10) == [0]
|
|
assert s.solver.eval_upto(s.memory.load(200, 2), 10) == [0x4200]
|
|
|
|
st2 = strtok_r(s, arguments=[claripy.BVV(0, s.arch.bits), delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st2, 10) == [107]
|
|
assert s.solver.eval_upto(s.memory.load(st2 - 1, 1), 10) == [0]
|
|
|
|
st3 = strtok_r(s, arguments=[claripy.BVV(0, s.arch.bits), delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st3, 10) == [109]
|
|
assert s.solver.eval_upto(s.memory.load(st3 - 1, 1), 10) == [0]
|
|
|
|
st4 = strtok_r(s, arguments=[claripy.BVV(0, s.arch.bits), delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st4, 10) == [0]
|
|
assert s.solver.eval_upto(s.memory.load(300, s.arch.bytes, endness=s.arch.memory_endness), 10) == [109]
|
|
|
|
st5 = strtok_r(s, arguments=[claripy.BVV(0, s.arch.bits), delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st5, 10) == [0]
|
|
assert s.solver.eval_upto(s.memory.load(300, s.arch.bytes, endness=s.arch.memory_endness), 10) == [109]
|
|
|
|
s.memory.store(1000, claripy.BVV(0x4141414241414241424300, 88), endness="Iend_BE")
|
|
s.memory.store(2000, claripy.BVV(0x4200, 16), endness="Iend_BE")
|
|
str_ptr = claripy.BVV(1000, s.arch.bits)
|
|
delim_ptr = claripy.BVV(2000, s.arch.bits)
|
|
state_ptr = claripy.BVV(3000, s.arch.bits)
|
|
|
|
st1 = strtok_r(s, arguments=[str_ptr, delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st1, 10) == [1004]
|
|
assert s.solver.eval_upto(s.memory.load(st1 - 1, 1), 10) == [0]
|
|
assert s.solver.eval_upto(s.memory.load(2000, 2), 10) == [0x4200]
|
|
|
|
st2 = strtok_r(s, arguments=[claripy.BVV(0, s.arch.bits), delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st2, 10) == [1007]
|
|
assert s.solver.eval_upto(s.memory.load(st2 - 1, 1), 10) == [0]
|
|
|
|
st3 = strtok_r(s, arguments=[claripy.BVV(0, s.arch.bits), delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st3, 10) == [1009]
|
|
assert s.solver.eval_upto(s.memory.load(st3 - 1, 1), 10) == [0]
|
|
|
|
st4 = strtok_r(s, arguments=[claripy.BVV(0, s.arch.bits), delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st4, 10) == [0]
|
|
assert s.solver.eval_upto(s.memory.load(3000, s.arch.bytes, endness=s.arch.memory_endness), 10) == [1009]
|
|
|
|
st5 = strtok_r(s, arguments=[claripy.BVV(0, s.arch.bits), delim_ptr, state_ptr])
|
|
assert s.solver.eval_upto(st5, 10) == [0]
|
|
assert s.solver.eval_upto(s.memory.load(3000, s.arch.bytes, endness=s.arch.memory_endness), 10) == [1009]
|
|
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_ptr = claripy.BVV(100, s.arch.bits)
|
|
delim_ptr = claripy.BVV(200, s.arch.bits)
|
|
state_ptr = claripy.BVV(300, s.arch.bits)
|
|
|
|
s.add_constraints(s.memory.load(delim_ptr, 1) != 0)
|
|
|
|
st1 = strtok_r(s, arguments=[str_ptr, delim_ptr, state_ptr])
|
|
s.add_constraints(st1 != 0)
|
|
assert s.solver.eval_upto(s.memory.load(st1 - 1, 1), 10) == [0]
|
|
|
|
def test_getc(self):
|
|
s = make_state_with_stdin(b"1234")
|
|
stdin = s.posix.get_fd(0)
|
|
s.mem[0x1000 + 0x70].int = 0
|
|
|
|
assert s.solver.eval_one(stdin.tell()) == 0
|
|
|
|
# The argument of getc should be a FILE *
|
|
c = getc(s, [0x1000])
|
|
assert s.solver.eval_upto(c, 300) == [0x31]
|
|
assert s.solver.eval_upto(stdin.tell(), 300) == [1]
|
|
|
|
c = getc(s, [0x1000])
|
|
assert s.solver.eval_upto(c, 300) == [0x32]
|
|
assert s.solver.eval_upto(stdin.tell(), 300) == [2]
|
|
|
|
c = getc(s, [0x1000])
|
|
assert s.solver.eval_upto(c, 300) == [0x33]
|
|
assert s.solver.eval_upto(stdin.tell(), 300) == [3]
|
|
|
|
c = getc(s, [0x1000])
|
|
assert s.solver.eval_upto(c, 300) == [0x34]
|
|
assert s.solver.eval_upto(stdin.tell(), 300) == [4]
|
|
|
|
def test_getchar(self):
|
|
s = make_state_with_stdin(b"1234")
|
|
stdin = s.posix.get_fd(0)
|
|
|
|
assert s.solver.eval_upto(stdin.tell(), 300) == [0]
|
|
c = getchar(s, arguments=[])
|
|
assert s.solver.eval_upto(c, 300) == [0x31]
|
|
assert s.solver.eval_upto(stdin.tell(), 300) == [1]
|
|
|
|
c = getchar(s, arguments=[])
|
|
assert s.solver.eval_upto(c, 300) == [0x32]
|
|
assert s.solver.eval_upto(stdin.tell(), 300) == [2]
|
|
|
|
c = getchar(s, arguments=[])
|
|
assert s.solver.eval_upto(c, 300) == [0x33]
|
|
assert s.solver.eval_upto(stdin.tell(), 300) == [3]
|
|
|
|
c = getchar(s, arguments=[])
|
|
assert s.solver.eval_upto(c, 300) == [0x34]
|
|
assert s.solver.eval_upto(stdin.tell(), 300) == [4]
|
|
|
|
def test_scanf(self):
|
|
s = make_state_with_stdin(b"Hello\n")
|
|
s.memory.store(0x2000, b"%1s\0")
|
|
scanf(s, [0x2000, 0x1000])
|
|
assert s.solver.eval_upto(s.memory.load(0x1000, 2), 2, cast_to=bytes) == [b"H\x00"]
|
|
|
|
def test_strcmp_concrete(self):
|
|
log.info("concrete a, concrete b")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
a_addr = claripy.BVV(0x10, 64)
|
|
b_addr = claripy.BVV(0xB0, 64)
|
|
|
|
s.memory.store(a_addr, b"heck\x00")
|
|
s.memory.store(b_addr, b"heck\x00")
|
|
|
|
r = strcmp(s, arguments=[a_addr, b_addr])
|
|
assert s.solver.eval_upto(r, 2) == [0]
|
|
|
|
log.info("concrete a, empty b")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
a_addr = claripy.BVV(0x10, 64)
|
|
b_addr = claripy.BVV(0xB0, 64)
|
|
|
|
s.memory.store(a_addr, b"heck\x00")
|
|
s.memory.store(b_addr, b"\x00")
|
|
|
|
r = strcmp(s, arguments=[a_addr, b_addr])
|
|
assert s.solver.eval_upto(r, 2) == [1]
|
|
|
|
log.info("empty a, concrete b")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
a_addr = claripy.BVV(0x10, 64)
|
|
b_addr = claripy.BVV(0xB0, 64)
|
|
|
|
s.memory.store(a_addr, b"\x00")
|
|
s.memory.store(b_addr, b"heck\x00")
|
|
|
|
r = strcmp(s, arguments=[a_addr, b_addr])
|
|
assert s.solver.eval_upto(r, 2) == [0xFFFFFFFF]
|
|
|
|
log.info("empty a, empty b")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
a_addr = claripy.BVV(0x10, 64)
|
|
b_addr = claripy.BVV(0xB0, 64)
|
|
|
|
s.memory.store(a_addr, b"\x00")
|
|
s.memory.store(b_addr, b"\x00")
|
|
|
|
r = strcmp(s, arguments=[a_addr, b_addr])
|
|
assert s.solver.eval_upto(r, 2) == [0]
|
|
|
|
def test_wcscmp(self):
|
|
# concrete cases for the wide char version sufficiently overlap with strcmp and friends
|
|
log.info("concrete a, symbolic b")
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
heck = "heck\x00".encode("utf-16")[2:] # remove encoding prefix
|
|
a_addr = claripy.BVV(0x10, 64)
|
|
b_addr = claripy.BVV(0xB0, 64)
|
|
b_bvs = claripy.BVS("b", len(heck) * 8)
|
|
|
|
s.memory.store(a_addr, heck)
|
|
s.memory.store(b_addr, b_bvs)
|
|
|
|
r = wcscmp(s, arguments=[a_addr, b_addr])
|
|
|
|
solutions = s.solver.eval_upto(b_bvs, 2, cast_to=bytes, extra_constraints=(r == 0,))
|
|
assert solutions == [heck]
|
|
|
|
def test_string_without_null(self):
|
|
s = SimState(arch="AMD64", mode="symbolic")
|
|
str_ = b"abcd"
|
|
str_addr = claripy.BVV(0x10, 64)
|
|
s.memory.store(str_addr, str_)
|
|
assert s.solver.eval(s.mem[str_addr].string.resolved, cast_to=bytes) == b"abcd"
|
|
|
|
|
|
if __name__ == "__main__":
|
|
unittest.main()
|