DeforaNetworks/manticore
3
0
Fork 0
Code Releases Activity

Use issymbolic() throughout Manticore (#22)

Browse Source 
* Use issymbolic() throughout Manticore

* Add a missed import

* absolute -> relative import

* Import issymbolic from helpers

* Missing import
This commit is contained in:
Yan
2017-02-24 15:56:46 -05:00
committed by Mark Mossberg
parent 103d32c0a7
commit bbc36a2b2e
14 changed files with 112 additions and 98 deletions
Download Patch File Download Diff File Expand all files Collapse all files
manticore/__init__.py
+2 -1
View File
@@ -1 +1,2 @@
from .manticore import Manticore, issymbolic
from .manticore import Manticore
from .utils.helpers import issymbolic
manticore/core/cpu/abstractcpu.py
+5 -4
View File
@@ -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)):
manticore/core/cpu/arm.py
+5 -4
View File
@@ -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
pass
manticore/core/cpu/x86.py
+14 -13
View File
@@ -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<<OperandSize)-1
SIGN_MASK = 1<<(OperandSize-1)
if isinstance(count, Expression):
if issymbolic(count):
cpu.CF = Operators.ITE(count!=0, ((value >> 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
manticore/core/executor.py
+6 -5
View File
@@ -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:
manticore/core/memory.py
+7 -6
View File
@@ -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
page_bit_size = 12
manticore/core/smtlib/operators.py
+3 -2
View File
@@ -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
manticore/core/smtlib/solver.py
+4 -3
View File
@@ -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
manticore/manticore.py
+1 -9
View File
@@ -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))
manticore/models/decree.py
+20 -18
View File
@@ -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)
manticore/models/libc.py
+9 -8
View File
@@ -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)
manticore/models/linux.py
+15 -14
View File
@@ -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)
manticore/models/windows.py
+12 -11
View File
@@ -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)
manticore/utils/helpers.py
+9
View File
@@ -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)