Symbolic-length reads from symbolic sockets (#1786)

* Symbolic-length reads from symbolic sockets

* Add native binary test

* Add type hints to recvfrom

Co-authored-by: sschriner <60201678+sschriner@users.noreply.github.com>

* Fixup type hints for recvfrom

* Update SymbolicSocket constraints pointers on fork

Co-authored-by: Eric Hennenfent <eric.hennenfent@trailofbits.com>
Co-authored-by: sschriner <60201678+sschriner@users.noreply.github.com>

manticore/native/state.py

@@ -39,6 +39,19 @@ def __enter__(self) -> "State":
         new_state = super().__enter__()
         new_state._hooks = copy.copy(self._hooks)
         new_state._after_hooks = copy.copy(self._after_hooks)
+
+        # Update constraint pointers in platform objects
+        from ..platforms.linux import SLinux
+
+        if isinstance(new_state.platform, SLinux):
+            from ..platforms.linux import SymbolicSocket
+
+            # Add constraints to symbolic sockets
+            for fd_entry in new_state.platform.fd_table.entries():
+                symb_socket_entry = fd_entry.fdlike
+                if isinstance(symb_socket_entry, SymbolicSocket):
+                    symb_socket_entry._constraints = new_state.constraints
+
         return new_state
 
     def _get_hook_context(

manticore/platforms/linux.py

@@ -27,7 +27,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
@@ -731,14 +731,23 @@ 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__()
         state["inputs_recvd"] = self.inputs_recvd
         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):
@@ -747,10 +756,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:
         """
@@ -764,8 +774,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
@@ -774,9 +783,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
 
 
@@ -2493,6 +2524,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
@@ -2513,18 +2563,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)
@@ -3243,6 +3281,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):
@@ -3286,13 +3326,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:
@@ -3397,34 +3444,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):
@@ -3444,8 +3508,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)

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 <stdio.h>
+#include <stdlib.h>
+#include <netinet/in.h>
+
+#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");
+    }
+}