-
Notifications
You must be signed in to change notification settings - Fork 4
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(handle_t): redef handle_t as pointer #16
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
storage_ipc_indirect_handlers_unsat_test | ||
storage_ipc_msg_buffer_unsat_test | ||
gatekeeper_ipc_unsat_test | ||
# following tracked in https://github.com/seahorn/verifyTrusty/issues/18 | ||
storage_ipc_port_create_destroy_unsat_test | ||
# following tracked in https://github.com/seahorn/verifyTrusty/issues/19 | ||
port_send_msg_pf_unsat_test |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
storage_ipc_indirect_handlers_unsat_test | ||
storage_ipc_msg_buffer_unsat_test | ||
gatekeeper_ipc_unsat_test |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1 +1 @@ | ||
add_subdirectory(user/base/lib/libc-trusty) | ||
add_subdirectory(user/base/lib) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. are there multiple conflicting compiler definitions? Are you assuming they are resolved somehow by CMake or by the compiler? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. In the original spec (impl), some jobs are written assuming a valid There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I noticed that this definition is added multiple times in different CMakeLists.txt files. I am asking how the exclusivity of which definition is active is maintained. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. The short answer is that exclusivity is maintained by user discipline. Each directory of jobs is independent of other jobs hence there should not be a conflict. -- Changing the compilation model seems out of scope in this PR. |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,53 @@ | ||
#include "trusty_ipc.h" | ||
#include <seahorn/seahorn.h> | ||
|
||
/* Documentation from trusty API: | ||
accept() | ||
Accepts an incoming connection and gets a handle to a channel. | ||
long accept(uint32_t handle_id, uuid_t *peer_uuid); | ||
[in] handle_id: Handle representing the port to which a client has connected | ||
[out] peer_uuid: Pointer to a uuud_t structure to be filled with the UUID of | ||
the connecting client application. It will be set to all zeros if the | ||
connection originated from the non-secure world. | ||
[retval]: Handle to a channel (if non-negative) on which the server can exchange | ||
messages with the client (or an error code otherwise) | ||
*/ | ||
|
||
const char *HANDLE_PATH = "seahorn.com"; | ||
|
||
bool is_uuid_all_zeros(uuid_t *peer_uuid) { | ||
return peer_uuid->time_low == 0 && peer_uuid->time_mid == 0 && | ||
peer_uuid->time_hi_and_version == 0; | ||
} | ||
|
||
int main(void) { | ||
|
||
handle_t port; | ||
int rc; | ||
|
||
port = port_create(HANDLE_PATH, 1, 100, | ||
IPC_PORT_ALLOW_NS_CONNECT | IPC_PORT_ALLOW_TA_CONNECT); | ||
|
||
// -- got expected handle | ||
sassert(!port->secure); | ||
|
||
uuid_t peer_uuid; | ||
handle_t chan; | ||
chan = accept(port, &peer_uuid); | ||
assume(chan != INVALID_IPC_HANDLE); | ||
sassert(is_uuid_all_zeros(&peer_uuid)); | ||
|
||
rc = close(port); | ||
sassert(rc == 0); | ||
|
||
port = port_create(HANDLE_PATH, 1, 100, IPC_PORT_ALLOW_NS_CONNECT); | ||
|
||
// -- expected secure handle handle | ||
sassert(port->secure); | ||
|
||
chan = accept(port, &peer_uuid); | ||
assume(chan != INVALID_IPC_HANDLE); | ||
return 0; | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@priyasiddharth you can also add
HANDLE_TYPE_IS_PTR
to definitions using CMakeadd_definitions
command and then use it as#ifdef
inside header files. This might be simpler than changing include directories with cmake.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A simple solution would delegate the decision to each include point and would duplicate the conditional for evey use. A more complex solution would be to have a wrapper header which makes the decision internally. It's not clear why that's needed for now.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I was suggesting a wrapper header, simply because this is the typical way to address this problem. This guarantees less unexpected issues later on.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
We discussed this in https://seahornteam.slack.com/archives/DPND2KEJU/p1659124357825129.
conclusion: to use wrap header file you would need to merge common files rather than have two completely different source trees
This requires adding more moving pieces to the build and IMO is overkill for now. My vote is to submit this PR and revisit this if it needs more engineering to make it robust -- once it moves beyond being a proof of concept.