From 04ccba863cca4924f36704491bde7bf474a411ff Mon Sep 17 00:00:00 2001 From: Siddharth Priya Date: Tue, 19 Jul 2022 14:24:45 -0400 Subject: [PATCH] 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 * Use Mock style expect(...).return(...) statements for new sea_handle_table model. * 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/main.yml | 3 + CMakeLists.txt | 19 +- docker/seahorn-dev10-verify-trusty.Dockerfile | 4 + seahorn/CMakeLists.txt | 12 +- seahorn/sea.yaml | 2 + seahorn/sea_base.yaml | 45 -- seahorn/storage/CMakeLists.txt | 11 + .../jobs/ipc/indirect_handlers/CMakeLists.txt | 3 +- .../indirect_handlers_harness.c | 7 +- .../jobs/ipc/msg_buffer/CMakeLists.txt | 3 +- .../jobs/ipc/msg_buffer/msg_buffer_harness.c | 6 +- .../ipc/port_create_destroy/CMakeLists.txt | 8 +- seahorn/storage/lib/sea_ipc_helper.c | 2 +- seahorn/trusty/CMakeLists.txt | 2 +- seahorn/trusty/user/base/lib/CMakeLists.txt | 12 + .../base/lib/libc-trusty-ptr/CMakeLists.txt | 10 + .../lib/libc-trusty-ptr/proof/CMakeLists.txt | 11 + .../proof/port_accept/CMakeLists.txt | 5 + .../libc-trusty-ptr/proof/port_accept/main.c | 56 +++ .../proof/port_close/CMakeLists.txt | 5 + .../libc-trusty-ptr/proof/port_close/main.c | 33 ++ .../proof/port_connect/CMakeLists.txt | 5 + .../libc-trusty-ptr/proof/port_connect/main.c | 50 ++ .../proof/port_create/CMakeLists.txt | 5 + .../libc-trusty-ptr/proof/port_create/main.c | 40 ++ .../proof/port_get_msg/CMakeLists.txt | 5 + .../libc-trusty-ptr/proof/port_get_msg/main.c | 73 +++ .../proof/port_put_msg/CMakeLists.txt | 6 + .../libc-trusty-ptr/proof/port_put_msg/main.c | 72 +++ .../proof/port_put_msg/sea.yaml | 3 + .../proof/port_read_msg/CMakeLists.txt | 5 + .../proof/port_read_msg/main.c | 79 ++++ .../proof/port_send_msg/CMakeLists.txt | 5 + .../proof/port_send_msg/main.c | 93 ++++ .../proof/port_set_cookie/CMakeLists.txt | 5 + .../proof/port_set_cookie/main.c | 49 ++ .../proof/port_wait/CMakeLists.txt | 5 + .../libc-trusty-ptr/proof/port_wait/main.c | 53 +++ .../proof/port_wait_any/CMakeLists.txt | 6 + .../proof/port_wait_any/main.c | 56 +++ .../proof/port_wait_any/sea.yaml | 3 + .../lib/libc-trusty-ptr/sea_handle_table.c | 189 ++++++++ .../lib/libc-trusty-ptr/sea_handle_table.h | 49 ++ .../lib/libc-trusty-ptr/trusty_syscalls.h | 33 ++ .../libc-trusty-ptr/trusty_syscalls_impl.c | 182 +++++++ .../user/base/lib/libc-trusty/CMakeLists.txt | 13 +- .../lib/libc-trusty/proof/port_accept/main.c | 2 +- .../lib/libc-trusty/proof/port_close/main.c | 2 +- .../lib/libc-trusty/proof/port_connect/main.c | 4 +- .../lib/libc-trusty/proof/port_create/main.c | 2 +- .../lib/libc-trusty/proof/port_get_msg/main.c | 4 +- .../lib/libc-trusty/proof/port_put_msg/main.c | 4 +- .../libc-trusty/proof/port_read_msg/main.c | 4 +- .../libc-trusty/proof/port_send_msg/main.c | 4 +- .../libc-trusty/proof/port_set_cookie/main.c | 4 +- .../lib/libc-trusty/proof/port_wait/main.c | 4 +- .../libc-trusty/proof/port_wait_any/main.c | 4 +- .../lib/libc-trusty/trusty_syscalls_impl.c | 2 +- seahorn/trusty_common/include/handle_table.h | 2 +- seahorn/trusty_common/lib/CMakeLists.txt | 26 +- seahorn/trusty_common/lib/handle_table_ptr.c | 45 ++ seahorn/trusty_common/stubs/CMakeLists.txt | 2 +- trusty_mod/trusty/user/app/storage/ipc.c | 447 ++++++++++++++++++ .../trusty/user/base/include/user/AUTHORS | 10 + .../trusty/user/base/include/user/LICENSE | 21 + .../base/include/user/trusty_app_manifest.h | 62 +++ .../user/base/include/user/trusty_err.h | 23 + .../user/base/include/user/trusty_ipc.h | 158 +++++++ .../user/base/include/user/trusty_log.h | 100 ++++ .../user/base/include/user/trusty_uio.h | 31 ++ .../user/base/include/user/trusty_unittest.h | 30 ++ 71 files changed, 2240 insertions(+), 100 deletions(-) delete mode 100644 seahorn/sea_base.yaml create mode 100644 seahorn/trusty/user/base/lib/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_accept/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_accept/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_close/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_close/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_connect/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_connect/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_create/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_create/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_get_msg/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_get_msg/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/sea.yaml create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_read_msg/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_read_msg/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_send_msg/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_send_msg/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_set_cookie/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_set_cookie/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/CMakeLists.txt create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/main.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/sea.yaml create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.c create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.h create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls.h create mode 100644 seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls_impl.c create mode 100644 seahorn/trusty_common/lib/handle_table_ptr.c create mode 100644 trusty_mod/trusty/user/app/storage/ipc.c create mode 100644 trusty_mod/trusty/user/base/include/user/AUTHORS create mode 100644 trusty_mod/trusty/user/base/include/user/LICENSE create mode 100644 trusty_mod/trusty/user/base/include/user/trusty_app_manifest.h create mode 100644 trusty_mod/trusty/user/base/include/user/trusty_err.h create mode 100644 trusty_mod/trusty/user/base/include/user/trusty_ipc.h create mode 100644 trusty_mod/trusty/user/base/include/user/trusty_log.h create mode 100644 trusty_mod/trusty/user/base/include/user/trusty_uio.h create mode 100644 trusty_mod/trusty/user/base/include/user/trusty_unittest.h diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index e57f612..872c833 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -37,3 +37,6 @@ jobs: - 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_ptr && 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 }}\"" diff --git a/CMakeLists.txt b/CMakeLists.txt index 2b1eb53..b757ac4 100644 --- a/CMakeLists.txt +++ b/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) diff --git a/docker/seahorn-dev10-verify-trusty.Dockerfile b/docker/seahorn-dev10-verify-trusty.Dockerfile index 1d890f7..6be38d1 100644 --- a/docker/seahorn-dev10-verify-trusty.Dockerfile +++ b/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 diff --git a/seahorn/CMakeLists.txt b/seahorn/CMakeLists.txt index d1f6d61..5f72f44 100644 --- a/seahorn/CMakeLists.txt +++ b/seahorn/CMakeLists.txt @@ -169,10 +169,14 @@ 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) - # work-around for Mac + #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() @@ -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) diff --git a/seahorn/sea.yaml b/seahorn/sea.yaml index 38316b0..14483ea 100644 --- a/seahorn/sea.yaml +++ b/seahorn/sea.yaml @@ -43,3 +43,5 @@ verify_options: temp-dir: /tmp/verifyTrusty # time and result stats horn-stats: true + horn-bv2-ptr-size: 8 + horn-bv2-word-size: 8 \ No newline at end of file diff --git a/seahorn/sea_base.yaml b/seahorn/sea_base.yaml deleted file mode 100644 index 865245b..0000000 --- a/seahorn/sea_base.yaml +++ /dev/null @@ -1,45 +0,0 @@ -verify_options: -# Optimization level - '-O3': '' -# -# PREPROCESSING -# - inline: '' - enable-loop-idiom: '' - enable-indvar: '' - no-lower-gv-init-struct: '' - externalize-addr-taken-functions: '' - no-kill-vaarg: '' - with-arith-overflow: true - horn-unify-assumes: true - horn-gsa: '' -# do not instrument library functions with memory assertions - no-fat-fns: 'bcmp,memcpy,assert_bytes_match,ensure_linked_list_is_allocated,sea_aws_linked_list_is_valid' -# context-sensitive type-aware alias analysis - dsa: sea-cs-t -# weak support for function pointers. sea-dsa is better but less stable - devirt-functions: 'types' -# bit-precise memory-precise operational semantics - bmc: opsem - horn-vcgen-use-ite: '' -# ignore control flow - horn-vcgen-only-dataflow: true -# reduce by data dependence - horn-bmc-coi: true -# static allocator supports symbolic allocation size - sea-opsem-allocator: static -# stack allocation from a symbolic starting point - horn-explicit-sp0: false -# lambdas for memory - horn-bv2-lambdas: '' -# use z3 simplifier during vcgen - horn-bv2-simplify: true -# wide memory manager to track pointer sizes - horn-bv2-extra-widemem: '' -# intermediate results in human readable form for debugging - '-S': '' -# keep intermediate results for debugging - keep-temps: '' - temp-dir: /tmp/verifyTrusty -# time and result stats - horn-stats: true diff --git a/seahorn/storage/CMakeLists.txt b/seahorn/storage/CMakeLists.txt index f916674..4da3a7d 100644 --- a/seahorn/storage/CMakeLists.txt +++ b/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) \ No newline at end of file diff --git a/seahorn/storage/jobs/ipc/indirect_handlers/CMakeLists.txt b/seahorn/storage/jobs/ipc/indirect_handlers/CMakeLists.txt index a207498..72a710d 100644 --- a/seahorn/storage/jobs/ipc/indirect_handlers/CMakeLists.txt +++ b/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 ) diff --git a/seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c b/seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c index 8161b12..dd9772c 100644 --- a/seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c +++ b/seahorn/storage/jobs/ipc/indirect_handlers/indirect_handlers_harness.c @@ -22,10 +22,9 @@ #include "ipc.h" -#include "handle_table.h" +#include #include "seahorn/seahorn.h" #include "sea_ipc_helper.h" -#define assert sassert #include "tipc_limits.h" #include @@ -43,7 +42,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); diff --git a/seahorn/storage/jobs/ipc/msg_buffer/CMakeLists.txt b/seahorn/storage/jobs/ipc/msg_buffer/CMakeLists.txt index 02bca07..4cdc4af 100644 --- a/seahorn/storage/jobs/ipc/msg_buffer/CMakeLists.txt +++ b/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 ) diff --git a/seahorn/storage/jobs/ipc/msg_buffer/msg_buffer_harness.c b/seahorn/storage/jobs/ipc/msg_buffer/msg_buffer_harness.c index ad060bf..3436890 100644 --- a/seahorn/storage/jobs/ipc/msg_buffer/msg_buffer_harness.c +++ b/seahorn/storage/jobs/ipc/msg_buffer/msg_buffer_harness.c @@ -10,7 +10,7 @@ #include "tipc_limits.h" #include -#include "handle_table.h" +#include #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); diff --git a/seahorn/storage/jobs/ipc/port_create_destroy/CMakeLists.txt b/seahorn/storage/jobs/ipc/port_create_destroy/CMakeLists.txt index ba666e7..a1be337 100644 --- a/seahorn/storage/jobs/ipc/port_create_destroy/CMakeLists.txt +++ b/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) diff --git a/seahorn/storage/lib/sea_ipc_helper.c b/seahorn/storage/lib/sea_ipc_helper.c index 512d12e..6dd7e43 100644 --- a/seahorn/storage/lib/sea_ipc_helper.c +++ b/seahorn/storage/lib/sea_ipc_helper.c @@ -56,7 +56,7 @@ static int sync_ipc_msg_handler(struct ipc_channel_context *context, void *msg, .iov_len = msg_size, }; - handle_t rc = sync_ipc_send_msg(context->common.handle, &tx_iov, 1, &rx_iov, 1); + int rc = sync_ipc_send_msg(context->common.handle, &tx_iov, 1, &rx_iov, 1); if (rc < 0) return rc; diff --git a/seahorn/trusty/CMakeLists.txt b/seahorn/trusty/CMakeLists.txt index e692b86..c105cd9 100644 --- a/seahorn/trusty/CMakeLists.txt +++ b/seahorn/trusty/CMakeLists.txt @@ -1 +1 @@ -add_subdirectory(user/base/lib/libc-trusty) +add_subdirectory(user/base/lib) diff --git a/seahorn/trusty/user/base/lib/CMakeLists.txt b/seahorn/trusty/user/base/lib/CMakeLists.txt new file mode 100644 index 0000000..7d78f18 --- /dev/null +++ b/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) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/CMakeLists.txt new file mode 100644 index 0000000..836a039 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/CMakeLists.txt new file mode 100644 index 0000000..10bd623 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_accept/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_accept/CMakeLists.txt new file mode 100644 index 0000000..7464315 --- /dev/null +++ b/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) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_accept/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_accept/main.c new file mode 100644 index 0000000..bfe283e --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_accept/main.c @@ -0,0 +1,56 @@ +#include +#include "trusty_ipc.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; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_close/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_close/CMakeLists.txt new file mode 100644 index 0000000..ac8107d --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_close/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(port_close_pf main.c) +sea_link_libraries(port_close_pf sea_libc_trusty.ir) + +sea_attach_bc(port_close_pf) +sea_add_unsat_test(port_close_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_close/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_close/main.c new file mode 100644 index 0000000..19a3f70 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_close/main.c @@ -0,0 +1,33 @@ +#include +#include "trusty_ipc.h" + +const char* PATH = "seahorn.com"; + +int main(void) { + + handle_t port; + + port = + port_create(PATH, 1, 100, + IPC_PORT_ALLOW_NS_CONNECT | IPC_PORT_ALLOW_TA_CONNECT); + + // -- got expected handle + sassert(!port->secure); + + int rc; + + // release handle + rc = close(port); + sassert(rc == 0); + sassert(!port->active); + + // check if a new port can be created after close + port = + port_create(PATH, 1, 100, + IPC_PORT_ALLOW_NS_CONNECT | IPC_PORT_ALLOW_TA_CONNECT); + + // -- got expected handle + sassert(!port->secure); + + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_connect/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_connect/CMakeLists.txt new file mode 100644 index 0000000..6067ce5 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_connect/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(port_connect_pf main.c) +sea_link_libraries(port_connect_pf sea_libc_trusty.ir) + +sea_attach_bc(port_connect_pf) +sea_add_unsat_test(port_connect_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_connect/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_connect/main.c new file mode 100644 index 0000000..ca967ab --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_connect/main.c @@ -0,0 +1,50 @@ +#include +#include "trusty_ipc.h" +#include "uapi/err.h" +#include + +/* Documentation from trusty API: + connect() +Initiates a connection to a port specified by name. + +long connect(const char *path, uint flags); + +[in] path: Name of a port published by a Trusty application +[in] flags: Specifies additional, optional behavior + +[retval]: Handle to a channel over which messages can be exchanged +with the server; error if negative +*/ + +const char* PATH = "ta.seahorn.com"; + +int main(void) { + + handle_t h1 = + port_create(PATH, 1, 100, IPC_PORT_ALLOW_TA_CONNECT); + + // expect non-secure handle + sassert(!h1->secure); + + handle_t h2 = + port_create(PATH, 1, 100, + IPC_PORT_ALLOW_NS_CONNECT); + + // expect secure handle + sassert(h2->secure); + + handle_t rc; + + // connect will connect to h2 + on_connect_return(h2); + + rc = connect(PATH, IPC_CONNECT_ASYNC | IPC_CONNECT_WAIT_FOR_PORT); + // expect valid connection + sassert(rc > 0); + + rc = connect(PATH, IPC_CONNECT_ASYNC | IPC_CONNECT_WAIT_FOR_PORT); + // expect valid connection + sassert(rc > 0); + + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_create/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_create/CMakeLists.txt new file mode 100644 index 0000000..f0cd888 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_create/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(port_create_pf main.c) +sea_link_libraries(port_create_pf sea_libc_trusty.ir) + +sea_attach_bc(port_create_pf) +sea_add_unsat_test(port_create_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_create/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_create/main.c new file mode 100644 index 0000000..c55bff6 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_create/main.c @@ -0,0 +1,40 @@ +#include +#include "trusty_ipc.h" + +const char* PATH = "seahorn.com"; + +int main(void) { + + handle_t h = + port_create(PATH, 1, 100, + IPC_PORT_ALLOW_NS_CONNECT | IPC_PORT_ALLOW_TA_CONNECT); + + // -- got expected handle + sassert(!h->secure); + + handle_t h2 = + port_create(PATH, 1, 100, + IPC_PORT_ALLOW_NS_CONNECT | IPC_PORT_ALLOW_TA_CONNECT); + + // -- can create more insecure handles + sassert(!h2->secure); + + h2 = port_create(PATH, 1, 100, IPC_PORT_ALLOW_NS_CONNECT); + // -- expected secure handle handle + sassert(h2->secure); + + handle_t h3 = port_create(PATH, 1, 100, IPC_PORT_ALLOW_NS_CONNECT); + // -- can create more secure handles + sassert(h3->secure); + + + // release handle + close(h); + h = INVALID_IPC_HANDLE; + + // request again + h = port_create("seahorn.com", 1, 100, + IPC_PORT_ALLOW_NS_CONNECT | IPC_PORT_ALLOW_TA_CONNECT); + sassert(!h->secure); + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_get_msg/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_get_msg/CMakeLists.txt new file mode 100644 index 0000000..4eda125 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_get_msg/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(port_get_msg_pf main.c) +sea_link_libraries(port_get_msg_pf sea_libc_trusty.ir) + +sea_attach_bc(port_get_msg_pf) +sea_add_unsat_test(port_get_msg_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_get_msg/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_get_msg/main.c new file mode 100644 index 0000000..b8c7bb4 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_get_msg/main.c @@ -0,0 +1,73 @@ +#include +#include +#include "trusty_ipc.h" +#include "uapi/err.h" +/* Documentation from trusty API: + get_msg() +Gets meta-information about the next message in an incoming message queue +of a specified channel. + +long get_msg(uint32_t handle, ipc_msg_info_t *msg_info); +[in] handle: Handle of the channel on which a new message must be retrieved. +[out] msg_info: Message information structure described as follows: +typedef struct ipc_msg_info { + size_t len; + uint32_t id; +} ipc_msg_info_t; +Each message is assigned a unique ID across the set of outstanding messages, +and the total length of each message is filled in. +If configured and allowed by the protocol, +there can be multiple outstanding (opened) messages at once for a particular channel. + +[retval]: NO_ERROR on success; a negative error otherwise +*/ + +int main(void) { + + handle_t port = + port_create("ta.seahorn.com", 1, 100, IPC_PORT_ALLOW_TA_CONNECT); + + // expect non-secure handle + sassert(!port->secure); + + uevent_t event = {.handle = INVALID_IPC_HANDLE, .event = 0, .cookie = NULL}; + + int rc = wait(port, &event, INFINITE_TIME); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + /* got an event */ + sassert(event.handle == port); + // No cookie set + sassert(!event.cookie); + + // handle port event + uuid_t peer_uuid; + if (event.event & IPC_HANDLE_POLL_READY) { + /* incoming connection: accept it */ + handle_t chan = accept(port, &peer_uuid); + sassert(chan->type == channel); + + uevent_t cev; + + rc = wait(chan, &cev, INFINITE_TIME); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + if (cev.event & IPC_HANDLE_POLL_MSG) { + ipc_msg_info_t msg_info; + + /* get message info */ + rc = get_msg(chan, &msg_info); + if (rc == NO_ERROR) { + sassert(msg_info.id != 0); + sassert(msg_info.len >= 0); + } + + rc = close(chan); + sassert(rc == NO_ERROR); + } + } + } + } + + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/CMakeLists.txt new file mode 100644 index 0000000..2d0d343 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/CMakeLists.txt @@ -0,0 +1,6 @@ +add_executable(port_put_msg_pf main.c) +sea_link_libraries(port_put_msg_pf sea_libc_trusty.ir) + +sea_attach_bc(port_put_msg_pf) +configure_file(sea.yaml sea.yaml @ONLY) +sea_add_unsat_test(port_put_msg_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/main.c new file mode 100644 index 0000000..50f371b --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/main.c @@ -0,0 +1,72 @@ +#include +#include "trusty_ipc.h" +#include "uapi/err.h" +/* Documentation from trusty API: + put_msg() +Retires a message with a specified ID. + +long put_msg(uint32_t handle, uint32_t msg_id); +[in] handle: Handle of the channel on which the message has arrived. +[in] msg_id: ID of message being retired. + +[retval]: NO_ERROR on success; a negative error otherwise. +*/ + +# define MAX_ECHO_MSG_SIZE 64 + +int main(void) { + + handle_t port = + port_create("ta.seahorn.com", 1, 100, IPC_PORT_ALLOW_TA_CONNECT); + + // expect non-secure handle + sassert(!port->secure); + + uevent_t event = {.handle = INVALID_IPC_HANDLE, .event = 0, .cookie = NULL}; + + int rc = wait(port, &event, INFINITE_TIME); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + /* got an event */ + sassert(event.handle == port); + // No cookie set + sassert(!event.cookie); + + // handle port event + uuid_t peer_uuid; + if (event.event & IPC_HANDLE_POLL_READY) { + handle_t chan = accept(port, &peer_uuid); + sassert(chan->type == channel); + + uevent_t cev; + + rc = wait(chan, &cev, INFINITE_TIME); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + if (cev.event & IPC_HANDLE_POLL_MSG) { + ipc_msg_info_t msg_info; + rc = get_msg(chan, &msg_info); + assume(rc == NO_ERROR); + sassert(msg_info.id != 0); + + uint8_t buf[MAX_ECHO_MSG_SIZE]; + struct iovec iov = {.iov_base = buf, .iov_len = sizeof(buf)}; + ipc_msg_t msg = {.num_iov = 1, .iov = &iov, .num_handles = 1, .handles = NULL}; + rc = read_msg(chan, msg_info.id, 0, &msg); + assume(rc >= NO_ERROR); + sassert(rc <= MAX_ECHO_MSG_SIZE); + + // discard msg + rc = put_msg(chan, msg_info.id); + assume(rc == NO_ERROR); + rc = read_msg(chan, msg_info.id, 0, &msg); + sassert(rc < NO_ERROR); + } + } + } + } + + + + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/sea.yaml b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/sea.yaml new file mode 100644 index 0000000..89a54c2 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_put_msg/sea.yaml @@ -0,0 +1,3 @@ +verify_options: +# stack allocation from a symbolic starting point + horn-explicit-sp0: true \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_read_msg/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_read_msg/CMakeLists.txt new file mode 100644 index 0000000..98484a7 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_read_msg/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(port_read_msg_pf main.c) +sea_link_libraries(port_read_msg_pf sea_libc_trusty.ir) + +sea_attach_bc(port_read_msg_pf) +sea_add_unsat_test(port_read_msg_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_read_msg/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_read_msg/main.c new file mode 100644 index 0000000..c150ba7 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_read_msg/main.c @@ -0,0 +1,79 @@ +#include +#include "trusty_ipc.h" +#include "uapi/err.h" +/* Documentation from trusty API: + read_msg() +Reads the content of the message with the specified ID starting from the +specified offset. + +long read_msg(uint32_t handle, uint32_t msg_id, uint32_t offset, ipc_msg_t +*msg); +[in] handle: Handle of the channel from which to read the message. +[in] msg_id: ID of the message to read. +[in] offset: Offset into the message from which to start reading. +[in] msg: Pointer to the ipc_msg_t structure describing a set of buffers into +which to store incoming message data. + +[retval]: Total number of bytes stored in the dst buffers on success; +a negative error otherwise. +*/ + +# define MAX_ECHO_MSG_SIZE 64 + +int main(void) { + + handle_t port = + port_create("ta.seahorn.com", 1, 100, IPC_PORT_ALLOW_TA_CONNECT); + + // expect non-secure handle + sassert(!port->secure); + + uevent_t event = {.handle = INVALID_IPC_HANDLE, .event = 0, .cookie = NULL}; + + int rc = wait(port, &event, INFINITE_TIME); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + /* got an event */ + sassert(event.handle == port); + // No cookie set + sassert(!event.cookie); + + // handle port event + uuid_t peer_uuid; + if (event.event & IPC_HANDLE_POLL_READY) { + handle_t chan = accept(port, &peer_uuid); + assume(chan != INVALID_IPC_HANDLE); + sassert(chan->type == channel); + + uevent_t cev; + + rc = wait(chan, &cev, INFINITE_TIME); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + if (cev.event & IPC_HANDLE_POLL_MSG) { + ipc_msg_info_t msg_info; + rc = get_msg(chan, &msg_info); + assume(rc == NO_ERROR); + sassert(msg_info.id != 0); + + uint8_t buf[MAX_ECHO_MSG_SIZE]; + struct iovec iov = {.iov_base = buf, .iov_len = sizeof(buf)}; + ipc_msg_t msg = {.num_iov = 1, .iov = &iov, .num_handles = 1, .handles = NULL}; + rc = read_msg(chan, msg_info.id, 0, &msg); + assume(rc >= NO_ERROR); + sassert(rc <= MAX_ECHO_MSG_SIZE); + + /* cleanup */ + rc = put_msg(chan, msg_info.id); + assume(rc == NO_ERROR); + rc = close(chan); + sassert(rc == NO_ERROR); + } + } + } + } + + + + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_send_msg/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_send_msg/CMakeLists.txt new file mode 100644 index 0000000..81af646 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_send_msg/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(port_send_msg_pf main.c) +sea_link_libraries(port_send_msg_pf sea_libc_trusty.ir) + +sea_attach_bc(port_send_msg_pf) +sea_add_unsat_test(port_send_msg_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_send_msg/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_send_msg/main.c new file mode 100644 index 0000000..8ff5c03 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_send_msg/main.c @@ -0,0 +1,93 @@ +#include +#include +#include "trusty_ipc.h" +#include "uapi/err.h" +/* Documentation from trusty API: + send_msg() +Sends a message over a specified channel. + +long send_msg(uint32_t handle, ipc_msg_t *msg); +[in] handle: Handle to the channel over which to send the message. +[in] msg: Pointer to the ipc_msg_t structure describing the message. + +[retval]: Total number of bytes sent on success; a negative error otherwise. +*/ + +# define MAX_ECHO_MSG_SIZE 64 + +const char* PATH = "ta.seahorn.com"; + +int main(void) { + + /* server side */ + handle_t port = + port_create(PATH, 1, 100, IPC_PORT_ALLOW_TA_CONNECT); + + // expect non-secure handle + sassert(!port->secure); + + on_connect_return(port); + + /* client side */ + handle_t c_chan; + c_chan = connect(PATH, IPC_CONNECT_ASYNC | IPC_CONNECT_WAIT_FOR_PORT); + // check if use a valid connection + sassert(c_chan->type == channel); + + // send a message + uint8_t snd_buf[32]; + struct iovec snd_iov = {.iov_base = snd_buf, .iov_len = sizeof(snd_buf)}; + ipc_msg_t snd_msg = {.num_iov = 1, .iov = &snd_iov, .num_handles = 1, .handles = NULL}; + + ssize_t rc = send_msg(c_chan, &snd_msg); + assume(rc >= 0); + + /* server side */ + uevent_t event = {.handle = INVALID_IPC_HANDLE, .event = 0, .cookie = NULL}; + rc = wait(port, &event, INFINITE_TIME); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + /* got an event */ + sassert(event.handle == port); + // No cookie set + sassert(!event.cookie); + + // handle port event + uuid_t peer_uuid; + if (event.event & IPC_HANDLE_POLL_READY) { + handle_t chan = accept(port, &peer_uuid); + assume(chan != INVALID_IPC_HANDLE); + sassert(chan->type == channel); + + uevent_t cev; + + rc = wait(chan, &cev, INFINITE_TIME); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + if (cev.event & IPC_HANDLE_POLL_MSG) { + ipc_msg_info_t msg_info; + rc = get_msg(chan, &msg_info); + assume(rc == NO_ERROR); + sassert(msg_info.id != 0); + + uint8_t rcv_buf[MAX_ECHO_MSG_SIZE]; + struct iovec rcv_iov = {.iov_base = rcv_buf, .iov_len = sizeof(rcv_buf)}; + ipc_msg_t rcv_msg = {.num_iov = 1, .iov = &rcv_iov, .num_handles = 1, .handles = NULL}; + rc = read_msg(chan, msg_info.id, 0, &rcv_msg); + assume(rc >= NO_ERROR); + sassert(rc <= MAX_ECHO_MSG_SIZE); + + /* cleanup */ + rc = put_msg(chan, msg_info.id); + assume(rc == NO_ERROR); + rc = close(chan); + sassert(rc == NO_ERROR); + } + } + } + } + + + + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_set_cookie/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_set_cookie/CMakeLists.txt new file mode 100644 index 0000000..e32adee --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_set_cookie/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(port_set_cookie_pf main.c) +sea_link_libraries(port_set_cookie_pf sea_libc_trusty.ir) + +sea_attach_bc(port_set_cookie_pf) +sea_add_unsat_test(port_set_cookie_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_set_cookie/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_set_cookie/main.c new file mode 100644 index 0000000..0cea4d2 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_set_cookie/main.c @@ -0,0 +1,49 @@ +#include +#include "trusty_ipc.h" +#include "uapi/err.h" + +typedef void (*event_handler_proc_t)(const uevent_t* ev, void* ctx); + +struct ipc_event_handler { + event_handler_proc_t proc; + void* priv; +}; + +void port_handler(const uevent_t* ev, void* ctx) { + return; +} + +static struct ipc_event_handler port_evt_handler = { + .proc = port_handler, + .priv = NULL, +}; + +int main(void) { + + handle_t port = + port_create("ta.seahorn.com", 1, 100, IPC_PORT_ALLOW_TA_CONNECT); + + // expect non-secure handle + sassert(!port->secure); + + uevent_t event; + int rc; + + rc = set_cookie(port, &port_evt_handler); + sassert(rc == 0); + + event.handle = INVALID_IPC_HANDLE; + event.event = 0; + event.cookie = NULL; + + rc = wait(port, &event, 0); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + /* got an event */ + sassert(event.handle == port); + // Cookie set + sassert(event.cookie); + } + + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait/CMakeLists.txt new file mode 100644 index 0000000..a8d5655 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait/CMakeLists.txt @@ -0,0 +1,5 @@ +add_executable(port_wait_pf main.c) +sea_link_libraries(port_wait_pf sea_libc_trusty.ir) + +sea_attach_bc(port_wait_pf) +sea_add_unsat_test(port_wait_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait/main.c new file mode 100644 index 0000000..67295f7 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait/main.c @@ -0,0 +1,53 @@ +#include +#include "trusty_ipc.h" +#include "uapi/err.h" + +int main(void) { + + handle_t port = + port_create("ta.seahorn.com", 1, 100, IPC_PORT_ALLOW_TA_CONNECT); + + // expect non-secure handle + sassert(!port->secure); + + uevent_t event = {.handle = INVALID_IPC_HANDLE, .event = 0, .cookie = NULL}; + + int rc = wait(port, &event, 0); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + /* got an event */ + sassert(event.handle == port); + // No cookie set + sassert(!event.cookie); + } + + uuid_t peer_uuid; + handle_t chan = accept(port, &peer_uuid); + assume(chan != INVALID_IPC_HANDLE); + sassert(chan->type == channel); + + rc = wait(chan, &event, 0); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + if (event.event & IPC_HANDLE_POLL_MSG) { + struct ipc_msg_info msg_info; + rc = get_msg(chan, &msg_info); + assume(rc == NO_ERROR); + sassert(msg_info.id != 0); + + char buf[4096]; + struct iovec iov = {.iov_base = buf, .iov_len = sizeof(buf)}; + struct ipc_msg msg = {.num_iov = 1, .iov = &iov}; + rc = read_msg(chan, msg_info.id, 0, &msg); + assume(rc >= NO_ERROR); + sassert(rc <= 4096); + + rc = put_msg(chan, msg_info.id); + assume(rc == NO_ERROR); + rc = read_msg(chan, msg_info.id, 0, &msg); + sassert(rc < NO_ERROR); + } + } + + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/CMakeLists.txt new file mode 100644 index 0000000..ced597e --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/CMakeLists.txt @@ -0,0 +1,6 @@ +add_executable(port_wait_any_pf main.c) +sea_link_libraries(port_wait_any_pf sea_libc_trusty.ir) + +sea_attach_bc(port_wait_any_pf) +configure_file(sea.yaml sea.yaml @ONLY) +sea_add_unsat_test(port_wait_any_pf) diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/main.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/main.c new file mode 100644 index 0000000..f653bbd --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/main.c @@ -0,0 +1,56 @@ +#include +#include +#include "trusty_ipc.h" +#include "uapi/err.h" + +int main(void) { + + handle_t port = + port_create("ta.seahorn.com", 1, 100, IPC_PORT_ALLOW_TA_CONNECT); + + // expect non-secure handle + sassert(!port->secure); + + uevent_t event = {.handle = INVALID_IPC_HANDLE, .event = 0, .cookie = NULL}; + + on_waitany_return(port); + + int rc = wait_any(&event, 0); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + /* got an event */ + sassert(event.handle == port); + // No cookie set + sassert(!event.cookie); + } + + uuid_t peer_uuid; + handle_t chan = accept(port, &peer_uuid); + assume(chan != INVALID_IPC_HANDLE); + sassert(chan->type == channel); + + rc = wait_any(&event, 0); + sassert(rc <= NO_ERROR); + if (rc == NO_ERROR) { + if (event.event & IPC_HANDLE_POLL_MSG) { + struct ipc_msg_info msg_info; + rc = get_msg(chan, &msg_info); + assume(rc == NO_ERROR); + sassert(msg_info.id != 0); + + char buf[4096]; + struct iovec iov = {.iov_base = buf, .iov_len = sizeof(buf)}; + struct ipc_msg msg = {.num_iov = 1, .iov = &iov}; + rc = read_msg(chan, msg_info.id, 0, &msg); + assume(rc >= NO_ERROR); + sassert(rc <= 4096); + + rc = put_msg(chan, msg_info.id); + assume(rc == NO_ERROR); + rc = read_msg(chan, msg_info.id, 0, &msg); + sassert(rc < NO_ERROR); + } + } + + return 0; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/sea.yaml b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/sea.yaml new file mode 100644 index 0000000..89a54c2 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/proof/port_wait_any/sea.yaml @@ -0,0 +1,3 @@ +verify_options: +# stack allocation from a symbolic starting point + horn-explicit-sp0: true \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.c new file mode 100644 index 0000000..0f3672f --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.c @@ -0,0 +1,189 @@ +/** +Implementation of table of handles to be used by IPC +*/ + +/** Global variables that keep current handle information */ + +#include "sea_handle_table.h" +#include "trusty_ipc.h" +#include +#include + +#include + +#define ND __declspec(noalias) + +// Records the handle to return on wait_any +handle_t g_on_waitany_handle; +// Records the handle to return on connect +handle_t g_on_connect_handle; + +extern ND bool nd_bool(void); + +void* malloc_can_fail(size_t sz) { + return nd_bool() ? malloc(sz) : NULL; +} + +void* malloc_no_fail(size_t sz) { + return malloc(sz); +} + +handle_t ptoh(HandleState* p) { + // This narrowing operation is safe since ptr is assumed to be aligned. + return p; +} + +HandleState* htop(handle_t h) { + // This widening operation is safe since ptr is assumed to be aligned. + return ((HandleState*)(h)); +} + + +bool sea_ht_has_msg(handle_t chan_handle) { + return htop(chan_handle)->msg.id > INVALID_IPC_MSG_ID; +} + +uint32_t sea_ht_get_msg_id(handle_t chan_handle) { + return htop(chan_handle)->msg.id; +} + +// assume channel handle +void sea_ht_set_msg_id(handle_t chan_handle, uint32_t id) { + htop(chan_handle)->msg.id = id; +} + +// assume channel handle +size_t sea_ht_get_msg_len(handle_t chan_handle) { + return htop(chan_handle)->msg.len; +} + +void sea_ht_set_msg_len(handle_t chan_handle, size_t len) { + htop(chan_handle)->msg.len = len; +} + +extern ND size_t nd_msg_len(void); +extern ND size_t nd_size(void); +extern ND uint32_t nd_msg_id(void); + +void sea_ht_new_nd_msg(handle_t chan_handle) { + htop(chan_handle)->msg.len = nd_msg_len(); + htop(chan_handle)->msg.id = nd_msg_id(); + assume(htop(chan_handle)->msg.id> INVALID_IPC_MSG_ID); + return; +} + +/** + * Set handle to inactive + */ +void sea_ht_free(handle_t handle) { + // we cannot "free" the handle since we might want to query state after this call + handle->active = false; +} + +/** +Allocates a new port handle + +Return INVALID_IPC_HANDLE if no handle is available to be allocated +*/ +handle_t sea_ht_new_port(bool secure, const char *path) { +#if CAN_RETURN_INVALID_IPC_HANDLE + HandleState* h = (HandleState*) malloc_can_fail(sizeof(HandleState)); +#else + HandleState* h = (HandleState*) malloc_no_fail(sizeof(HandleState)); +#endif + if (!h) return INVALID_IPC_HANDLE; + h->active = true; + h->secure = secure; + h->type = port; + h->cookie = NULL; + h->path = path; + h->msg = (struct Msg){INVALID_IPC_MSG_ID}; + return ptoh(h); +} + +// TODO: should be "match" +handle_t sea_ht_math_port(const char *path) { + if (g_on_connect_handle == NULL) { + return INVALID_IPC_HANDLE; + } + // Check that the user followed the convention that identical paths + // have the same address. + sassert(g_on_connect_handle->path == path); + return g_on_connect_handle; +} + +/** +Non-deterministically chooses an active handle + +Blocks if no active handle is available +*/ +handle_t sea_ht_choose_active_handle(void) { + if (g_on_waitany_handle == NULL) { + return INVALID_IPC_HANDLE; + } + // Check that the user set an active handle + sassert(g_on_waitany_handle->active == true); + return g_on_waitany_handle; +} + +handle_t sea_ht_new_channel(handle_t parent_port) { +#if CAN_RETURN_INVALID_IPC_HANDLE + HandleState* c = (HandleState *) malloc_can_fail(sizeof(HandleState)); +#else + HandleState* c = (HandleState *) malloc_no_fail(sizeof(HandleState)); +#endif + if (!c) return INVALID_IPC_HANDLE; + c->active = true; + c->type = channel; + c->cookie = NULL; + c->path = NULL; + sea_ht_new_nd_msg(c); + return ptoh(c); +} + +// return true if passed handle is port type and active +bool sea_ht_is_active_port(handle_t handle) { + return htop(handle)->type == port && htop(handle)->active == true; +} + +// assume we are passed a port +void sea_ht_set_cookie_port(handle_t handle, void *cookie) { + htop(handle)->cookie = cookie; +} + +// assume we are passed a port +void* sea_ht_get_cookie_port(handle_t handle) { +return htop(handle)->cookie; +} + +// assume we are passed a channel +void sea_ht_set_cookie_channel(handle_t handle, void *cookie) { + htop(handle)->cookie = cookie; +} + +// assume we are passed a channel +void *sea_ht_get_cookie_channel(handle_t handle) { + return htop(handle)->cookie; +} + +// set cookie for both port/channel type +void sea_ht_set_cookie(handle_t handle, void *cookie) { + htop(handle)->cookie = cookie; +} + +// get cookie for both port/channel type +void *sea_ht_get_cookie(handle_t handle) { + return htop(handle)->cookie; +} + +// Set the handle to return on next wait_any call. +// This remains set unless unset explicitly. +void on_waitany_return(handle_t handle) { + g_on_waitany_handle = handle; +} + +// Set the handle to return on next connect call +// This remains set unless unset explicitly. +void on_connect_return(handle_t handle) { + g_on_connect_handle = handle; +} \ No newline at end of file diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.h b/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.h new file mode 100644 index 0000000..54e1f0b --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/sea_handle_table.h @@ -0,0 +1,49 @@ +#ifndef _SEA_HANDLE_TABLE_H_ +#define _SEA_HANDLE_TABLE_H_ + +#include +#include + +#define IS_PORT_IPC_HANDLE(h) (htop(h)->type == port) +#define IS_CHAN_IPC_HANDLE(h) (htop(h)->type == channel) +#define IS_SECURE_IPC_HANDLE(h) (htop(h)->secure) +#define IS_NONSECURE_IPC_HANDLE(h) (!htop(h)->secure) + +#define INVALID_IPC_MSG_ID 0 + +handle_t ptoh(HandleState* p); +HandleState* htop(handle_t h); + +handle_t sea_ht_new_port(bool secure, const char *path); +handle_t sea_ht_new_channel(handle_t port); + +handle_t sea_ht_choose_active_handle(void); + +bool sea_ht_is_active_port(handle_t handle); + +void sea_ht_set_cookie_port(handle_t handle, void *cookie); +void *sea_ht_get_cookie_port(handle_t handle); + +void sea_ht_set_cookie_channel(handle_t handle, void *cookie); +void *sea_ht_get_cookie_channel(handle_t handle); + +void sea_ht_set_cookie(handle_t handle, void *cookie); +void *sea_ht_get_cookie(handle_t handle); + +void sea_ht_free(handle_t handle); + +bool sea_ht_has_msg(handle_t chan_handle); +uint32_t sea_ht_get_msg_id(handle_t chan_handle); +void sea_ht_set_msg_id(handle_t chan_handle, uint32_t id); +size_t sea_ht_get_msg_len(handle_t chan_handle); +void sea_ht_set_msg_len(handle_t chan_handle, size_t len); +void sea_ht_new_nd_msg(handle_t chan_handle); + +handle_t sea_ht_math_port(const char *path); + +// Set the handle to return on next wait_any call +void on_waitany_return(handle_t handle); + +// Set the handle to return on next connect call +void on_connect_return(handle_t handle); +#endif diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls.h b/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls.h new file mode 100644 index 0000000..fa42475 --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls.h @@ -0,0 +1,33 @@ +#ifndef _SEA_TRUSTY_SYSCALLS_H_ +#define _SEA_TRUSTY_SYSCALLS_H_ +#include + +handle_t _trusty_port_create(const char *path, uint32_t num_recv_bufs, + uint32_t recv_buf_size, uint32_t flags); + +handle_t _trusty_connect(const char *path, uint32_t flags); + +handle_t _trusty_accept(handle_t handle, struct uuid *peer_uuid); + +int _trusty_close(handle_t handle); + +int _trusty_set_cookie(handle_t handle, void *cookie); + +handle_t _trusty_handle_set_create(void); + +int _trusty_handle_set_ctrl(handle_t handle, uint32_t cmd, struct uevent *evt); + +int _trusty_wait(handle_t handle, struct uevent *event, uint32_t timeout_msecs); + +int _trusty_wait_any(struct uevent *event, uint32_t timeout_msecs); + +int _trusty_get_msg(handle_t handle, struct ipc_msg_info *msg_info); + +ssize_t _trusty_read_msg(handle_t handle, uint32_t msg_id, uint32_t offset, + struct ipc_msg *msg); + +int _trusty_put_msg(handle_t handle, uint32_t msg_id); + +ssize_t _trusty_send_msg(handle_t handle, struct ipc_msg *msg); + +#endif diff --git a/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls_impl.c b/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls_impl.c new file mode 100644 index 0000000..6c3780e --- /dev/null +++ b/seahorn/trusty/user/base/lib/libc-trusty-ptr/trusty_syscalls_impl.c @@ -0,0 +1,182 @@ +#include "sea_handle_table.h" +#include "trusty_syscalls.h" + +#include // trusty errors definitions + +#include + +#define ND __declspec(noalias) + +extern ND void memhavoc(void *ptr, size_t size); + +handle_t _trusty_port_create(const char *path, uint32_t num_recv_bufs, + uint32_t recv_buf_size, uint32_t flags) { + (void)path; + (void)num_recv_bufs; + (void)recv_buf_size; + + if (!path) return INVALID_IPC_HANDLE; + + bool secure = (flags & IPC_PORT_ALLOW_NS_CONNECT) && + !(flags & IPC_PORT_ALLOW_TA_CONNECT); + handle_t h = sea_ht_new_port(secure, path); + return h; +} + +handle_t _trusty_connect(const char *path, uint32_t flags) { + handle_t port_handle = sea_ht_math_port(path); + if (port_handle != INVALID_IPC_HANDLE) { + handle_t chan = sea_ht_new_channel(port_handle); + return chan; + } + return INVALID_IPC_HANDLE; +} + +extern uint32_t ND nd_time_low(void); +extern uint16_t ND nd_time_mid(void); +extern uint16_t ND nd_time_hi_n_ver(void); + +unsigned int is_allow_ta_connect(handle_t handle) { + return handle->secure == true; +} + +handle_t _trusty_accept(handle_t port_handle, uuid_t *peer_uuid) { + (void)port_handle; + handle_t chan = sea_ht_new_channel(port_handle); + if (chan != INVALID_IPC_HANDLE) { + if (!is_allow_ta_connect(port_handle)) { + // non-secure world + peer_uuid->time_low = 0; + peer_uuid->time_mid = 0; + peer_uuid->time_hi_and_version = 0; + } + else { + // define peer_uuid to a dummy value + peer_uuid->time_low = nd_time_low(); + peer_uuid->time_mid = nd_time_mid(); + peer_uuid->time_hi_and_version = nd_time_hi_n_ver(); + } + } + return chan; +} + +int _trusty_close(handle_t handle) { + sea_ht_free(handle); + return NO_ERROR; +} + +int _trusty_set_cookie(handle_t handle, void *cookie) { + sea_ht_set_cookie(handle, cookie); + return NO_ERROR; +} + +handle_t _trusty_handle_set_create(void) { return INVALID_IPC_HANDLE; } + +int _trusty_handle_set_ctrl(handle_t handle, uint32_t cmd, struct uevent *evt) { + return ERR_GENERIC; +} + +extern int ND nd_trusty_ipc_err(void); +extern uint32_t nd_trusty_ipc_event(void); + +int _trusty_wait(handle_t handle, struct uevent *event, + uint32_t timeout_msecs) { + int err = nd_trusty_ipc_err(); + if (err < NO_ERROR) + return err; + + event->handle = handle; + event->cookie = sea_ht_get_cookie(handle); + event->event = nd_trusty_ipc_event(); + + if (event->event & IPC_HANDLE_POLL_MSG) { + sea_ht_new_nd_msg(handle); + } + + return NO_ERROR; +} + +int _trusty_wait_any(uevent_t *ev, uint32_t timeout_msecs) { + int err = nd_trusty_ipc_err(); + if (err < NO_ERROR) + return err; + + handle_t h = sea_ht_choose_active_handle(); + ev->handle = h; + ev->cookie = sea_ht_get_cookie(h); + ev->event = nd_trusty_ipc_event(); + + if (ev->event & IPC_HANDLE_POLL_MSG) { + sea_ht_new_nd_msg(h); + } + + return NO_ERROR; +} + +int _trusty_get_msg(handle_t handle, struct ipc_msg_info *msg_info) { + int err = nd_trusty_ipc_err(); + if (err < NO_ERROR) + return err; + + msg_info->id = sea_ht_get_msg_id(handle); + msg_info->len = sea_ht_get_msg_len(handle); + return msg_info->id != INVALID_IPC_MSG_ID ? NO_ERROR : ERR_GENERIC; +} + +ssize_t _trusty_read_msg(handle_t handle, uint32_t msg_id, uint32_t offset, + struct ipc_msg *msg) { + if (sea_ht_get_msg_id(handle) != msg_id) + return ERR_GENERIC; + size_t msg_len = sea_ht_get_msg_len(handle); + if (msg_len == 0) return ERR_GENERIC; + sassert(offset <= msg_len); + + msg_len -= offset; + + sassert(1 <= msg->num_iov); + sassert(msg->num_iov <= 2); + + if (msg_len < msg->iov[0].iov_len) { + memhavoc(msg->iov[0].iov_base, msg_len); + return msg_len; + } + memhavoc(msg->iov->iov_base, msg->iov[0].iov_len); + size_t num_bytes_read = msg->iov[0].iov_len; + if (msg->num_iov == 1) + return num_bytes_read; + msg_len -= num_bytes_read; + + if (msg_len < msg->iov[1].iov_len) { + memhavoc(msg->iov[1].iov_base, msg_len); + num_bytes_read += msg_len; + return num_bytes_read; + } + memhavoc(msg->iov->iov_base, msg->iov[1].iov_len); + num_bytes_read += msg->iov[1].iov_len; + return num_bytes_read; +} + +int _trusty_put_msg(handle_t handle, uint32_t msg_id) { + int err = nd_trusty_ipc_err(); + if (err < NO_ERROR) + return err; + + sea_ht_set_msg_id(handle, INVALID_IPC_MSG_ID); + return NO_ERROR; +} +ssize_t _trusty_send_msg(handle_t handle, struct ipc_msg *msg) { + int err = nd_trusty_ipc_err(); + if (err < NO_ERROR) + return err; + + sassert(1 <= msg->num_iov); + sassert(msg->num_iov <= 2); + + switch (msg->num_iov) { + case 1: + return msg->iov[0].iov_len; + case 2: + return msg->iov[0].iov_len + msg->iov[1].iov_len; + } + return ERR_GENERIC; +} diff --git a/seahorn/trusty/user/base/lib/libc-trusty/CMakeLists.txt b/seahorn/trusty/user/base/lib/libc-trusty/CMakeLists.txt index f1b09a8..923ad52 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/CMakeLists.txt +++ b/seahorn/trusty/user/base/lib/libc-trusty/CMakeLists.txt @@ -1,13 +1,10 @@ -set(EXTERNAL ${TRUSTY_ROOT}/trusty/user/base/lib/libc-trusty) -add_library( - sea_libc_trusty - ${EXTERNAL}/ipc.c - sea_handle_table.c - trusty_syscalls_impl.c -) - +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_libc_trusty.ir has to be built before attaching subdirectories since they depend on it sea_attach_bc(sea_libc_trusty) add_subdirectory(proof) diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_accept/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_accept/main.c index e290a05..9b8fe3c 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_accept/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_accept/main.c @@ -1,5 +1,5 @@ #include -#include +#include "trusty_ipc.h" /* Documentation from trusty API: accept() diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_close/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_close/main.c index 0ce6e7a..e5aa2e6 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_close/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_close/main.c @@ -1,5 +1,5 @@ #include -#include +#include "trusty_ipc.h" int main(void) { diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_connect/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_connect/main.c index d1bb2f5..9a08621 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_connect/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_connect/main.c @@ -1,6 +1,6 @@ #include -#include -#include +#include "trusty_ipc.h" +#include "uapi/err.h" /* Documentation from trusty API: connect() Initiates a connection to a port specified by name. diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_create/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_create/main.c index 8f50b41..15d4079 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_create/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_create/main.c @@ -1,5 +1,5 @@ #include -#include +#include "trusty_ipc.h" int main(void) { diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_get_msg/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_get_msg/main.c index fb64cd6..ce0f8c5 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_get_msg/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_get_msg/main.c @@ -1,6 +1,6 @@ #include -#include -#include +#include "trusty_ipc.h" +#include "uapi/err.h" /* Documentation from trusty API: get_msg() Gets meta-information about the next message in an incoming message queue diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_put_msg/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_put_msg/main.c index f39b9e1..3646e8a 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_put_msg/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_put_msg/main.c @@ -1,6 +1,6 @@ #include -#include -#include +#include "trusty_ipc.h" +#include "uapi/err.h" /* Documentation from trusty API: put_msg() Retires a message with a specified ID. diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_read_msg/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_read_msg/main.c index 6dc5a98..d4b269c 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_read_msg/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_read_msg/main.c @@ -1,6 +1,6 @@ #include -#include -#include +#include "trusty_ipc.h" +#include "uapi/err.h" /* Documentation from trusty API: read_msg() Reads the content of the message with the specified ID starting from the diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_send_msg/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_send_msg/main.c index f906ff0..1b9fc1e 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_send_msg/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_send_msg/main.c @@ -1,6 +1,6 @@ #include -#include -#include +#include "trusty_ipc.h" +#include "uapi/err.h" /* Documentation from trusty API: send_msg() Sends a message over a specified channel. diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_set_cookie/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_set_cookie/main.c index 2af61ff..9b9ec85 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_set_cookie/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_set_cookie/main.c @@ -1,6 +1,6 @@ #include -#include -#include +#include "trusty_ipc.h" +#include "uapi/err.h" typedef void (*event_handler_proc_t)(const uevent_t* ev, void* ctx); diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_wait/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_wait/main.c index 7f6aff0..4a67353 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_wait/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_wait/main.c @@ -1,6 +1,6 @@ #include -#include -#include +#include "trusty_ipc.h" +#include "uapi/err.h" int main(void) { diff --git a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_wait_any/main.c b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_wait_any/main.c index 863f8c3..ba67b27 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/proof/port_wait_any/main.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/proof/port_wait_any/main.c @@ -1,6 +1,6 @@ #include -#include -#include +#include "trusty_ipc.h" +#include "uapi/err.h" int main(void) { diff --git a/seahorn/trusty/user/base/lib/libc-trusty/trusty_syscalls_impl.c b/seahorn/trusty/user/base/lib/libc-trusty/trusty_syscalls_impl.c index 03d1ecb..162ca94 100644 --- a/seahorn/trusty/user/base/lib/libc-trusty/trusty_syscalls_impl.c +++ b/seahorn/trusty/user/base/lib/libc-trusty/trusty_syscalls_impl.c @@ -1,7 +1,7 @@ #include "sea_handle_table.h" #include "trusty_syscalls.h" -#include // trusty errors definitions +#include "uapi/err.h" // trusty errors definitions #include diff --git a/seahorn/trusty_common/include/handle_table.h b/seahorn/trusty_common/include/handle_table.h index 389d675..7ed783b 100644 --- a/seahorn/trusty_common/include/handle_table.h +++ b/seahorn/trusty_common/include/handle_table.h @@ -1,5 +1,5 @@ #pragma once -#include "seahorn/seahorn.h" +#include #include #include diff --git a/seahorn/trusty_common/lib/CMakeLists.txt b/seahorn/trusty_common/lib/CMakeLists.txt index 678928a..4f6a999 100644 --- a/seahorn/trusty_common/lib/CMakeLists.txt +++ b/seahorn/trusty_common/lib/CMakeLists.txt @@ -1,11 +1,21 @@ # proof helpers -add_library(sea_common_proofs - handle_table.c - nondet.c - bcmp.c -) - -if(SEA_ALLOCATOR_CAN_FAIL) - target_compile_definitions(sea_common_proofs PRIVATE SEA_ALLOCATOR_CAN_FAIL) +if (HANDLE_TYPE_IS_PTR) + add_library(sea_common_proofs + handle_table_ptr.c + nondet.c + bcmp.c + ) + if(SEA_ALLOCATOR_CAN_FAIL) + target_compile_definitions(sea_common_proofs PRIVATE SEA_ALLOCATOR_CAN_FAIL) + endif() +else() + add_library(sea_common_proofs + handle_table.c + nondet.c + bcmp.c + ) + if(SEA_ALLOCATOR_CAN_FAIL) + target_compile_definitions(sea_common_proofs PRIVATE SEA_ALLOCATOR_CAN_FAIL) + endif() endif() sea_attach_bc(sea_common_proofs) diff --git a/seahorn/trusty_common/lib/handle_table_ptr.c b/seahorn/trusty_common/lib/handle_table_ptr.c new file mode 100644 index 0000000..a3d7f10 --- /dev/null +++ b/seahorn/trusty_common/lib/handle_table_ptr.c @@ -0,0 +1,45 @@ +/** +Channel and Port Handles. + +A channel/port is active if a handle is registered for it. +*/ +#include "handle_table.h" +#include "sea_handle_table.h" +#include +#include + +void handle_table_init(handle_t secure_port, handle_t non_secure_port, handle_t channel) { + +} + +unsigned int is_port_handle(handle_t handle) { + return handle->type == port; +} + +unsigned int is_secure_handle(handle_t handle) { + return handle->secure == true; +} + + +#define IS_PORT_HANDLE(h) is_port_handle(h) +#define IS_SECURE_HANDLE(h) is_port_handle(h) +void add_handle(handle_t handle) { + handle->active = true; +} + +void remove_handle(handle_t handle) { + handle->active = false; +} + +bool contains_handle(handle_t handle) { + return sea_contains_handle(handle); +} + +void *get_handle_cookie(handle_t handle) { + return handle->cookie; +} + +void set_handle_cookie(handle_t handle, void *cookie) { + handle->cookie = cookie; +} + diff --git a/seahorn/trusty_common/stubs/CMakeLists.txt b/seahorn/trusty_common/stubs/CMakeLists.txt index 2a618ca..b69f1db 100644 --- a/seahorn/trusty_common/stubs/CMakeLists.txt +++ b/seahorn/trusty_common/stubs/CMakeLists.txt @@ -14,4 +14,4 @@ add_library(time_override time_override.c) sea_attach_bc(time_override) add_library(new_delete_override new_delete_override.cpp) -sea_attach_bc_cc(new_delete_override) \ No newline at end of file +sea_attach_bc_cc(new_delete_override) diff --git a/trusty_mod/trusty/user/app/storage/ipc.c b/trusty_mod/trusty/user/app/storage/ipc.c new file mode 100644 index 0000000..93fda00 --- /dev/null +++ b/trusty_mod/trusty/user/app/storage/ipc.c @@ -0,0 +1,447 @@ +/* + * Copyright (C) 2015 The Android Open Source Project + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +#include +#include +#include +#include +#include +#include + +#include "ipc.h" + +#define MSG_BUF_MAX_SIZE 4096 + +#define TLOG_TAG "ss-ipc" + +static void* msg_buf; +static size_t msg_buf_size; + +static void handle_channel(struct ipc_context* ctx, const struct uevent* ev); +static void handle_port(struct ipc_context* ctx, const struct uevent* ev); + +static int maybe_grow_msg_buf(size_t new_max_size) { + if (new_max_size > msg_buf_size) { + uint8_t* tmp = realloc(msg_buf, new_max_size); + if (tmp == NULL) { + return ERR_NO_MEMORY; + } + msg_buf = tmp; + msg_buf_size = new_max_size; + } + return NO_ERROR; +} + +static inline void handle_port_errors(const uevent_t* ev) { + if ((ev->event & IPC_HANDLE_POLL_ERROR) || + (ev->event & IPC_HANDLE_POLL_HUP) || + (ev->event & IPC_HANDLE_POLL_MSG) || + (ev->event & IPC_HANDLE_POLL_SEND_UNBLOCKED)) { + /* should never happen with port handles */ + TLOGE("error event (0x%x) for port (%p)\n", ev->event, ev->handle); + abort(); + } +} + +static inline void handle_chan_errors(const uevent_t* ev) { + if ((ev->event & IPC_HANDLE_POLL_ERROR) || + (ev->event & IPC_HANDLE_POLL_READY)) { + TLOGE("error event (0x%x) for chan (%p)\n", ev->event, ev->handle); + abort(); + } +} + +static int is_valid_port_ops(struct ipc_port_ops* ops) { + return (ops->on_connect != NULL); +} + +static bool is_valid_chan_ops(struct ipc_channel_ops* ops) { + return (ops->on_disconnect != NULL); +} + +static struct ipc_port_context* to_port_context(struct ipc_context* context) { + assert(context); + return containerof(context, struct ipc_port_context, common); +} + +static struct ipc_channel_context* to_channel_context( + struct ipc_context* context) { + assert(context); + return containerof(context, struct ipc_channel_context, common); +} + +static int do_connect(struct ipc_port_context* ctx, const uevent_t* ev) { + int rc; + handle_t rc1; + handle_t chan_handle; + struct ipc_channel_context* chan_ctx; + + if (ev->event & IPC_HANDLE_POLL_READY) { + /* incoming connection: accept it */ + uuid_t peer_uuid; + rc1 = accept(ev->handle, &peer_uuid); + if (rc1 == INVALID_IPC_HANDLE) { + TLOGE("failed (%p) to accept on port %p\n", rc1, ev->handle); + return rc; + } + + chan_handle = (handle_t)rc1; + + chan_ctx = ctx->ops.on_connect(ctx, &peer_uuid, chan_handle); + if (chan_ctx == NULL) { + TLOGE("%s: failure initializing channel state (%p)\n", __func__, + rc1); + rc = ERR_GENERIC; + goto err_on_connect; + } + + assert(is_valid_chan_ops(&chan_ctx->ops)); + + chan_ctx->common.evt_handler = handle_channel; + chan_ctx->common.handle = chan_handle; + + rc = set_cookie(chan_handle, chan_ctx); + if (rc < 0) { + TLOGE("failed (%d) to set_cookie on chan %p\n", rc, chan_handle); + goto err_set_cookie; + } + list_add_tail(&ctx->channels, &chan_ctx->node); + } + + return NO_ERROR; + +err_set_cookie: + chan_ctx->ops.on_disconnect(chan_ctx); +err_on_connect: + close(chan_handle); + return rc; +} + +static int do_handle_msg(struct ipc_channel_context* ctx, const uevent_t* ev) { + handle_t chan = ev->handle; + + /* get message info */ + ipc_msg_info_t msg_inf; + int rc = get_msg(chan, &msg_inf); + if (rc == ERR_NO_MSG) + return NO_ERROR; /* no new messages */ + + if (rc != NO_ERROR) { + TLOGE("failed (%d) to get_msg for chan (%p), closing connection\n", rc, + chan); + return rc; + } + + if (msg_inf.len > MSG_BUF_MAX_SIZE) { + TLOGE("%s: message too large %zu\n", __func__, msg_inf.len); + put_msg(chan, msg_inf.id); + return ERR_NOT_ENOUGH_BUFFER; + } + + /* read msg content */ + struct iovec iov = { + .iov_base = msg_buf, + .iov_len = msg_inf.len, + }; + ipc_msg_t msg = { + .iov = &iov, + .num_iov = 1, + }; + + rc = read_msg(chan, msg_inf.id, 0, &msg); + put_msg(chan, msg_inf.id); + if (rc < 0) { + TLOGE("failed to read msg (%d, %p)\n", rc, chan); + return rc; + } + + if (((size_t)rc) < msg_inf.len) { + TLOGE("invalid message of size (%d, %p)\n", rc, chan); + return ERR_NOT_VALID; + } + + rc = ctx->ops.on_handle_msg(ctx, msg_buf, msg_inf.len); + +err_handle_msg: +err_read_msg: + return rc; +} + +static void do_disconnect(struct ipc_channel_context* context, + const uevent_t* ev) { + list_delete(&context->node); + context->ops.on_disconnect(context); + close(ev->handle); +} + +static void handle_port(struct ipc_context* ctx, const struct uevent* ev) { + struct ipc_port_context* port_ctx = to_port_context(ctx); + assert(is_valid_port_ops(&port_ctx->ops)); + + handle_port_errors(ev); + + do_connect(port_ctx, ev); +} + +static void handle_channel(struct ipc_context* ctx, const struct uevent* ev) { + struct ipc_channel_context* channel_ctx = to_channel_context(ctx); + assert(is_valid_chan_ops(&channel_ctx->ops)); + + handle_chan_errors(ev); + + if (ev->event & IPC_HANDLE_POLL_MSG) { + if (channel_ctx->ops.on_handle_msg != NULL) { + int rc = do_handle_msg(channel_ctx, ev); + if (rc < 0) { + TLOGE("error (%d) in channel, disconnecting " + "peer\n", + rc); + do_disconnect(channel_ctx, ev); + return; + } + } else { + TLOGE("error: unexpected message in channel (%p). closing...\n", + ev->handle); + do_disconnect(channel_ctx, ev); + return; + } + } + + if (ev->event & IPC_HANDLE_POLL_HUP) { + do_disconnect(channel_ctx, ev); + } +} + +static int read_response(handle_t session, + uint32_t msg_id, + struct iovec* iovecs, + size_t iovec_count) { + struct ipc_msg rx_msg = { + .iov = iovecs, + .num_iov = iovec_count, + }; + + long rc = read_msg(session, msg_id, 0, &rx_msg); + put_msg(session, msg_id); + if (rc < 0) { + TLOGE("%s: failed to read msg (%ld)\n", __func__, rc); + return rc; + } + + size_t read_size = (size_t)rc; + return read_size; +} + +static int await_response(handle_t session, struct ipc_msg_info* inf) { + uevent_t uevt; + long rc = wait(session, &uevt, INFINITE_TIME); + if (rc != NO_ERROR) { + TLOGE("%s: interrupted waiting for response (%ld)", __func__, rc); + return rc; + } + + rc = get_msg(session, inf); + if (rc != NO_ERROR) { + TLOGE("%s: failed to get_msg (%ld)\n", __func__, rc); + } + + return rc; +} + +static int wait_to_send(handle_t session, struct ipc_msg* msg) { + int rc; + struct uevent ev = UEVENT_INITIAL_VALUE(ev); + + rc = wait(session, &ev, INFINITE_TIME); + if (rc < 0) { + TLOGE("failed to wait for outgoing queue to free up\n"); + return rc; + } + + if (ev.event & IPC_HANDLE_POLL_SEND_UNBLOCKED) { + return send_msg(session, msg); + } + + if (ev.event & IPC_HANDLE_POLL_MSG) { + return ERR_BUSY; + } + + if (ev.event & IPC_HANDLE_POLL_HUP) { + return ERR_CHANNEL_CLOSED; + } + + return rc; +} + +int sync_ipc_send_msg(handle_t session, + struct iovec* tx_iovecs, + unsigned int tx_iovec_count, + struct iovec* rx_iovecs, + unsigned int rx_iovec_count) { + struct ipc_msg tx_msg = { + .iov = tx_iovecs, + .num_iov = tx_iovec_count, + }; + + long rc = send_msg(session, &tx_msg); + if (rc == ERR_NOT_ENOUGH_BUFFER) { + rc = wait_to_send(session, &tx_msg); + } + + if (rc < 0) { + TLOGE("%s: failed (%ld) to send_msg\n", __func__, rc); + return rc; + } + + if (rx_iovecs == NULL || rx_iovec_count == 0) { + assert(rx_iovec_count == 0); + assert(rx_iovecs == NULL); + return NO_ERROR; + } + + struct ipc_msg_info inf; + rc = await_response(session, &inf); + if (rc < 0) { + TLOGE("%s: failed (%ld) to await response\n", __func__, rc); + return rc; + } + + size_t min_len = rx_iovecs[0].iov_len; + if (inf.len < min_len) { + TLOGE("%s: invalid response length (%zu)\n", __func__, inf.len); + put_msg(session, inf.id); + return ERR_NOT_VALID; + } + + /* calculate total message size */ + size_t resp_size = 0; + for (size_t i = 0; i < rx_iovec_count; ++i) { + resp_size += rx_iovecs[i].iov_len; + } + + if (resp_size < inf.len) { + TLOGE("%s: response buffer too short (%zu < %zu) \n", __func__, + resp_size, inf.len); + put_msg(session, inf.id); + return ERR_BAD_LEN; + } + + rc = read_response(session, inf.id, rx_iovecs, rx_iovec_count); + put_msg(session, inf.id); + if (rc < 0) { + TLOGE("%s: response has error (%ld)\n", __func__, rc); + return rc; + } + + size_t read_len = (size_t)rc; + if (read_len != inf.len) { + // data read in does not match message length + TLOGE("%s: invalid response length (%zu)\n", __func__, read_len); + return ERR_IO; + } + + return read_len; +} + +static void dispatch_event(const uevent_t* ev) { + assert(ev); + + if (ev->event == IPC_HANDLE_POLL_NONE) { + return; + } + + struct ipc_context* context = ev->cookie; + assert(context); + assert(context->evt_handler); + assert(context->handle == ev->handle); + + context->evt_handler(context, ev); +} + +int ipc_port_create(struct ipc_port_context* ctxp, + const char* port_name, + size_t queue_size, + size_t max_buffer_size, + uint32_t flags) { + int rc; + handle_t rc1; + assert(ctxp); + assert(is_valid_port_ops(&ctxp->ops)); + + rc1 = port_create(port_name, queue_size, max_buffer_size, flags); + if (rc1 == INVALID_IPC_HANDLE) { + TLOGE("Failed to create port %s %p\n", port_name, rc1); + return -1; + } + + handle_t port_handle = (handle_t)rc1; + rc = set_cookie(port_handle, ctxp); + if (rc < 0) { + TLOGE("Failed to set cookie on port %s (%d)\n", port_name, rc); + goto err_set_cookie; + } + + rc = maybe_grow_msg_buf(max_buffer_size); + if (rc < 0) { + TLOGE("Failed to create msg buffer of size %zu (%d)\n", max_buffer_size, + rc); + goto err_grow_msg; + } + + ctxp->common.handle = port_handle; + ctxp->common.evt_handler = handle_port; + list_initialize(&ctxp->channels); + return NO_ERROR; + +err_set_cookie: +err_grow_msg: + close(port_handle); + return rc; +} + +int ipc_port_destroy(struct ipc_port_context* ctx) { + close(ctx->common.handle); + while (!list_is_empty(&ctx->channels)) { + struct ipc_channel_context* chan_ctx = list_remove_head_type( + &ctx->channels, struct ipc_channel_context, node); + assert(chan_ctx); + handle_t chan_handle = chan_ctx->common.handle; + TLOGE("client still connected, handle %p\n", chan_handle); + chan_ctx->ops.on_disconnect(chan_ctx); + close(chan_handle); + } + return NO_ERROR; +} + +void ipc_loop(void) { + int rc; + uevent_t event; + + while (true) { + event.handle = INVALID_IPC_HANDLE; + event.event = 0; + event.cookie = NULL; + rc = wait_any(&event, INFINITE_TIME); + if (rc < 0) { + TLOGE("wait_any failed (%d)\n", rc); + break; + } + + if (rc == NO_ERROR) { /* got an event */ + dispatch_event(&event); + } + } +} diff --git a/trusty_mod/trusty/user/base/include/user/AUTHORS b/trusty_mod/trusty/user/base/include/user/AUTHORS new file mode 100644 index 0000000..8385e13 --- /dev/null +++ b/trusty_mod/trusty/user/base/include/user/AUTHORS @@ -0,0 +1,10 @@ +# This is the official list of LK Trusty authors for copyright purposes. +# This file is distinct from the CONTRIBUTORS files. +# See the latter for an explanation. + +# Names should be added to this file as: +# Name or Organization +# The email address is not required for organizations. + +Google Inc. +NVIDIA CORPORATION. diff --git a/trusty_mod/trusty/user/base/include/user/LICENSE b/trusty_mod/trusty/user/base/include/user/LICENSE new file mode 100644 index 0000000..2df4ba7 --- /dev/null +++ b/trusty_mod/trusty/user/base/include/user/LICENSE @@ -0,0 +1,21 @@ +Copyright (c) 2012-2015 LK Trusty Authors. All Rights Reserved. + +Permission is hereby granted, free of charge, to any person obtaining +a copy of this software and associated documentation files +(the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, +publish, distribute, sublicense, and/or sell copies of the Software, +and to permit persons to whom the Software is furnished to do so, +subject to the following conditions: + +The above copyright notice and this permission notice shall be +included in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, +EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + diff --git a/trusty_mod/trusty/user/base/include/user/trusty_app_manifest.h b/trusty_mod/trusty/user/base/include/user/trusty_app_manifest.h new file mode 100644 index 0000000..a2fe996 --- /dev/null +++ b/trusty_mod/trusty/user/base/include/user/trusty_app_manifest.h @@ -0,0 +1,62 @@ +/* + * Copyright (c) 2013, Google, Inc. All rights reserved + * Copyright (c) 2012-2013, NVIDIA CORPORATION. All rights reserved + * + * Permission is hereby granted, free of charge, to any person obtaining + * a copy of this software and associated documentation files + * (the "Software"), to deal in the Software without restriction, + * including without limitation the rights to use, copy, modify, merge, + * publish, distribute, sublicense, and/or sell copies of the Software, + * and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. + * IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY + * CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, + * TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE + * SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ +#pragma once + +#include +#include + +/* + * Layout of .trusty_app.manifest section in the trusted application is the + * required UUID followed by an abitrary number of configuration options. + */ +#define CONCAT(x, y) x##y +#define XCONCAT(x, y) CONCAT(x, y) + +#define TRUSTY_APP_CONFIG_MIN_STACK_SIZE(sz) \ + TRUSTY_APP_CONFIG_KEY_MIN_STACK_SIZE, sz + +#define TRUSTY_APP_CONFIG_MIN_HEAP_SIZE(sz) \ + TRUSTY_APP_CONFIG_KEY_MIN_HEAP_SIZE, sz + +#define TRUSTY_APP_CONFIG_MAP_MEM(id, off, sz) \ + TRUSTY_APP_CONFIG_KEY_MAP_MEM, id, off, sz + +#define TRUSTY_APP_CONFIG_MGMT_FLAGS(mgmt_flags) \ + TRUSTY_APP_CONFIG_KEY_MGMT_FLAGS, mgmt_flags + +/* Valid flags: IPC_PORT_ALLOW_* */ +#define TRUSTY_APP_START_PORT(name, flags) \ + struct trusty_app_manifest_entry_port \ + __attribute((section(".trusty_app.manifest.entry"))) \ + XCONCAT(trusty_app_manifest_entry_port_, __COUNTER__) = { \ + .config_key = TRUSTY_APP_CONFIG_KEY_START_PORT, \ + .port_flags = flags, \ + .port_name_size = sizeof(name), \ + .port_name = name, \ + }; + +/* manifest section attributes */ +#define TRUSTY_APP_MANIFEST_ATTRS \ + const __attribute((aligned(4))) \ + __attribute((section(".trusty_app.manifest"))) diff --git a/trusty_mod/trusty/user/base/include/user/trusty_err.h b/trusty_mod/trusty/user/base/include/user/trusty_err.h new file mode 100644 index 0000000..809fb4e --- /dev/null +++ b/trusty_mod/trusty/user/base/include/user/trusty_err.h @@ -0,0 +1,23 @@ +/* + * Copyright (C) 2020 The Android Open Source Project + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +#pragma once + +#include +#include + +int lk_err_to_errno(int lk_err); +int errno_to_lk_err(int err); diff --git a/trusty_mod/trusty/user/base/include/user/trusty_ipc.h b/trusty_mod/trusty/user/base/include/user/trusty_ipc.h new file mode 100644 index 0000000..454076f --- /dev/null +++ b/trusty_mod/trusty/user/base/include/user/trusty_ipc.h @@ -0,0 +1,158 @@ +/* + * Copyright (c) 2013 Google Inc. All rights reserved + * + * Permission is hereby granted, free of charge, to any person obtaining + * a copy of this software and associated documentation files + * (the "Software"), to deal in the Software without restriction, + * including without limitation the rights to use, copy, modify, merge, + * publish, distribute, sublicense, and/or sell copies of the Software, + * and to permit persons to whom the Software is furnished to do so, + * subject to the following conditions: + * + * The above copyright notice and this permission notice shall be + * included in all copies or substantial portions of the Software. + * + * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, + * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF + * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. + * IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY + * CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, + * TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE + * SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + */ + +#pragma once + +#include +#include +#include +#include +#include +#include + +__BEGIN_CDECLS + +typedef struct _handleState { + bool active; + bool secure; + enum Type { + port, + channel, + } type; + void* cookie; + const char* path; + struct Msg { + unsigned int id; + size_t len; + } msg; +} HandleState; + + +/* + * handle_t is an opaque 32 bit value that is used to reference an + * object (like ipc port or channel) in kernel space + */ +typedef HandleState* handle_t; + +/* + * Invalid IPC handle + */ +#define INVALID_IPC_HANDLE NULL + +/* + * Specify this timeout value to wait forever. + */ +#define INFINITE_TIME UINT32_MAX + +/* + * Combination of these flags sets additional options + * for port_create syscall. + */ +enum { + /* allow Trusted Apps to connect to this port */ + IPC_PORT_ALLOW_TA_CONNECT = 0x1, + /* allow non-secure clients to connect to this port */ + IPC_PORT_ALLOW_NS_CONNECT = 0x2, +}; + +/* + * Options for connect syscall + */ +enum { + IPC_CONNECT_WAIT_FOR_PORT = 0x1, + IPC_CONNECT_ASYNC = 0x2, +}; + +/* + * IPC message + */ +typedef struct ipc_msg { + uint32_t num_iov; + struct iovec* iov; + + uint32_t num_handles; + handle_t* handles; +} ipc_msg_t; + +typedef struct ipc_msg_info { + size_t len; + uint32_t id; + uint32_t num_handles; +} ipc_msg_info_t; + +/* + * Combination of these values is used for event field + * ot uevent_t structure. + */ +enum { + IPC_HANDLE_POLL_NONE = 0x0, + IPC_HANDLE_POLL_READY = 0x1, + IPC_HANDLE_POLL_ERROR = 0x2, + IPC_HANDLE_POLL_HUP = 0x4, + IPC_HANDLE_POLL_MSG = 0x8, + IPC_HANDLE_POLL_SEND_UNBLOCKED = 0x10, +}; + +/* + * Values for cmd parameter of handle_set_ctrl call + */ +enum { + HSET_ADD = 0x0, /* adds new handle to handle set */ + HSET_DEL = 0x1, /* deletes handle from handle set */ + HSET_MOD = 0x2, /* modifies handle attributes in handle set */ +}; + +/* + * Is used by wait and wait_any calls to return information + * about event. + */ +typedef struct uevent { + handle_t handle; /* handle this event is related too */ + uint32_t event; /* combination of IPC_HANDLE_POLL_XXX flags */ + void* cookie; /* cookie aasociated with handle */ +} uevent_t; + +#define UEVENT_INITIAL_VALUE(event) \ + { 0, 0, 0 } + +handle_t port_create(const char* path, + uint32_t num_recv_bufs, + uint32_t recv_buf_size, + uint32_t flags); +handle_t connect(const char* path, uint32_t flags); +handle_t accept(handle_t handle, uuid_t* peer_uuid); +int close(handle_t handle); +int set_cookie(handle_t handle, void* cookie); +handle_t handle_set_create(void); +int handle_set_ctrl(handle_t handle, uint32_t cmd, struct uevent* evt); +int wait(handle_t handle, uevent_t* event, uint32_t timeout_msecs); +int wait_any(uevent_t* event, uint32_t timeout_msecs); +int get_msg(handle_t handle, ipc_msg_info_t* msg_info); +ssize_t read_msg(handle_t handle, + uint32_t msg_id, + uint32_t offset, + ipc_msg_t* msg); +int put_msg(handle_t handle, uint32_t msg_id); +ssize_t send_msg(handle_t handle, ipc_msg_t* msg); + +__END_CDECLS diff --git a/trusty_mod/trusty/user/base/include/user/trusty_log.h b/trusty_mod/trusty/user/base/include/user/trusty_log.h new file mode 100644 index 0000000..3165883 --- /dev/null +++ b/trusty_mod/trusty/user/base/include/user/trusty_log.h @@ -0,0 +1,100 @@ +/* + * Copyright (C) 2018 The Android Open Source Project + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +#pragma once + +#include +#include + +#define TLOG_LVL_NONE 0 +#define TLOG_LVL_CRIT 1 +#define TLOG_LVL_ERROR 2 +#define TLOG_LVL_WARN 3 +#define TLOG_LVL_INFO 4 +#define TLOG_LVL_DEBUG 5 + +#ifndef TLOG_LVL +#ifdef TLOG_LVL_DEFAULT +#define TLOG_LVL TLOG_LVL_DEFAULT +#else +#define TLOG_LVL TLOG_LVL_INFO +#endif +#endif + +__BEGIN_CDECLS + +#ifdef TRUSTY_USERSPACE + +/* Defined in libc and libunittest, whichever is statically linked first will be + * used, so libunittest must always come before libc in the link order. */ +int _tlog(const char* fmt, ...) __PRINTFLIKE(1, 2); + +#else + +/* TLOG is also called from host code, where we don't provide a definition of + * _tlog. In this case, just printf */ +#define _tlog(fmt, ...) \ + do { \ + fprintf(stderr, fmt, ##__VA_ARGS__); \ + } while (0) +#endif + +__END_CDECLS + +#define TLOG(fmt, ...) \ + do { \ + _tlog("%s: %d: " fmt, TLOG_TAG, __LINE__, ##__VA_ARGS__); \ + } while (0) + +/* debug */ +#define TLOGD(x...) \ + do { \ + if (TLOG_LVL >= TLOG_LVL_DEBUG) { \ + TLOG(x); \ + } \ + } while (0) + +/* info */ +#define TLOGI(x...) \ + do { \ + if (TLOG_LVL >= TLOG_LVL_INFO) { \ + TLOG(x); \ + } \ + } while (0) + +/* warning */ +#define TLOGW(x...) \ + do { \ + if (TLOG_LVL >= TLOG_LVL_WARN) { \ + TLOG(x); \ + } \ + } while (0) + +/* error */ +#define TLOGE(x...) \ + do { \ + if (TLOG_LVL >= TLOG_LVL_ERROR) { \ + TLOG(x); \ + } \ + } while (0) + +/* critical */ +#define TLOGC(x...) \ + do { \ + if (TLOG_LVL >= TLOG_LVL_CRIT) { \ + TLOG(x); \ + } \ + } while (0) diff --git a/trusty_mod/trusty/user/base/include/user/trusty_uio.h b/trusty_mod/trusty/user/base/include/user/trusty_uio.h new file mode 100644 index 0000000..f4d8c10 --- /dev/null +++ b/trusty_mod/trusty/user/base/include/user/trusty_uio.h @@ -0,0 +1,31 @@ +/* + * Copyright (C) 2020 The Android Open Source Project + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +#pragma once + +#include +#include "trusty_err.h" + +/* + * The following routines are functionally equivalent to libc read{v}/write{v} + * except how an error condition is handled. On error: + * read{v}/write{v} returns -1 and sets errno + * trusty_read(v)/trusty_write{v} return negative LK error instead + */ +ssize_t trusty_readv(int fd, const struct iovec* iov, int iovcnt); +ssize_t trusty_read(int fd, void* buf, size_t count); +ssize_t trusty_writev(int fd, const struct iovec* iov, int iovcnt); +ssize_t trusty_write(int fd, const void* buf, size_t count); diff --git a/trusty_mod/trusty/user/base/include/user/trusty_unittest.h b/trusty_mod/trusty/user/base/include/user/trusty_unittest.h new file mode 100644 index 0000000..76384b0 --- /dev/null +++ b/trusty_mod/trusty/user/base/include/user/trusty_unittest.h @@ -0,0 +1,30 @@ +/* + * Copyright (C) 2014-2015 The Android Open Source Project + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +#pragma once + +#include "trusty_log.h" + +#define trusty_unittest_printf(args...) \ + do { \ + _tlog(args); \ + } while (0) + +#include + +#ifdef TRUSTY_USERSPACE +#include +#endif