feat(handle_t): redef handle_t as pointer

* Add a "HANDLE_TYPE_IS_PTR" compile flag that
redefines handle_t as ptr (instead of int32).

* Create a local copy of storage/ipc.c in trusty_mod directory to allow handle_t to be treated as an opaque object.

* Create a local include dir with trusty_ipc.h for the actual handle_t is ptr redef.

* Run port_create_destroy_harness and msg_buffer_harness with redefined handle_t on
local ipc.c

* Add handle is ptr jobs to CI

Known issues/Needs investigation:

The following issues need to be fixed but not blocking the PR since the infrastructure changes are quite big itself.

* msg_buffer_harness.c fails in vac mode with handle_t as ptr. It seems to be failing at head (added to CI blacklist) so this PR doesn't make the situation worse.

.github/workflows/blacklist.ptr.cex.txt

@@ -0,0 +1,7 @@
+storage_ipc_indirect_handlers_unsat_test
+storage_ipc_msg_buffer_unsat_test
+gatekeeper_ipc_unsat_test
+# following tracked in https://github.com/seahorn/verifyTrusty/issues/18
+storage_ipc_port_create_destroy_unsat_test
+# following tracked in https://github.com/seahorn/verifyTrusty/issues/19
+port_send_msg_pf_unsat_test

.github/workflows/blacklist.ptr.vac.txt

@@ -0,0 +1,3 @@
+storage_ipc_indirect_handlers_unsat_test
+storage_ipc_msg_buffer_unsat_test
+gatekeeper_ipc_unsat_test

.github/workflows/main.yml

@@ -17,23 +17,30 @@ jobs:
         verify_flag: ["", "--vac", "--cex"]
 
     steps:
-      - name: Checkout 
+      - name: Checkout
         uses: actions/checkout@master
-      
+
       - name: Get type
         id: type
         run: echo ::set-output name=type::$(echo ${{ matrix.verify_flag }} | awk '{ print substr($1,3,5) "" substr($2,22) }')
-      
+
       - name: Get exclude test
         id: exclude_files
         run: (test -f ".github/workflows/blacklist.${{steps.type.outputs.type}}.txt" && echo ::set-output name=exclude_files::"($(cut -f 1 ".github/workflows/blacklist.${{steps.type.outputs.type}}.txt" | head -c -1 | tr '\n' '|'))" ) || (echo ::set-output name=exclude_files::" ")
-
-      - name: Docker 
+
+      - name: Get exclude test (for handle-type-is-ptr)
+        id: exclude_files_ptr
+        run: (test -f ".github/workflows/blacklist.ptr.${{steps.type.outputs.type}}.txt" && echo ::set-output name=exclude_files::"($(cut -f 1 ".github/workflows/blacklist.ptr.${{steps.type.outputs.type}}.txt" | head -c -1 | tr '\n' '|'))" ) || (echo ::set-output name=exclude_files::" ")
+
+      - name: Docker
         run: docker build -t verify-trusty . --file docker/seahorn-dev10-verify-trusty.Dockerfile
-      
+
       - name: Get number of Cores
         id: cores
         run: echo "::set-output name=num_cores::$(nproc --all)"
-      
-      - name: Run Tests 
+
+      - name: Run Tests
         run: docker run -t verify-trusty /bin/bash -c "cd build && mkdir -p /tmp/verifyTrusty && env VERIFY_FLAGS=\"${{ matrix.verify_flag }}\" ctest -j ${{steps.cores.outputs.num_cores}} --output-on-failure --timeout 2000 -E \"${{ steps.exclude_files.outputs.exclude_files }}\""
+
+      - name: Run handle-type-is-ptr Tests
+        run: docker run -t verify-trusty /bin/bash -c "cd build_ptr && mkdir -p /tmp/verifyTrusty && env VERIFY_FLAGS=\"${{ matrix.verify_flag }}\" ctest -j ${{steps.cores.outputs.num_cores}} --output-on-failure --timeout 2000 -E \"${{ steps.exclude_files_ptr.outputs.exclude_files }}\""

CMakeLists.txt

@@ -29,9 +29,10 @@ set(LLVMIR_OPT ${SEA_OPT})
 set(CPPSTDLIB "libc++" CACHE STRING "C++ std library to use")
 
 set(TRUSTY_ROOT ${CMAKE_CURRENT_SOURCE_DIR}/trusty)
+set(TRUSTY_MOD_ROOT ${CMAKE_CURRENT_SOURCE_DIR}/trusty_mod)
 set(TRUSTY_TARGET "arm32" CACHE STRING "Trusty target for verification")
 set(EXTERNAL_ROOT ${TRUSTY_ROOT}/external)
-
+option(HANDLE_TYPE_IS_PTR "Build SHADOW MEM versions of jobs" OFF)
 # set C++ stdlib
 string(APPEND CMAKE_CXX_FLAGS " -stdlib=${CPPSTDLIB}")
 
@@ -53,8 +54,14 @@ set(VERIFY_CMD ${CMAKE_CURRENT_BINARY_DIR}/verify)
 include_directories(BEFORE ${CMAKE_CURRENT_BINARY_DIR}/include)
 
 include_directories(seahorn/trusty_common/include)
-include_directories(seahorn/trusty/user/base/lib/libc-trusty)
-
+# TODO: Don't include at global level
+# I don't get why we have two directories trusty_common and trusty
+# and why is trusty included as an implicit dep of trusty_common
+if (HANDLE_TYPE_IS_PTR)
+  include_directories(seahorn/trusty/user/base/lib/libc-trusty-ptr)
+else ()
+  include_directories(seahorn/trusty/user/base/lib/libc-trusty)
+endif ()
 # Include header's directories
 include_directories(${TRUSTY_ROOT}/hardware/libhardware/include)
 include_directories(${TRUSTY_ROOT}/trusty/user/base/interface/storage/include)
@@ -63,7 +70,11 @@ include_directories(${TRUSTY_ROOT}/trusty/user/base/interface/keymaster/include)
 include_directories(${TRUSTY_ROOT}/trusty/user/base/interface/hwkey/include)
 include_directories(${TRUSTY_ROOT}/trusty/user/base/include/uapi)
 include_directories(${TRUSTY_ROOT}/trusty/user/base/include/shared)
-include_directories(${TRUSTY_ROOT}/trusty/user/base/include/user)
+if (HANDLE_TYPE_IS_PTR)
+  include_directories(${TRUSTY_MOD_ROOT}/trusty/user/base/include/user)
+else ()
+  include_directories(${TRUSTY_ROOT}/trusty/user/base/include/user)
+endif ()
 include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/libc-trusty/include)
 include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/libstdc++-trusty/include)
 include_directories(${TRUSTY_ROOT}/trusty/user/base/lib/libcxxabi-trusty/include)

docker/seahorn-dev10-verify-trusty.Dockerfile

@@ -58,5 +58,9 @@ RUN echo "Installing Trusty" && \
 WORKDIR /home/usea/verifyTrusty
 RUN mkdir build && cd build && cmake -DSEA_LINK=llvm-link-10 -DCMAKE_C_COMPILER=clang-10 -DCMAKE_CXX_COMPILER=clang++-10 -DSEAHORN_ROOT=/home/usea/seahorn -DTRUSTY_TARGET=x86_64 ../ -GNinja && cmake --build .
 
+## Also generate jobs using handle_t as ptr
+WORKDIR /home/usea/verifyTrusty
+RUN mkdir build_ptr && cd build_ptr && cmake -DSEA_LINK=llvm-link-10 -DCMAKE_C_COMPILER=clang-10 -DCMAKE_CXX_COMPILER=clang++-10 -DSEAHORN_ROOT=/home/usea/seahorn -DTRUSTY_TARGET=x86_64 -DHANDLE_TYPE_IS_PTR=ON ../ -GNinja && cmake --build .
+
 ## set default user and wait for someone to login and start running verification tasks
 USER usea

seahorn/CMakeLists.txt

@@ -169,20 +169,24 @@ function(sea_attach_bc name)
   target_compile_options(${SOURCE_EXE} PUBLIC -O1 -Xclang -disable-llvm-optzns -S)
   target_compile_options(${SOURCE_EXE} PUBLIC -Wno-macro-redefined)
   target_compile_options(${SOURCE_EXE} PUBLIC -g)
+  target_compile_options(${SOURCE_EXE} PUBLIC -Werror)  # warnings are errors
   target_compile_options(${SOURCE_EXE} PUBLIC -fdeclspec)
   target_compile_options(${SOURCE_EXE} PUBLIC -Wstrict-prototypes -Wwrite-strings)
 
+  #if (HANDLE_TYPE_IS_PTR)
+  #  target_compile_options(${SOURCE_EXE} PUBLIC -m32)  # use 32-bit ptr for x86_64 arch. See https://gcc.gnu.org/onlinedocs/gcc/x86-Options.html.
+  #endif()
   # work-around for Mac
   if (NOT APPLE)
     target_compile_options(${SOURCE_EXE} PUBLIC -target ${TARGET_ARCH}-linux-gnu)
-  endif()
+  endif ()
 
   if (${TRUSTY_TARGET} STREQUAL "arm32")
     target_compile_options(${SOURCE_EXE} PRIVATE -mfloat-abi=softfp
-    -fstack-protector-strong -mthumb
-    )
+      -fstack-protector-strong -mthumb
+      )
     target_compile_definitions(${SOURCE_EXE} PRIVATE __thumb__)
-  elseif(${TRUSTY_TARGET} STREQUAL "x86_64")
+  elseif (${TRUSTY_TARGET} STREQUAL "x86_64")
     target_compile_options(${SOURCE_EXE} PRIVATE -mcmodel=kernel -mno-red-zone -msoft-float
     -fno-pic -ffunction-sections -fdata-sections -fno-stack-protector -fasynchronous-unwind-tables )
   else ()
@@ -265,5 +269,9 @@ add_subdirectory(trusty_common)
 add_subdirectory(trusty)
 
 add_subdirectory(storage)
-add_subdirectory(gatekeeper)
+if (HANDLE_TYPE_IS_PTR)
+  # do nothing for MVP
+else ()
+  add_subdirectory(gatekeeper)
+endif ()
 # add_subdirectory(keymaster)

seahorn/storage/CMakeLists.txt

@@ -1,6 +1,17 @@
 include_directories(include)
+
+add_compile_definitions(CAN_RETURN_INVALID_IPC_HANDLE=1)
+if (HANDLE_TYPE_IS_PTR)
+  set(IPC_SRC ${TRUSTY_MOD_ROOT}/trusty/user/app/storage/ipc.c)
+  add_compile_definitions(HANDLE_TYPE_IS_PTR=1)
+else ()
+  set(IPC_SRC ${TRUSTY_ROOT}/trusty/user/app/storage/ipc.c)
+endif ()
+
 add_subdirectory(lib)
 add_subdirectory(stubs)
+
+# The following jobs will be built
 add_subdirectory(jobs/ipc/indirect_handlers)
 add_subdirectory(jobs/ipc/msg_buffer)
 add_subdirectory(jobs/ipc/port_create_destroy)

seahorn/storage/jobs/ipc/indirect_handlers/CMakeLists.txt

@@ -1,6 +1,7 @@
 add_executable(storage_ipc_indirect_handlers
-  ${TRUSTY_ROOT}/trusty/user/app/storage/ipc.c
+  ${IPC_SRC}
   indirect_handlers_harness.c)
+
 target_include_directories(storage_ipc_indirect_handlers 
   PRIVATE ${TRUSTY_ROOT}/trusty/user/app/storage
   )

seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c

@@ -22,10 +22,9 @@
 
 #include "ipc.h"
 
-#include "handle_table.h"
+#include <sea_handle_table.h>
 #include "seahorn/seahorn.h"
 #include "sea_ipc_helper.h"
-#define assert sassert
 
 #include "tipc_limits.h"
 #include <interface/storage/storage.h>
@@ -34,16 +33,19 @@
    entry point
 */
 int main(void) {
-  // handle_table_init(INVALID_IPC_HANDLE, INVALID_IPC_HANDLE, INVALID_IPC_HANDLE);
-  struct ipc_port_context* ctx = create_port_context();
+  // handle_table_init(INVALID_IPC_HANDLE, INVALID_IPC_HANDLE,
+  // INVALID_IPC_HANDLE);
+  struct ipc_port_context *ctx = create_port_context();
   int rc =
       ipc_port_create(ctx, STORAGE_DISK_PROXY_PORT, 1, STORAGE_MAX_BUFFER_SIZE,
                       IPC_PORT_ALLOW_TA_CONNECT | IPC_PORT_ALLOW_NS_CONNECT);
 
   if (rc < 0) {
     return rc;
   }
-
+#if HANDLE_TYPE_IS_PTR
+  on_waitany_return(ctx->common.handle);
+#endif
   ipc_loop();
 
   ipc_port_destroy(ctx);

seahorn/storage/jobs/ipc/msg_buffer/CMakeLists.txt

@@ -1,6 +1,7 @@
 add_executable(storage_ipc_msg_buffer
-  ${TRUSTY_ROOT}/trusty/user/app/storage/ipc.c
+  ${IPC_SRC}
   msg_buffer_harness.c)
+
 target_include_directories(storage_ipc_msg_buffer 
   PRIVATE ${TRUSTY_ROOT}/trusty/user/app/storage
   )

seahorn/storage/jobs/ipc/msg_buffer/msg_buffer_harness.c

@@ -10,7 +10,7 @@
 #include "tipc_limits.h"
 #include <interface/storage/storage.h>
 
-#include "handle_table.h"
+#include <sea_handle_table.h>
 #include "seahorn/seahorn.h"
 #include "sea_ipc_helper.h"
 
@@ -30,7 +30,9 @@ int main(void) {
   if (rc < 0) {
     return rc;
   }
-
+#if HANDLE_TYPE_IS_PTR
+  on_waitany_return(ctx.common.handle);
+#endif
   ipc_loop();
 
   ipc_port_destroy(&ctx);

seahorn/storage/jobs/ipc/port_create_destroy/CMakeLists.txt

@@ -1,7 +1,11 @@
+# We verify a modified copy of ipc.c since the original
+# casts between a handle_t and int.
+# This breaks the original spec that handle_t is a 32-bit opaque number
+# and hence breaks our impl of type(handle_t) == 32 bit pointer.
 add_executable(storage_ipc_port_create_destroy
-  ${TRUSTY_ROOT}/trusty/user/app/storage/ipc.c
+  ${IPC_SRC}
   port_create_destroy_harness.c)
-target_include_directories(storage_ipc_port_create_destroy 
+target_include_directories(storage_ipc_port_create_destroy
   PRIVATE ${TRUSTY_ROOT}/trusty/user/app/storage
   )
 sea_link_libraries(storage_ipc_port_create_destroy sea_storage_ipc_proofs.ir)

seahorn/storage/lib/sea_ipc_helper.c

@@ -45,25 +45,26 @@ static int sea_ipc_msg_handler(struct ipc_channel_context *context, void *msg,
 
 static int sync_ipc_msg_handler(struct ipc_channel_context *context, void *msg,
                                size_t msg_size) {
-    uint8_t* snd_buf = malloc(sizeof(msg_size));
-    uint8_t* recv_buf = malloc(sizeof(msg_size));
-    struct iovec tx_iov = {
-            .iov_base = snd_buf,
-            .iov_len = msg_size,
-    };
-    struct iovec rx_iov = {
-            .iov_base = recv_buf,
-            .iov_len = msg_size,
-    };
-
-    handle_t rc = sync_ipc_send_msg(context->common.handle, &tx_iov, 1, &rx_iov, 1);
-
-    if (rc < 0)
-      return rc;
-
-    if (rc > 0) sassert(rc == msg_size);
+  uint8_t *snd_buf = malloc(sizeof(msg_size));
+  uint8_t *recv_buf = malloc(sizeof(msg_size));
+  struct iovec tx_iov = {
+      .iov_base = snd_buf,
+      .iov_len = msg_size,
+  };
+  struct iovec rx_iov = {
+      .iov_base = recv_buf,
+      .iov_len = msg_size,
+  };
+
+  int rc = sync_ipc_send_msg(context->common.handle, &tx_iov, 1, &rx_iov, 1);
 
-    return NO_ERROR;
+  if (rc < 0)
+    return rc;
+
+  if (rc > 0)
+    sassert(rc == msg_size);
+
+  return NO_ERROR;
 }
 
 /*

seahorn/trusty/CMakeLists.txt

@@ -1 +1 @@
-add_subdirectory(user/base/lib/libc-trusty)
+add_subdirectory(user/base/lib)

seahorn/trusty/user/base/lib/CMakeLists.txt

@@ -0,0 +1,12 @@
+set(EXTERNAL ${TRUSTY_ROOT}/trusty/user/base/lib/libc-trusty)
+add_library(
+  sea_libc_trusty
+  ${EXTERNAL}/ipc.c
+)
+
+if (HANDLE_TYPE_IS_PTR)
+  add_subdirectory(libc-trusty-ptr)
+else ()
+  add_subdirectory(libc-trusty)
+endif ()
+add_compile_definitions(CAN_RETURN_INVALID_IPC_HANDLE=0)

seahorn/trusty/user/base/lib/libc-trusty-ptr/CMakeLists.txt

@@ -0,0 +1,10 @@
+target_sources(sea_libc_trusty PUBLIC
+  sea_handle_table.c
+  trusty_syscalls_impl.c
+  )
+
+target_include_directories(sea_libc_trusty PUBLIC ${CMAKE_CURRENT_SOURCE_DIR})
+
+sea_attach_bc(sea_libc_trusty)
+
+add_subdirectory(proof)

seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/CMakeLists.txt

@@ -0,0 +1,11 @@
+add_subdirectory(port_create)
+add_subdirectory(port_close)
+add_subdirectory(port_connect)
+add_subdirectory(port_accept)
+add_subdirectory(port_get_msg)
+add_subdirectory(port_put_msg)
+add_subdirectory(port_read_msg)
+add_subdirectory(port_send_msg)
+add_subdirectory(port_wait)
+add_subdirectory(port_wait_any)
+add_subdirectory(port_set_cookie)

seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_accept/CMakeLists.txt

@@ -0,0 +1,5 @@
+add_executable(port_accept_pf main.c)
+sea_link_libraries(port_accept_pf sea_libc_trusty.ir)
+
+sea_attach_bc(port_accept_pf)
+sea_add_unsat_test(port_accept_pf)

seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_accept/main.c

@@ -0,0 +1,53 @@
+#include "trusty_ipc.h"
+#include <seahorn/seahorn.h>
+
+/* Documentation from trusty API:
+  accept()
+Accepts an incoming connection and gets a handle to a channel.
+
+long accept(uint32_t handle_id, uuid_t *peer_uuid);
+[in] handle_id: Handle representing the port to which a client has connected
+[out] peer_uuid: Pointer to a uuud_t structure to be filled with the UUID of
+  the connecting client application. It will be set to all zeros if the
+  connection originated from the non-secure world.
+
+[retval]: Handle to a channel (if non-negative) on which the server can exchange
+  messages with the client (or an error code otherwise)
+*/
+
+const char *HANDLE_PATH = "seahorn.com";
+
+bool is_uuid_all_zeros(uuid_t *peer_uuid) {
+  return peer_uuid->time_low == 0 && peer_uuid->time_mid == 0 &&
+         peer_uuid->time_hi_and_version == 0;
+}
+
+int main(void) {
+
+  handle_t port;
+  int rc;
+
+  port = port_create(HANDLE_PATH, 1, 100,
+                     IPC_PORT_ALLOW_NS_CONNECT | IPC_PORT_ALLOW_TA_CONNECT);
+
+  // -- got expected handle
+  sassert(!port->secure);
+
+  uuid_t peer_uuid;
+  handle_t chan;
+  chan = accept(port, &peer_uuid);
+  assume(chan != INVALID_IPC_HANDLE);
+  sassert(is_uuid_all_zeros(&peer_uuid));
+
+  rc = close(port);
+  sassert(rc == 0);
+
+  port = port_create(HANDLE_PATH, 1, 100, IPC_PORT_ALLOW_NS_CONNECT);
+
+  // -- expected secure handle handle
+  sassert(port->secure);
+
+  chan = accept(port, &peer_uuid);
+  assume(chan != INVALID_IPC_HANDLE);
+  return 0;
+}