diff --git a/docs/gotchas.rst b/docs/gotchas.rst index 6dc0744..57a2de8 100644 --- a/docs/gotchas.rst +++ b/docs/gotchas.rst @@ -30,7 +30,14 @@ Client code should use the :meth:`~manticore.Manticore.locked_context` API:: global_context['flag1'] += ['a'] global_context['flag2'] += ['b'] + "Random" Policy --------------- The `random` policy, which is the manticore default, is not actually random and is instead deterministically seeded. This means that running the same analysis twice should return the same results (and get stuck in the same places). + + +Symbolic Socket Support +----------------------- + +The current implementation of the socket family of system calls is very barebones and is deemed to be experimental. All created sockets are assumed to contain 64 bytes of symbolic input. diff --git a/examples/linux/basic.c b/examples/linux/basic.c index fb48c1e..9bb323b 100644 --- a/examples/linux/basic.c +++ b/examples/linux/basic.c @@ -35,6 +35,7 @@ #include #include +#include int main(int argc, char* argv[], char* envp[]){ unsigned int cmd; diff --git a/manticore/core/workspace.py b/manticore/core/workspace.py index fb0d856..925563a 100644 --- a/manticore/core/workspace.py +++ b/manticore/core/workspace.py @@ -526,18 +526,25 @@ class ManticoreOutput(object): f.write(repr(state.platform.syscall_trace)) def save_fds(self, state): + def solve_to_fd(data, fd): + try: + for c in data: + fd.write(chr(solver.get_value(state.constraints, c))) + except SolverException: + fd.write('{SolverException}') + with self._named_stream('stdout') as _out: with self._named_stream('stdout') as _err: with self._named_stream('stdin') as _in: - for name, fd, data in state.platform.syscall_trace: - if name in ('_transmit', '_write'): - if fd == 1: - _out.write(''.join(str(c) for c in data)) - elif fd == 2: - _err.write(''.join(str(c) for c in data)) - if name in ('_receive', '_read') and fd == 0: - try: - for c in data: - _in.write(chr(solver.get_value(state.constraints, c))) - except SolverException: - _in.write('{SolverException}') + with self._named_stream('net') as _net: + for name, fd, data in state.platform.syscall_trace: + s = ''.join(str(c) for c in data) + if name in ('_transmit', '_write'): + if fd == 1: + _out.write(s) + elif fd == 2: + _err.write(s) + if name in ('_recv'): + solve_to_fd(data, _net) + if name in ('_receive', '_read') and fd == 0: + solve_to_fd(data, _in) diff --git a/manticore/manticore.py b/manticore/manticore.py index 89c4b39..b4627ad 100644 --- a/manticore/manticore.py +++ b/manticore/manticore.py @@ -543,10 +543,10 @@ class Manticore(object): self._assertions[pc] = ' '.join(line.split(' ')[1:]) def _store_state_callback(self, state, state_id): - logger.debug("store state %r", state_id) + logger.info("store state %r", state_id) def _load_state_callback(self, state, state_id): - logger.debug("load state %r", state_id) + logger.info("load state %r", state_id) def _terminate_state_callback(self, state, state_id, ex): #aggregates state statistics into exceutor statistics. FIXME split diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index 9170462..bb062b4 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -5,6 +5,7 @@ import os import random import struct import ctypes +import socket #Remove in favor of binary.py from elftools.elf.elffile import ELFFile @@ -213,6 +214,17 @@ class SymbolicFile(File): for i in xrange(self.pos, self.pos + size): self.array[i] = data[i - self.pos] + +class SocketDesc(object): + ''' + Represents a socket descriptor (i.e. value returned by socket(2) + ''' + def __init__(self, domain=None, socket_type=None, protocol=None): + self.domain = domain + self.socket_type = socket_type + self.protocol = protocol + + class Socket(object): def stat(self): from collections import namedtuple @@ -1657,6 +1669,99 @@ class Linux(Platform): logger.debug("sys_gettimeofday(%x, %x) -> 0", tv, tz) return 0 + def sys_socket(self, domain, socket_type, protocol): + if domain != socket.AF_INET: + return -errno.EINVAL + + if socket_type != socket.SOCK_STREAM: + return -errno.EINVAL + + if protocol != 0: + return -errno.EINVAL + + f = SocketDesc(domain, socket_type, protocol) + fd = self._open(f) + logger.debug("socket(%d, %d, %d) -> %d", domain, socket_type, protocol, fd) + return fd + + def _is_sockfd(self, sockfd): + try: + fd = self.files[sockfd] + if not isinstance(fd, SocketDesc): + return -errno.ENOTSOCK + return 0 + except IndexError: + return -errno.EBADF + + def sys_bind(self, sockfd, address, address_len): + logger.debug("bind(%d, %x, %d)", sockfd, address, address_len) + return self._is_sockfd(sockfd) + + def sys_listen(self, sockfd, backlog): + logger.debug("listen(%d, %d)", sockfd, backlog) + return self._is_sockfd(sockfd) + + def sys_accept(self, sockfd, addr, addrlen, flags): + ret = self._is_sockfd(sockfd) + if ret != 0: + return ret + + sock = Socket() + fd = self._open(sock) + logger.debug('accept(%d, %x, %d, %d) -> %d', sockfd, addr, addrlen, flags, fd) + return fd + + def sys_recv(self, sockfd, buf, count, flags): + try: + sock = self.files[sockfd] + except IndexError: + return -errno.EINVAL + + if not isinstance(sock, Socket): + return -errno.ENOTSOCK + + data = sock.read(count) + self.current.write_bytes(buf, data) + self.syscall_trace.append(("_recv", sockfd, data)) + + logger.debug("recv(%d, 0x%08x, %d, 0x%08x) -> <%s> (size:%d)", + sockfd, buf, count, len(data), repr(data)[:min(count,32)], + len(data)) + + return len(data) + + + def sys_send(self, sockfd, buf, count, flags): + try: + sock = self.files[sockfd] + except IndexError: + return -errno.EINVAL + + if not isinstance(sock, Socket): + return -errno.ENOTSOCK + + data = self.current.read_bytes(buf, count) + #XXX(yan): send(2) is currently a nop; we don't communicate yet + self.syscall_trace.append(("_send", sockfd, data)) + + return count + + def sys_sendfile(self, out_fd, in_fd, offset_p, count): + if offset_p != 0: + offset = self.current.read_int(offset_p, self.count.address_bit_size) + else: + offset = 0 + + try: + out_sock = self.files[out_fd] + in_sock = self.files[in_fd] + except IndexError: + return -errno.EINVAL + + #XXX(yan): sendfile(2) is currently a nop; we don't communicate yet + + return count + #Distpatchers... def syscall(self): ''' @@ -2143,3 +2248,64 @@ class SLinux(Linux): raise ConcretizeArgument(self, 2) return super(SLinux, self).sys_write(fd, buf, count) + + def sys_recv(self, sockfd, buf, count, flags): + if issymbolic(sockfd): + logger.debug("Ask to read from a symbolic file descriptor!!") + raise ConcretizeArgument(self, 0) + + if issymbolic(buf): + logger.debug("Ask to read to a symbolic buffer") + raise ConcretizeArgument(self, 1) + + if issymbolic(count): + logger.debug("Ask to read a symbolic number of bytes ") + raise ConcretizeArgument(self, 2) + + if issymbolic(flags): + logger.debug("Submitted a symbolic flags") + raise ConcretizeArgument(self, 3) + + return super(SLinux, self).sys_recv(sockfd, buf, count, flags) + + def sys_accept(self, sockfd, addr, addrlen, flags): + #TODO(yan): Transmit some symbolic bytes as soon as we start. + # Remove this hack once no longer needed. + + fd = super(SLinux, self).sys_accept(sockfd, addr, addrlen, flags) + if fd < 0: + return fd + sock = self._get_fd(fd) + nbytes = 32 + symb = self.constraints.new_array(name='socket', index_max=nbytes) + for i in range(nbytes): + sock.buffer.append(symb[i]) + return fd + + def sys_open(self, buf, flags, mode): + ''' + A version of open(2) that includes a special case for a symbolic path. + When given a symbolic path, it will create a temporary file with + 64 bytes of symbolic bytes as contents and return that instead. + + :param buf: address of zero-terminated pathname + :param flags: file access bits + :param mode: file permission mode + ''' + offset = 0 + symbolic_path = issymbolic(self.current.read_int(buf, 8)) + if symbolic_path: + import tempfile + fd, path = tempfile.mkstemp() + with open(path, 'wb+') as f: + f.write('+'*64) + self.symbolic_files.append(path) + buf = self.current.memory.mmap(None, 1024, 'rw ', data_init=path) + + rv = super(SLinux, self).sys_open(buf, flags, mode) + + if symbolic_path: + self.current.memory.munmap(buf, 1024) + + return rv +