Merge 8b25940 into 2347b21

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,14 +692,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):
@@ -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)

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");
+    }
+}

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):