diff --git a/manticore/platforms/linux.py b/manticore/platforms/linux.py index bc2e88f016..68d4badb09 100644 --- a/manticore/platforms/linux.py +++ b/manticore/platforms/linux.py @@ -25,7 +25,7 @@ from . import linux_syscalls from .linux_syscall_stubs import SyscallStubs -from ..core.state import TerminateState +from ..core.state import TerminateState, Concretize from ..core.smtlib import ConstraintSet, Operators, Expression, issymbolic, ArrayProxy from ..core.smtlib.solver import SelectedSolver from ..exceptions import SolverError @@ -692,6 +692,14 @@ def __init__( # Keep track of the symbolic inputs we create self.inputs_recvd: List[ArrayProxy] = [] self.recv_pos = 0 + # This is a meta-variable, of sorts, and it is responsible for + # determining the symbolic length of the array during recv/read. + # Initially, it is None, to indicate we haven't forked yet. After + # fork, each state will be assigned their respective _actual_, + # concretized, receive length + self._symb_len: Optional[int] = None + # Set after adding this socket to the file descriptor list + self.fd: Optional[int] = None def __getstate__(self): state = super().__getstate__() @@ -699,7 +707,8 @@ def __getstate__(self): state["symb_name"] = self.symb_name state["recv_pos"] = self.recv_pos state["max_recv_symbolic"] = self.max_recv_symbolic - state["constraints"] = self._constraints + state["_symb_len"] = self._symb_len + state["fd"] = self.fd return state def __setstate__(self, state): @@ -708,10 +717,11 @@ def __setstate__(self, state): self.symb_name = state["symb_name"] self.recv_pos = state["recv_pos"] self.max_recv_symbolic = state["max_recv_symbolic"] - self._constraints = state["constraints"] + self._symb_len = state["_symb_len"] + self.fd = state["fd"] def __repr__(self): - return f"SymbolicSocket({hash(self):x}, inputs_recvd={self.inputs_recvd}, buffer={self.buffer}, net={self.net}" + return f"SymbolicSocket({hash(self):x}, fd={self.fd}, inputs_recvd={self.inputs_recvd}, buffer={self.buffer}, net={self.net}" def _next_symb_name(self) -> str: """ @@ -725,8 +735,7 @@ def receive(self, size: int) -> Union[ArrayProxy, List[bytes]]: :param size: Size of receive :return: Symbolic array or list of concrete bytes """ - # NOTE: self.buffer isn't used at all for SymbolicSocket. Not sure if there is a better - # way to use it for on-demand generation of symbolic data or not. + # First, get our max valid rx_bytes size rx_bytes = ( size if self.max_recv_symbolic == 0 @@ -735,9 +744,31 @@ def receive(self, size: int) -> Union[ArrayProxy, List[bytes]]: if rx_bytes == 0: # If no symbolic bytes left, return empty list return [] - ret = self._constraints.new_array(name=self._next_symb_name(), index_max=rx_bytes) - self.recv_pos += rx_bytes + # Then do some forking with self._symb_len + if self._symb_len is None: + self._symb_len = self._constraints.new_bitvec( + 8, "_socket_symb_len", avoid_collisions=True + ) + self._constraints.add(Operators.AND(self._symb_len >= 1, self._symb_len <= rx_bytes)) + + def setstate(state: State, value): + state.platform.fd_table.get_fdlike(self.fd)._symb_len = value + + logger.debug("Raising concretize in SymbolicSocket receive") + raise Concretize( + "Returning symbolic amount of data to SymbolicSocket", + self._symb_len, + setstate=setstate, + policy="MINMAX", + ) + ret = self._constraints.new_array( + name=self._next_symb_name(), index_max=self._symb_len, avoid_collisions=True + ) + logger.info(f"Setting recv symbolic length to {self._symb_len}") + self.recv_pos += self._symb_len self.inputs_recvd.append(ret) + # Reset _symb_len for next recv + self._symb_len = None return ret @@ -2454,6 +2485,25 @@ def sys_accept4(self, sockfd: int, addr, addrlen, flags) -> int: return fd def sys_recv(self, sockfd: int, buf: int, count: int, flags: int, trace_str="_recv") -> int: + # act like sys_recvfrom + return self.sys_recvfrom(sockfd, buf, count, flags, 0, 0, trace_str=trace_str) + + def sys_recvfrom( + self, + sockfd: int, + buf: int, + count: int, + flags: int, + src_addr: int, + addrlen: int, + trace_str="_recvfrom", + ) -> int: + if src_addr != 0: + logger.warning("sys_recvfrom: Unimplemented non-NULL src_addr") + + if addrlen != 0: + logger.warning("sys_recvfrom: Unimplemented non-NULL addrlen") + if not self.current.memory.access_ok(slice(buf, buf + count), "w"): logger.info("RECV: buf within invalid memory. Returning -errno.EFAULT") return -errno.EFAULT @@ -2474,18 +2524,6 @@ def sys_recv(self, sockfd: int, buf: int, count: int, flags: int, trace_str="_re return len(data) - def sys_recvfrom( - self, sockfd: int, buf: int, count: int, flags: int, src_addr: int, addrlen: int - ) -> int: - if src_addr != 0: - logger.warning("sys_recvfrom: Unimplemented non-NULL src_addr") - - if addrlen != 0: - logger.warning("sys_recvfrom: Unimplemented non-NULL addrlen") - - # TODO Unimplemented src_addr and addrlen, so act like sys_recv - return self.sys_recv(sockfd, buf, count, flags, trace_str="_recvfrom") - def sys_send(self, sockfd, buf, count, flags) -> int: try: sock = self.fd_table.get_fdlike(sockfd) @@ -3183,6 +3221,8 @@ def __init__( self._pure_symbolic = pure_symbolic self.random = 0 self.symbolic_files = symbolic_files + # Keep track of number of accepted symbolic sockets + self.net_accepts = 0 super().__init__(programs, argv=argv, envp=envp, disasm=disasm) def _mk_proc(self, arch): @@ -3226,13 +3266,20 @@ def __getstate__(self): state["constraints"] = self.constraints state["random"] = self.random state["symbolic_files"] = self.symbolic_files + state["net_accepts"] = self.net_accepts return state def __setstate__(self, state): self._constraints = state["constraints"] self.random = state["random"] self.symbolic_files = state["symbolic_files"] + self.net_accepts = state["net_accepts"] super().__setstate__(state) + # Add constraints to symbolic sockets + for fd_entry in self.fd_table.entries(): + symb_socket_entry = fd_entry.fdlike + if isinstance(symb_socket_entry, SymbolicSocket): + symb_socket_entry._constraints = self._constraints def _sys_open_get_file(self, filename: str, flags: int) -> FdLike: if filename in self.symbolic_files: @@ -3316,34 +3363,51 @@ def sys_recv(self, sockfd, buf, count, flags, trace_str="_recv"): logger.debug("Submitted a symbolic flags") raise ConcretizeArgument(self, 3) - return super().sys_recv(sockfd, buf, count, flags) + return self.sys_recvfrom(sockfd, buf, count, flags, 0, 0, trace_str) - def sys_recvfrom(self, sockfd, buf, count, flags, src_addr, addrlen): + def sys_recvfrom( + self, + sockfd: Union[int, Expression], + buf: Union[int, Expression], + count: Union[int, Expression], + flags: Union[int, Expression], + src_addr: Union[int, Expression], + addrlen: Union[int, Expression], + trace_str: str = "_recvfrom", + ): if issymbolic(sockfd): - logger.debug("Ask to read from a symbolic file descriptor!!") + logger.debug("Ask to recvfrom a symbolic file descriptor!!") raise ConcretizeArgument(self, 0) if issymbolic(buf): - logger.debug("Ask to read to a symbolic buffer") + logger.debug("Ask to recvfrom to a symbolic buffer") raise ConcretizeArgument(self, 1) if issymbolic(count): - logger.debug("Ask to read a symbolic number of bytes ") + logger.debug("Ask to recvfrom a symbolic number of bytes ") raise ConcretizeArgument(self, 2) if issymbolic(flags): - logger.debug("Submitted a symbolic flags") + logger.debug("Ask to recvfrom with symbolic flags") raise ConcretizeArgument(self, 3) if issymbolic(src_addr): - logger.debug("Submitted a symbolic source address") + logger.debug("Ask to recvfrom with symbolic source address") raise ConcretizeArgument(self, 4) if issymbolic(addrlen): - logger.debug("Submitted a symbolic address length") + logger.debug("Ask to recvfrom with symbolic address length") raise ConcretizeArgument(self, 5) - return super().sys_recvfrom(sockfd, buf, count, flags, src_addr, addrlen) + # mypy doesn't know issymbolic works like `isinstance` + assert isinstance(sockfd, int) + assert isinstance(buf, int) + assert isinstance(count, int) + assert isinstance(flags, int) + assert isinstance(src_addr, int) + assert isinstance(addrlen, int) + + return super().sys_recvfrom(sockfd, buf, count, flags, src_addr, addrlen, trace_str) def sys_accept(self, sockfd, addr, addrlen): if issymbolic(sockfd): @@ -3363,8 +3427,10 @@ def sys_accept(self, sockfd, addr, addrlen): return ret # TODO: maybe combine name with addr? - sock = SymbolicSocket(self.constraints, "SymbSocket", net=True) + sock = SymbolicSocket(self.constraints, f"SymbSocket_{self.net_accepts}", net=True) + self.net_accepts += 1 fd = self._open(sock) + sock.fd = fd return fd # TODO: Make a concrete connection actually an option # return super().sys_accept(sockfd, addr, addrlen) diff --git a/tests/native/binaries/symbolic_length_recv b/tests/native/binaries/symbolic_length_recv new file mode 100755 index 0000000000..88408962a1 Binary files /dev/null and b/tests/native/binaries/symbolic_length_recv differ diff --git a/tests/native/binaries/symbolic_length_recv.c b/tests/native/binaries/symbolic_length_recv.c new file mode 100644 index 0000000000..cea15ade55 --- /dev/null +++ b/tests/native/binaries/symbolic_length_recv.c @@ -0,0 +1,39 @@ +// Compiled on Ubuntu 18.04 Manticore Docker image with +// gcc -static symbolic_read_count.c -o symbolic_read_count + +#include +#include +#include + +#define PORT 8081 +#define BUFFER_SIZE 4 + +int main() { + int server_fd, new_client; + struct sockaddr_in address; + + // create socket file descriptor, attach to 8081 + int opt = 1; // Reuse address + server_fd = socket(AF_INET, SOCK_STREAM, 0); + if (setsockopt(server_fd, SOL_SOCKET, SO_REUSEADDR | SO_REUSEPORT, &opt, sizeof(opt))) + return -1; + address.sin_family = AF_INET; + address.sin_addr.s_addr = INADDR_ANY; + address.sin_port = htons(PORT); + if (bind(server_fd, (struct sockaddr *)&address, sizeof(address))) + return -1; + + printf("Listening on port %i...\n", PORT); + + + char buffer[BUFFER_SIZE]; + + int addrlen = sizeof(address); + listen(server_fd, 10); + new_client = accept(server_fd, (struct sockaddr *)&address, (socklen_t *)&addrlen); + + ssize_t num_rcv = recv(new_client, buffer, BUFFER_SIZE, 0); + if (num_rcv < BUFFER_SIZE) { + printf("Received less than BUFFER_SIZE\n"); + } +} diff --git a/tests/native/test_syscalls.py b/tests/native/test_syscalls.py index d5e96091a0..b46ee81b50 100644 --- a/tests/native/test_syscalls.py +++ b/tests/native/test_syscalls.py @@ -11,6 +11,8 @@ import re from glob import glob +from manticore.core.smtlib import Solver +from manticore.core.state import Concretize from manticore.native import Manticore from manticore.platforms import linux, linux_syscall_stubs @@ -39,6 +41,27 @@ def test_symbolic_syscall_arg() -> None: assert found_win_msg, f'Did not find win message in {outs_glob}: "{win_msg}"' +def test_symbolic_length_recv() -> None: + BIN_PATH = os.path.join(os.path.dirname(__file__), "binaries", "symbolic_length_recv") + tmp_dir = tempfile.TemporaryDirectory(prefix="mcore_test_") + m = Manticore(BIN_PATH, workspace_url=str(tmp_dir.name)) + + m.run() + m.finalize() + + found_msg = False + less_len_msg = "Received less than BUFFER_SIZE" + outs_glob = f"{str(m.workspace)}/test_*.stdout" + # Search all output messages + for output_p in glob(outs_glob): + with open(output_p) as f: + if less_len_msg in f.read(): + found_msg = True + break + + assert found_msg, f'Did not find our message in {outs_glob}: "{less_len_msg}"' + + class LinuxTest(unittest.TestCase): _multiprocess_can_split_ = True BIN_PATH = os.path.join(os.path.dirname(__file__), "binaries", "basic_linux_amd64") @@ -195,28 +218,38 @@ def test_read_symb_socket(self): # Try to receive 5 symbolic bytes BYTES = 5 + # Need to set this so we don't fork in our tests + sock_obj._symb_len = BYTES wrote = self.linux.sys_read(conn_fd, 0x1100, BYTES) self.assertEqual(wrote, BYTES) # Try to receive into address 0x0 - wrote = self.linux.sys_read(conn_fd, 0x0, 100) + BYTES = 100 + sock_obj._symb_len = BYTES + wrote = self.linux.sys_read(conn_fd, 0x0, BYTES) self.assertEqual(wrote, -errno.EFAULT) # Try to receive all remaining symbolic bytes plus some more - recvd_bytes = sock_obj.recv_pos remaining_bytes = sock_obj.max_recv_symbolic - sock_obj.recv_pos BYTES = remaining_bytes + 10 + # Needs to be remaining_bytes so that we can simulate overread + sock_obj._symb_len = remaining_bytes wrote = self.linux.sys_read(conn_fd, 0x1100, BYTES) self.assertNotEqual(wrote, BYTES) self.assertEqual(wrote, remaining_bytes) # Try to receive 10 more bytes when already at max - wrote = self.linux.sys_read(conn_fd, 0x1100, 10) + BYTES = 10 + # Needs to be 0 so that we can simulate overread + sock_obj._symb_len = 0 + wrote = self.linux.sys_read(conn_fd, 0x1100, BYTES) self.assertEqual(wrote, 0) # Close and make sure we can't write more stuff + BYTES = 10 + sock_obj._symb_len = BYTES self.linux.sys_close(conn_fd) - wrote = self.linux.sys_read(conn_fd, 0x1100, 10) + wrote = self.linux.sys_read(conn_fd, 0x1100, BYTES) self.assertEqual(wrote, -errno.EBADF) def test_recvfrom_symb_socket(self): @@ -242,6 +275,8 @@ def test_recvfrom_symb_socket(self): # Try to receive 5 symbolic bytes BYTES = 5 + # Need to set this so we don't fork in our tests + sock_obj._symb_len = BYTES wrote = self.linux.sys_recvfrom(conn_fd, 0x1100, BYTES, 0x0, 0x0, 0x0) self.assertEqual(wrote, BYTES) @@ -250,20 +285,26 @@ def test_recvfrom_symb_socket(self): self.assertEqual(wrote, -errno.EFAULT) # Try to receive all remaining symbolic bytes plus some more - recvd_bytes = sock_obj.recv_pos remaining_bytes = sock_obj.max_recv_symbolic - sock_obj.recv_pos BYTES = remaining_bytes + 10 + # Needs to be remaining_bytes so that we can simulate overread + sock_obj._symb_len = remaining_bytes wrote = self.linux.sys_recvfrom(conn_fd, 0x1100, BYTES, 0x0, 0x0, 0x0) self.assertNotEqual(wrote, BYTES) self.assertEqual(wrote, remaining_bytes) # Try to receive 10 more bytes when already at max - wrote = self.linux.sys_recvfrom(conn_fd, 0x1100, 10, 0x0, 0x0, 0x0) + BYTES = 10 + # Needs to be 0 so that we can simulate overread + sock_obj._symb_len = 0 + wrote = self.linux.sys_recvfrom(conn_fd, 0x1100, BYTES, 0x0, 0x0, 0x0) self.assertEqual(wrote, 0) # Close and make sure we can't write more stuff self.linux.sys_close(conn_fd) - wrote = self.linux.sys_recvfrom(conn_fd, 0x1100, 10, 0x0, 0x0, 0x0) + BYTES = 10 + sock_obj._symb_len = 0 + wrote = self.linux.sys_recvfrom(conn_fd, 0x1100, BYTES, 0x0, 0x0, 0x0) self.assertEqual(wrote, -errno.EBADF) def test_multiple_sockets(self):