From bbc36a2b2e1be545f138be44c9c1be1764f2551d Mon Sep 17 00:00:00 2001 From: Yan Date: Fri, 24 Feb 2017 15:56:46 -0500 Subject: [PATCH] Use issymbolic() throughout Manticore (#22) * Use issymbolic() throughout Manticore * Add a missed import * absolute -> relative import * Import issymbolic from helpers * Missing import --- manticore/__init__.py | 3 ++- manticore/core/cpu/abstractcpu.py | 9 +++---- manticore/core/cpu/arm.py | 9 +++---- manticore/core/cpu/x86.py | 27 +++++++++++---------- manticore/core/executor.py | 11 +++++---- manticore/core/memory.py | 13 +++++----- manticore/core/smtlib/operators.py | 5 ++-- manticore/core/smtlib/solver.py | 7 +++--- manticore/manticore.py | 10 +------- manticore/models/decree.py | 38 ++++++++++++++++-------------- manticore/models/libc.py | 17 ++++++------- manticore/models/linux.py | 29 ++++++++++++----------- manticore/models/windows.py | 23 +++++++++--------- manticore/utils/helpers.py | 9 +++++++ 14 files changed, 112 insertions(+), 98 deletions(-) create mode 100644 manticore/utils/helpers.py diff --git a/manticore/__init__.py b/manticore/__init__.py index 145f57e..aa195c2 100644 --- a/manticore/__init__.py +++ b/manticore/__init__.py @@ -1 +1,2 @@ -from .manticore import Manticore, issymbolic \ No newline at end of file +from .manticore import Manticore +from .utils.helpers import issymbolic \ No newline at end of file diff --git a/manticore/core/cpu/abstractcpu.py b/manticore/core/cpu/abstractcpu.py index ca4ddba..dc00713 100644 --- a/manticore/core/cpu/abstractcpu.py +++ b/manticore/core/cpu/abstractcpu.py @@ -7,6 +7,7 @@ from unicorn.arm_const import * from abc import ABCMeta, abstractmethod from ..smtlib import Expression, Bool, BitVec, Array, Operators, Constant from ..memory import MemoryException +from ...utils.helpers import issymbolic import sys from functools import wraps import types @@ -311,7 +312,7 @@ class Cpu(object): # check access_ok for i in xrange(0, self.max_instr_width): c = self.memory[pc+i] - if isinstance(c, Expression): + if issymbolic(c): assert isinstance(c, BitVec) and c.size == 8 if isinstance(c, Constant): c = chr(c.value) @@ -405,7 +406,7 @@ class Cpu(object): self.PC += instruction.size addr = op.address() #FIXME maybe add a kwarg parameter to operand.address() with the current pc? self.PC -= instruction.size - assert not isinstance(addr, Expression) + assert not issymbolic(addr) num_bytes = op.size/8 needed_bytes.update(range(addr, addr + num_bytes)) # Request the bytes of the instruction. @@ -415,7 +416,7 @@ class Cpu(object): for addr in needed_bytes: needed_pages.add(addr & (~0xFFF)) val = self.read_int(addr, 8) - if isinstance(val, Expression): + if issymbolic(val): logger.debug("Concretizing bytes before passing it to unicorn") raise ConcretizeMemory(addr, 8, "Passing control to emulator", 'SAMPLED') byte_values[addr] = val @@ -504,7 +505,7 @@ class Cpu(object): regs = self._regfile.canonical_registers for reg_name in regs: value = self.read_register(reg_name) - if isinstance(value, Expression): + if issymbolic(value): aux = "%3s: "%reg_name +"%16s"%value result += aux elif isinstance(value, (int, long)): diff --git a/manticore/core/cpu/arm.py b/manticore/core/cpu/arm.py index f0f462e..7fa040f 100644 --- a/manticore/core/cpu/arm.py +++ b/manticore/core/cpu/arm.py @@ -5,6 +5,7 @@ from .abstractcpu import SymbolicPCException, InvalidPCException, Interruption from .abstractcpu import instruction as abstract_instruction from .register import Register from ..smtlib import Operators, Expression +from ...utils.helpers import issymbolic # from ..smtlib import * from functools import wraps from bitwise import * @@ -49,7 +50,7 @@ def instruction(body): should_execute = cpu.shouldExecuteConditional() - if isinstance(should_execute, Expression): + if issymbolic(should_execute): i_size = cpu.address_bit_size / 8 cpu.PC = Operators.ITEBV(cpu.address_bit_size, should_execute, cpu.PC-i_size, cpu.PC) @@ -312,7 +313,7 @@ class Armv7Cpu(Cpu): logger.debug("Emulator wants this regs %r", regs) for reg in regs: value = cpu.read_register(reg) - if isinstance(value, Expression): + if issymbolic(value): raise ConcretizeRegister(reg, "Passing control to emulator") #FIXME improve exception to handle multiple registers at a time reg_values[reg] = value @@ -527,7 +528,7 @@ class Armv7Cpu(Cpu): return Operators.ITEBV(cpu.address_bit_size, flag_expr, BitVecConstant(cpu.address_bit_size, 1 << offset), BitVecConstant(cpu.address_bit_size, 0)) - if any(isinstance(x, Expression) for x in [N, Z, C, V]): + if any(issymbolic(x) for x in [N, Z, C, V]): cpsr = (make_cpsr_flag(N, 31) | make_cpsr_flag(Z, 30) | make_cpsr_flag(C, 29) | @@ -959,4 +960,4 @@ class Armv7Cpu(Cpu): @instruction def STCL(cpu, *operands): - pass \ No newline at end of file + pass diff --git a/manticore/core/cpu/x86.py b/manticore/core/cpu/x86.py index 4da4a4b..fca8a8e 100644 --- a/manticore/core/cpu/x86.py +++ b/manticore/core/cpu/x86.py @@ -37,6 +37,7 @@ from functools import wraps, partial import collections from ..smtlib import * from ..memory import MemoryException +from ...utils.helpers import issymbolic import logging logger = logging.getLogger("CPU") @@ -84,7 +85,7 @@ def rep(old_method): if (X86_PREFIX_REP in prefix): counter_name = {16: 'CX', 32: 'ECX', 64: 'RCX'}[cpu.instruction.addr_size*8] count = cpu.read_register(counter_name) - if isinstance(count, Expression): + if issymbolic(count): raise ConcretizeRegister(counter_name, "Concretizing {} on REP instruction".format(counter_name), policy='SAMPLED') FLAG = count != 0 @@ -112,7 +113,7 @@ def repe(old_method): if (X86_PREFIX_REP in prefix) or (X86_PREFIX_REPNE in prefix): counter_name = {16: 'CX', 32: 'ECX', 64: 'RCX'}[cpu.instruction.addr_size*8] count = cpu.read_register(counter_name) - if isinstance(count, Expression): + if issymbolic(count): raise ConcretizeRegister(counter_name, "Concretizing {} on REP instruction".format(counter_name), policy='SAMPLED') FLAG = count != 0 @@ -129,7 +130,7 @@ def repe(old_method): elif X86_PREFIX_REPNE in prefix: FLAG = Operators.AND(cpu.ZF == False, count != 0) #true FLAG means loop - #if isinstance(FLAG, Expression): + #if issymbolic(FLAG): # raise ConcretizeRegister('ZF', "Concretizing ZF on REP instruction", policy='ALL') #if not FLAG: @@ -562,7 +563,7 @@ class AMD64RegFile(RegisterFile): for flag, offset in self._flags.iteritems(): flags.append((self._registers[flag], offset)) - if any(isinstance(flag, Expression) for flag, offset in flags): + if any(issymbolic(flag) for flag, offset in flags): res = reduce(operator.or_, map(make_symbolic, flags)) else: res = 0 @@ -830,7 +831,7 @@ class X86Cpu(Cpu): for reg in regs: value = cpu.read_register(reg) - if isinstance(value, Expression): + if issymbolic(value): raise ConcretizeRegister(reg, "Passing control to emulator") reg_values[reg] = value @@ -2402,7 +2403,7 @@ class X86Cpu(Cpu): @param src: source operand. ''' used_regs = (cpu.SF, cpu.ZF, cpu.AF, cpu.PF, cpu.CF) - is_expression = any(isinstance(x, Expression) for x in used_regs) + is_expression = any(issymbolic(x) for x in used_regs) def make_flag(val, offset): if is_expression: @@ -3830,7 +3831,7 @@ class X86Cpu(Cpu): # We can't use this one as the 'true' expresion gets eagerly calculated even on count == 0 + cpu.CF = Operators.ITE(count!=0, ((value >> Operators.ZEXTEND(count-1, OperandSize)) & 1) !=0, cpu.CF) # cpu.CF = Operators.ITE(count!=0, ((value >> Operators.ZEXTEND(count-1, OperandSize)) & 1) !=0, cpu.CF) - if isinstance(count, Expression): + if issymbolic(count): # We can't use this one as the EXTRACT op needs the offset arguments to be concrete # cpu.CF = Operators.ITE(count!=0, Operands.EXTRACT(value,count-1,1) !=0, cpu.CF) cpu.CF = Operators.ITE(Operators.AND(count != 0, count <= OperandSize), ((value >> Operators.ZEXTEND(count-1, OperandSize)) & 1) !=0, cpu.CF) @@ -3870,7 +3871,7 @@ class X86Cpu(Cpu): MASK = (1<> Operators.ZEXTEND(count-1, OperandSize)) & 1) !=0, cpu.CF) else: if count != 0: @@ -5578,7 +5579,7 @@ class X86Cpu(Cpu): def LSL(cpu, limit_ptr, selector): selector = selector.read() - if isinstance(selector, Expression): + if issymbolic(selector): # need to check if selector can be any of cpu_segments.keys() # and if so concretize acordinglyi raise NotImplementedError("Do not yet implement symbolic LSL") @@ -5829,7 +5830,7 @@ class AMD64Cpu(X86Cpu): regs = ('RAX', 'RCX', 'RDX', 'RBX', 'RSP', 'RBP', 'RSI', 'RDI', 'R8', 'R9', 'R10', 'R11', 'R12', 'R13', 'R14', 'R15', 'RIP', 'EFLAGS') for reg_name in regs: value = self.read_register(reg_name) - if isinstance(value, Expression): + if issymbolic(value): result += "%3s: "%reg_name + CFAIL result += visitors.pretty_print (value, depth=10) result += CEND @@ -5841,7 +5842,7 @@ class AMD64Cpu(X86Cpu): pos = 0 for reg_name in ('CF','SF','ZF','OF','AF', 'PF', 'IF', 'DF'): value = self.read_register(reg_name) - if isinstance(value, Expression): + if issymbolic(value): result += "%s:"%reg_name + CFAIL #"%16s"%value+CEND result += visitors.pretty_print (value, depth=10) + CEND @@ -5948,7 +5949,7 @@ class I386Cpu(X86Cpu): regs = ('EAX', 'ECX', 'EDX', 'EBX', 'ESP', 'EBP', 'ESI', 'EDI', 'EIP') for reg_name in regs: value = self.read_register(reg_name) - if isinstance(value, Expression): + if issymbolic(value): result += "%3s: "%reg_name + CFAIL result += visitors.pretty_print (value, depth=10) + CEND else: @@ -5959,7 +5960,7 @@ class I386Cpu(X86Cpu): pos = 0 for reg_name in ['CF','SF','ZF','OF','AF', 'PF', 'IF', 'DF']: value = self.read_register(reg_name) - if isinstance(value, Expression): + if issymbolic(value): result += "%s:"%reg_name + CFAIL #"%16s"%value+CEND result += visitors.pretty_print (value, depth=10) + CEND diff --git a/manticore/core/executor.py b/manticore/core/executor.py index 30a3faa..c60c7cc 100644 --- a/manticore/core/executor.py +++ b/manticore/core/executor.py @@ -46,6 +46,7 @@ from .cpu.abstractcpu import ConcretizeRegister, ConcretizeMemory, \ from .memory import MemoryException, SymbolicMemoryException from .smtlib import solver, Expression, Operators, SolverException, Array, BitVec, Bool, ConstraintSet from ..utils.event import Signal +from ..utils.helpers import issymbolic #Multiprocessing from multiprocessing import Manager @@ -245,7 +246,7 @@ class State(object): if string: for b in data: - if isinstance(b, Expression): + if issymbolic(b): self.constraints.add(b != 0) else: assert b!=0 @@ -494,12 +495,12 @@ class Executor(object): except KeyError: state.branches[(last_pc, state.cpu.PC)] = 1 item = (last_pc, state.cpu.PC) - assert not isinstance(last_pc, Expression) - assert not isinstance(state.cpu.PC, Expression) + assert not issymbolic(last_pc) + assert not issymbolic(state.cpu.PC) if item not in self._all_branches: self._all_branches.append(item) - assert not isinstance(last_pc, Expression) + assert not issymbolic(last_pc) self._states[state.name] = {'received' : receive_size, 'transmited': transmit_size, @@ -922,7 +923,7 @@ class Executor(object): count += 1 if self.dump_every and count >= max_iters: - if not isinstance(current_state.cpu.PC, Expression): + if not issymbolic(current_state.cpu.PC): raise MaxConsecutiveIntructions() except MaxConsecutiveIntructions as e: diff --git a/manticore/core/memory.py b/manticore/core/memory.py index 6ce59c5..8f20970 100644 --- a/manticore/core/memory.py +++ b/manticore/core/memory.py @@ -31,6 +31,7 @@ from cStringIO import StringIO from .smtlib import * import logging from .mappings import _mmap, _munmap +from ..utils.helpers import issymbolic logger = logging.getLogger('MEMORY') @@ -60,7 +61,7 @@ class SymbolicMemoryException(MemoryException): self.size = size def __str__(self): - return '%s <%s>'%(self.cause, isinstance(self.address, Expression) and repr(self.address) or '%08x'%self.address) + return '%s <%s>'%(self.cause, issymbolic(self.address) and repr(self.address) or '%08x'%self.address) class Map(object): ''' @@ -860,10 +861,10 @@ class SMemory(Memory): def read(self, address, size): ''' Read a stream of potentially symbolic bytes from a potentially symbolic address ''' size = self._get_size(size) - assert not isinstance(size, Expression) + assert not issymbolic(size) - if isinstance(address, Expression): + if issymbolic(address): assert solver.check(self.constraints) logger.info('Reading %d bytes from symbolic address %s', size, address) try: @@ -935,7 +936,7 @@ class SMemory(Memory): def write(self, address, value): size = len(value) - if isinstance(address, Expression): + if issymbolic(address): solutions = solver.get_all_values(self.constraints, address, maxcnt=0x1000) #if more than 0x3000 exception @@ -955,7 +956,7 @@ class SMemory(Memory): else: for offset in xrange(size): - if isinstance(value[offset], Expression): + if issymbolic(value[offset]): if not self.access_ok(address+offset, 'w'): raise MemoryException('No access writing', address+offset) self._symbols[address+offset] = [(True, value[offset])] @@ -984,4 +985,4 @@ class SMemory32L(SMemory): class SMemory64(SMemory): memory_bit_size = 64 - page_bit_size = 12 \ No newline at end of file + page_bit_size = 12 diff --git a/manticore/core/smtlib/operators.py b/manticore/core/smtlib/operators.py index 54bd78a..39e9b14 100644 --- a/manticore/core/smtlib/operators.py +++ b/manticore/core/smtlib/operators.py @@ -1,4 +1,5 @@ from expression import * +from ...utils.helpers import issymbolic import math @@ -146,7 +147,7 @@ def ZEXTEND(x, size): def CONCAT(total_size, *args): arg_size = total_size / len(args) - if any((isinstance(x, Expression) for x in args)): + if any(issymbolic(x) for x in args): if len(args) > 1: def cast(x): if isinstance(x, (int, long)): @@ -247,7 +248,7 @@ def SREM(a, b): def simplify(value): - if isinstance(value, Expression): + if issymbolic(value): return value.simplify() return value diff --git a/manticore/core/smtlib/solver.py b/manticore/core/smtlib/solver.py index d057746..1da0f60 100644 --- a/manticore/core/smtlib/solver.py +++ b/manticore/core/smtlib/solver.py @@ -23,6 +23,7 @@ import logging import re import time from visitors import * +from ...utils.helpers import issymbolic logger = logging.getLogger("SMT") class SolverException(Exception): @@ -92,7 +93,7 @@ class Solver(object): def minmax(self, constraints, x, iters=10000): ''' Returns the min and max possible values for x. ''' - if isinstance(x, Expression): + if issymbolic(x): m = self.min(constraints, x, iters) M = self.max(constraints, x, iters) return m, M @@ -275,7 +276,7 @@ class SMTSolver(Solver): of constraints. The current set of assertions must be sat. @param val: an expression or symbol ''' - if not isinstance(expression, Expression): + if not issymbolic(expression): return expression assert isinstance(expression, Variable) @@ -413,7 +414,7 @@ class SMTSolver(Solver): of constraints. The current set of assertions must be sat. @param val: an expression or symbol ''' - if not isinstance(expression, Expression): + if not issymbolic(expression): if isinstance(expression, str): expression = ord(expression) return expression diff --git a/manticore/manticore.py b/manticore/manticore.py index dbba194..c7eed2a 100644 --- a/manticore/manticore.py +++ b/manticore/manticore.py @@ -18,19 +18,11 @@ from .core.parser import parse from .core.smtlib import solver, Expression, Operators, SolverException, Array, ConstraintSet from core.smtlib import BitVec, Bool from .models import linux, decree, windows -from utils import gdb, qemu - +from .utils.helpers import issymbolic logger = logging.getLogger('MANTICORE') -def issymbolic(value): - ''' - Helper to determine whether a value read from memory is symbolic. - ''' - return isinstance(value, Expression) - - def makeDecree(args): constraints = ConstraintSet() model = decree.SDecree(constraints, ','.join(args.programs)) diff --git a/manticore/models/decree.py b/manticore/models/decree.py index 3b2cdd8..6120742 100644 --- a/manticore/models/decree.py +++ b/manticore/models/decree.py @@ -7,7 +7,7 @@ from ..core.cpu.abstractcpu import Interruption, Syscall, ConcretizeRegister from ..core.memory import SMemory32 from ..core.smtlib import * from ..core.executor import SyscallNotImplemented, ProcessExit, Deadlock, RestartSyscall -logger = logging.getLogger("MODEL") +from ..utils.helpers import issymbolic from ..binary import CGCElf from ..binary import CGCGrr from contextlib import closing @@ -15,6 +15,8 @@ import StringIO import logging import random +logger = logging.getLogger("MODEL") + class SymbolicSyscallArgument(ConcretizeRegister): def __init__(self, number, message='Concretizing syscall argument', policy='SAMPLED'): @@ -615,7 +617,7 @@ class Decree(object): self.sched() self.running.remove(procid) #self.procs[procid] = None #let it there so we can report? - if isinstance(error_code, Expression): + if issymbolic(error_code): logger.info("TERMINATE PROC_%02d with symbolic exit code [%d,%d]", procid, solver.minmax(constraints, error_code)) else: logger.info("TERMINATE PROC_%02d %x", procid, error_code) @@ -948,22 +950,22 @@ class SDecree(Decree): def sys_receive(self, cpu, fd, buf, count, rx_bytes): ''' Symbolic version of Decree.sys_receive ''' - if isinstance(fd, Expression): + if issymbolic(fd): logger.info("Ask to read from a symbolic file descriptor!!") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(0) - if isinstance(buf, Expression): + if issymbolic(buf): logger.info("Ask to read to a symbolic buffer") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(1) - if isinstance(count, Expression): + if issymbolic(count): logger.info("Ask to read a symbolic number of bytes ") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(2) - if isinstance(rx_bytes, Expression): + if issymbolic(rx_bytes): logger.info("Ask to return size to a symbolic address ") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(3) @@ -974,22 +976,22 @@ class SDecree(Decree): def sys_transmit(self, cpu, fd, buf, count, tx_bytes): ''' Symbolic version of Decree.sys_receive ''' - if isinstance(fd, Expression): + if issymbolic(fd): logger.info("Ask to write to a symbolic file descriptor!!") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(0) - if isinstance(buf, Expression): + if issymbolic(buf): logger.info("Ask to write to a symbolic buffer") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(1) - if isinstance(count, Expression): + if issymbolic(count): logger.info("Ask to write a symbolic number of bytes ") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(2) - if isinstance(tx_bytes, Expression): + if issymbolic(tx_bytes): logger.info("Ask to return size to a symbolic address ") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(3) @@ -998,43 +1000,43 @@ class SDecree(Decree): def sys_allocate(self, cpu, length, isX, address_p): - if isinstance(length, Expression): + if issymbolic(length): logger.info("Ask to ALLOCATE a symbolic number of bytes ") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(0) - if isinstance(isX, Expression): + if issymbolic(isX): logger.info("Ask to ALLOCATE potentially executable or not executable memory") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(1) - if isinstance(address_p, Expression): + if issymbolic(address_p): logger.info("Ask to return ALLOCATE result to a symbolic reference ") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(2) return super(SDecree, self).sys_allocate(cpu, length, isX, address_p) def sys_deallocate(self, cpu, addr, size): - if isinstance(addr, Expression): + if issymbolic(addr): logger.info("Ask to DEALLOCATE a symbolic pointer?!") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(0) - if isinstance(size, Expression): + if issymbolic(size): logger.info("Ask to DEALLOCATE a symbolic size?!") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(1) return super(SDecree, self).sys_deallocate(cpu, addr, size) def sys_random(self, cpu, buf, count, rnd_bytes): - if isinstance(buf, Expression): + if issymbolic(buf): logger.info("Ask to write random bytes to a symbolic buffer") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(0) - if isinstance(count, Expression): + if issymbolic(count): logger.info("Ask to read a symbolic number of random bytes ") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(1) - if isinstance(rnd_bytes, Expression): + if issymbolic(rnd_bytes): logger.info("Ask to return rnd size to a symbolic address ") cpu.PC = cpu.PC-cpu.instruction.size raise SymbolicSyscallArgument(2) diff --git a/manticore/models/libc.py b/manticore/models/libc.py index 4eca98d..90c4c20 100644 --- a/manticore/models/libc.py +++ b/manticore/models/libc.py @@ -9,6 +9,7 @@ from ..core.cpu.abstractcpu import Interruption, Syscall, \ ConcretizeMemory from ..core.memory import MemoryException from ..core.executor import ForkState +from ..utils.helpers import issymbolic logger = logging.getLogger("MODEL") @@ -67,7 +68,7 @@ class strings(object): cpu = state.cpu - if isinstance(size, Expression): + if issymbolic(size): single_sol = solver.get_all_values(state.constraints, size, maxcnt=2, silent=True) if len(single_sol) == 1: size = single_sol[0] @@ -87,7 +88,7 @@ class strings(object): def memset(state, dst, char, size): cpu = state.cpu - if isinstance(size, Expression): + if issymbolic(size): single_sol = solver.get_all_values(state.constraints, size, maxcnt=2, silent=True) if len(single_sol) == 1: size = single_sol[0] @@ -108,7 +109,7 @@ class strings(object): count = 0 while True: value = cpu.read_int(src+count, 8) - if isinstance(value, Expression): + if issymbolic(value): if solver.can_be_true(state.constraints, value==0): raise ForkState(value==0) elif value == 0: @@ -126,7 +127,7 @@ class strings(object): value = cpu.read_int(src, 8) if not cpu.mem.isWritable(dst+i): raise MemoryException("No access writing", dst+i) - if isinstance(value, Expression): + if issymbolic(value): if solver.can_be_true(state.constraints, value==0): raise ConcretizeMemory(src+i) else: @@ -142,7 +143,7 @@ class heap(object): @staticmethod def malloc(cpu, size): - if isinstance(size, Expression): + if issymbolic(size): logger.info("malloc(Symbolic Size); concretizing size") raise ConcretizeArgument(0) else: @@ -150,7 +151,7 @@ class heap(object): @staticmethod def realloc(cpu, ptr, size): - if isinstance(size, Expression): + if issymbolic(size): logger.info("realloc({}, Symbolic Size); concretizing size".format(str(ptr))) raise ConcretizeArgument(1) else: @@ -158,11 +159,11 @@ class heap(object): @staticmethod def calloc(cpu, count, size): - if isinstance(size, Expression): + if issymbolic(size): logger.info("calloc({}, Symbolic Size); concretizing size".format(str(count))) raise ConcretizeArgument(1) - if isinstance(count, Expression): + if issymbolic(count): logger.info("calloc(Symbolic count, {}); concretizing count".format(str(size))) raise ConcretizeArgument(0) diff --git a/manticore/models/linux.py b/manticore/models/linux.py index d3e26b0..690701c 100644 --- a/manticore/models/linux.py +++ b/manticore/models/linux.py @@ -2,6 +2,7 @@ import cgcrandom import weakref import sys, os, struct from ..utils import qemu +from ..utils.helpers import issymbolic from ..core.cpu.abstractcpu import Interruption, Syscall, ConcretizeRegister, InvalidPCException from ..core.cpu.cpufactory import CpuFactory from ..core.memory import SMemory32, SMemory64, Memory32, Memory64 @@ -2011,15 +2012,15 @@ class SLinux(Linux): def sys_read(self, cpu, fd, buf, count): ''' Symbolic version of Decree.sys_receive ''' - if isinstance(fd, Expression): + if issymbolic(fd): logger.debug("Ask to read from a symbolic file descriptor!!") raise SymbolicSyscallArgument(0) - if isinstance(buf, Expression): + if issymbolic(buf): logger.debug("Ask to read to a symbolic buffer") raise SymbolicSyscallArgument(1) - if isinstance(count, Expression): + if issymbolic(count): logger.debug("Ask to read a symbolic number of bytes ") raise SymbolicSyscallArgument(2) @@ -2148,15 +2149,15 @@ class SLinux(Linux): def sys_write(self, cpu, fd, buf, count): ''' Symbolic version of Decree.sys_receive ''' - if isinstance(fd, Expression): + if issymbolic(fd): logger.debug("Ask to write to a symbolic file descriptor!!") raise SymbolicSyscallArgument(0) - if isinstance(buf, Expression): + if issymbolic(buf): logger.debug("Ask to write to a symbolic buffer") raise SymbolicSyscallArgument(1) - if isinstance(count, Expression): + if issymbolic(count): logger.debug("Ask to write a symbolic number of bytes ") raise SymbolicSyscallArgument(2) @@ -2164,22 +2165,22 @@ class SLinux(Linux): def sys_allocate(self, cpu, length, isX, address_p): - if isinstance(length, Expression): + if issymbolic(length): logger.debug("Ask to ALLOCATE a symbolic number of bytes ") raise SymbolicSyscallArgument(0) - if isinstance(address_p, Expression): + if issymbolic(address_p): logger.debug("Ask to ALLOCATE potentially executable or not executable memory") raise SymbolicSyscallArgument(1) - if isinstance(address_p, Expression): + if issymbolic(address_p): logger.debug("Ask to return ALLOCATE result to a symbolic reference ") raise SymbolicSyscallArgument(2) return super(SLinux, self).sys_allocate(cpu, length, isX, address_p) def sys_deallocate(self, cpu, addr, size): - if isinstance(addr, Expression): + if issymbolic(addr): logger.debug("Ask to DEALLOCATE a symbolic pointer?!") raise SymbolicSyscallArgument(0) - if isinstance(size, Expression): + if issymbolic(size): logger.debug("Ask to DEALLOCATE a symbolic size?!") raise SymbolicSyscallArgument(1) return super(SLinux, self).sys_deallocate(cpu, addr, size) @@ -2196,15 +2197,15 @@ class DecreeEmu(object): @staticmethod def cgc_random(model, buf, count, rnd_bytes): import cgcrandom - if isinstance(buf, Expression): + if issymbolic(buf): logger.info("Ask to write random bytes to a symbolic buffer") raise ConcretizeArgument(0) - if isinstance(count, Expression): + if issymbolic(count): logger.info("Ask to read a symbolic number of random bytes ") raise ConcretizeArgument(1) - if isinstance(rnd_bytes, Expression): + if issymbolic(rnd_bytes): logger.info("Ask to return rnd size to a symbolic address ") raise ConcretizeArgument(2) diff --git a/manticore/models/windows.py b/manticore/models/windows.py index 595496c..917ebc6 100644 --- a/manticore/models/windows.py +++ b/manticore/models/windows.py @@ -8,6 +8,7 @@ from ..core.cpu.x86 import I386Cpu, Sysenter from ..core.cpu.abstractcpu import Interruption, Syscall, \ ConcretizeRegister, ConcretizeArgument, IgnoreAPI from ..core.executor import ForkState, SyscallNotImplemented +from ..utils.helpers import issymbolic from ..binary.pe import minidump @@ -38,7 +39,7 @@ class SymbolicSyscallArgument(ConcretizeRegister): #FIXME Cosider movnig this to executor.state? def toStr(state, value): - if isinstance(value, Expression): + if issymbolic(value): minmax = solver.get_all_values(state.constraints, value, maxcnt=2, silent=True) if len(minmax) > 1: return '?'*(value.size/8) + ' ' + repr(minmax) @@ -457,7 +458,7 @@ class SWindows(Windows): def readStringFromPointer(state, cpu, ptr, utf16, max_symbols=8): - if isinstance(ptr, Expression): + if issymbolic(ptr): ptrs = solver.get_all_values(state.constraints, ptr, maxcnt=2, silent=True) if len(ptrs) == 1: ptr = ptrs[0] @@ -481,7 +482,7 @@ def readStringFromPointer(state, cpu, ptr, utf16, max_symbols=8): value = cpu.read_int(ptr+i, width) # ooh, a symbolic char - if isinstance(value, Expression): + if issymbolic(value): # how symbolic is it? vals = solver.get_all_values(state.constraints, value, maxcnt=max_symbols, silent=True) if len(vals) == 1: @@ -526,7 +527,7 @@ class ntdll(object): @staticmethod def RtlAllocateHeap(model, handle, flags, size): - if isinstance(size, Expression): + if issymbolic(size): logger.info("RtlAllcoateHeap({}, {}, SymbolicSize); concretizing size".format(str(handle), str(flags)) ) raise ConcretizeArgument(2) else: @@ -577,14 +578,14 @@ class kernel32(object): str(hKey), key_str, str(ulOptions), str(samDesired), str(phkResult))) - if isinstance(phkResult, Expression): + if issymbolic(phkResult): #Check if the symbol has a single solution. values = solver.get_all_values(model.constraints, phkResult, maxcnt=2, silent=True) if len(values) == 1: phkResult = values[0] - if isinstance(phkResult, Expression): + if issymbolic(phkResult): if solver.can_be_true(model.constraints, phkResult==0): raise ForkState(phkResult==0) @@ -640,14 +641,14 @@ class kernel32(object): str(hKey), key_str, str(Reserved), str(lpClass), str(dwOptions), str(lpSecurityAttributes), str(samDesired), str(phkResult), str(lpdwDisposition))) - if isinstance(phkResult, Expression): + if issymbolic(phkResult): #Check if the symbol has a single solution. values = solver.get_all_values(model.constraints, phkResult, maxcnt=2, silent=True) if len(values) == 1: phkResult = values[0] - if isinstance(phkResult, Expression): + if issymbolic(phkResult): if solver.can_be_true(model.constraints, phkResult==0): raise ForkState(phkResult==0) @@ -677,7 +678,7 @@ class kernel32(object): STD_OUTPUT_HANDLE = -11 STD_ERROR_HANDLE = -12 - if isinstance(nStdHandle, Expression): + if issymbolic(nStdHandle): #Check if the symbol has a single solution. values = solver.get_all_values(model.constraints, nStdHandle, maxcnt=2, silent=True) @@ -776,7 +777,7 @@ class kernel32(object): toStr(model, lpOverlapped)) ) - if isinstance(lpNumberOfBytesWritten, Expression): + if issymbolic(lpNumberOfBytesWritten): #Check if the symbol has a single solution. values = solver.get_all_values(model.constraints, lpNumberOfBytesWritten, maxcnt=2, silent=True) @@ -785,7 +786,7 @@ class kernel32(object): lpNumberOfBytesWritten = values[0] cpu = model.current - if isinstance(lpNumberOfBytesWritten, Expression): + if issymbolic(lpNumberOfBytesWritten): if solver.can_be_true(model.constraints, lpNumberOfBytesWritten==0): raise ForkState(lpNumberOfBytesWritten==0) diff --git a/manticore/utils/helpers.py b/manticore/utils/helpers.py new file mode 100644 index 0000000..09e3344 --- /dev/null +++ b/manticore/utils/helpers.py @@ -0,0 +1,9 @@ + +from ..core.smtlib import Expression + +def issymbolic(value): + ''' + Helper to determine whether a value read is symbolic. + ''' + return isinstance(value, Expression) +