Sanitizers & Probes

Probe mechanism

TritonDSE introduces a probe mechanism. A probe is a class exposing a set of callbacks to register on a given exploration or execution. That enables writing more complex checkers that can be easily registered on a callback manager.

A probe as the following interface:

class ProbeInterface(object):
    """ The Probe interface """
    def __init__(self):
        self._cbs: List[Tuple[CbType, Callable, Optional[str]]] = []

    @property
    def callbacks(self) -> List[Tuple[CbType, Callable, Optional[str]]]:
        return self._cbs

    def _add_callback(self, typ: CbType, callback: Callable, arg: str = None):
        """ Add a callback """
        self._cbs.append((typ, callback, arg))

So to write its own probe one, just have to call _add_callback with its own hooks (usually some other methods). They will automatically be picked by the callback manager and registered.

Using built-in sanitizers

TritonDSE provides few simple sanitizers developped as probes. These sanitizers are the following:

• UAFSanitizer: checks for UaF using the simple built-in allocator (in ProcessState)

• NullDerefSanitizer: checks that no read or write in memory is performed at address 0

• FormatStringSanitizer: hooks various libc functions and checks that format string are not controlled

The registration of a probe can be done as follows:

from tritondse import SymbolicExecutor, Config, Seed, Program, ProcessState, SymbolicExplorator, CoverageStrategy
from tritondse.sanitizers import NullDerefSanitizer

dse = SymbolicExplorator(Config(), Program("crackme_xor"))

dse.callback_manager.register_probe(NullDerefSanitizer())

The probe will now be enabled for all executions.

Writing a sanitizer

For the purpose of this tutorial, let’s write a sanitizer that will checks fopen libc call and its variant freopen cannot be hijacked to open an unwanted file (here /etc/passwd). We are first going to check that the string given in input is controllable and if it is, checking by SMT that it can be the intended string.

from tritondse import ProbeInterface, SymbolicExecutor, ProcessState, CbType, SeedStatus
from tritondse.types import Addr, SolverStatus

class OpenSanitizer(ProbeInterface):

    PASSWD_FILE = "/etc/passwd"

    def __init__(self):
        super(OpenSanitizer, self).__init__()
        self._add_callback(CbType.PRE_RTN, self.fopen_check, 'fopen')
        self._add_callback(CbType.PRE_RTN, self.fopen_check, 'freopen')

    def fopen_check(self, se: SymbolicExecutor, pstate: ProcessState, rtn_name: str, addr: Addr):
        # the filepath is located in arg0 (ptr to a string)
        string_ptr = se.pstate.get_argument_value(0)

        symbolic = True
        cur_ptr = string_ptr
        while pstate.read_memory_int(cur_ptr, 1):        # while different from 0
            if not se.pstate.is_memory_symbolic(cur_ptr, 1): # check that the byte is symbolic
                symbolic = False
            cur_ptr += 1

        # if all memory bytes are symbolic and we have enough place to fit our string
        if symbolic and (cur_ptr - string_ptr) > len(self.PASSWD_FILE):

            # Try to solve by SMT that the filepath string is /etc/passwd
            constraints = [pstate.read_symbolic_memory_byte(string_ptr+i).getAst() == ord(pwd_byte) for i, pwd_byte in enumerate(self.PASSWD_FILE)]
            st, model = pstate.solve(constraints)

            if st == SolverStatus.SAT:                          # if formula satisfiable
                new_seed = se.mk_new_seed_from_model(model)  # create a new input from the model
                new_seed.status = SeedStatus.CRASH           # mark it as crash
                se.enqueue_seed(new_seed)                    # enqueue it *(so that it will put in the workspace..)*

Then we just have to register our new sanitizer!

dse.callback_manager.register_probe(OpenSanitizer())

There are no open in the crackme (but one can try with another example)