diff --git a/README.md b/README.md index 1f77144..47b397f 100644 --- a/README.md +++ b/README.md @@ -14,6 +14,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener The Copland Virtual Machine (CVM) is a Rocq library that formalizes a virtual machine for the Copland Domain Specific Language for layered remote attestation. +*NOTE*: The CVM expects to communicate with ASP's via a fork/exec style where the ASP is launched, reads input from stdin, and writes output to stdout. Utilizing the [`rust-am-lib`](https://github.com/ku-sldg/rust-am-lib) version 0.3.0 and greater should be sufficient to meet these requirements. The CVM does not currently support any other style of communication with ASP's, but support for additional styles may be added in the future. + ## Meta - Author(s): diff --git a/meta.yml b/meta.yml index c26d19c..96a0acb 100644 --- a/meta.yml +++ b/meta.yml @@ -10,7 +10,7 @@ authors: - name: "Will Thomas" email: "30wthomas@ku.edu" opam-file-maintainer: "30wthomas@ku.edu" # Need a strong default here or we will accidentally email a Coq developer -opam-file-version: "0.1.2" +opam-file-version: "0.2.0" ###################################################### # NOTE: Optional Extra Info diff --git a/rocq-cvm.opam b/rocq-cvm.opam index b2338c3..9730279 100644 --- a/rocq-cvm.opam +++ b/rocq-cvm.opam @@ -3,7 +3,7 @@ opam-version: "2.0" maintainer: "30wthomas@ku.edu" -version: "0.1.2" +version: "0.2.0" homepage: "https://github.com/ku-sldg/cvm" dev-repo: "git+https://github.com/ku-sldg/cvm.git" diff --git a/stubs/FFI/SysFFI.cml b/stubs/FFI/SysFFI.cml index 8fead1b..3eb9278 100644 --- a/stubs/FFI/SysFFI.cml +++ b/stubs/FFI/SysFFI.cml @@ -5,29 +5,35 @@ structure SysFFI = struct local fun ffi_system x y = #(system) x y - fun ffi_popen_string x y = #(popen_string) x y + fun ffi_exec_process_io x y = #(exec_process_io) x y in - fun escFn c = - case Char.ord c of - 8 => "\\b" - | 9 => "\\t" - | 10 => "\\n" - | 12 => "\\f" - | 13 => "\\r" - | 34 => "\\\"" - | _ => String.str c - - fun shellEscapeString str = - String.concat (List.map escFn (String.explode str)) - - (* () -> string *) - fun c_popen_string (com) = - let val command_bs = BString.fromString com - val resp_bs = FFI.buffered_call ffi_popen_string command_bs + (** + * c_exec_process_io: Spawn a process and communicate via stdin/stdout. + * + * The process at `process` is executed directly via fork/exec. + * `arg_str` is written to the process's stdin, then stdin is closed + * (sending EOF). The process's stdout is read and returned. + * + * Input encoding sent to FFI: + * [ ProcessPathLength : 4 bytes (big-endian) ; + * ProcessPath : ProcessPathLength bytes ; + * ArgString : remaining bytes ] + * + * @param process Absolute path to the executable + * @param arg_str String to write to the process's stdin + * @return The process's stdout output as a string + *) + fun c_exec_process_io (process : string) (arg_str : string) = + let val process_bs = BString.fromString process + val process_len_bs = BString.int_to_qword (BString.length process_bs) + val arg_bs = BString.fromString arg_str + val payload = BString.concat (BString.concat process_len_bs process_bs) arg_bs + val resp_bs = FFI.buffered_call ffi_exec_process_io payload in BString.toString resp_bs end - handle _ => raise (Exception "Unknown Error thrown from c_popen_string, likely check that the word8 array is right length that is expected and not accessing something outside of its bounds") + handle Exception e => raise (Exception e) + | _ => raise (Exception "Unknown Error thrown from c_exec_process_io, likely check that the word8 array is right length that is expected and not accessing something outside of its bounds") end end diff --git a/stubs/FFI/sys_ffi.c b/stubs/FFI/sys_ffi.c index c612867..fd122a4 100755 --- a/stubs/FFI/sys_ffi.c +++ b/stubs/FFI/sys_ffi.c @@ -4,22 +4,30 @@ #include #include #include +#include +#include +#include #include "shared_ffi_fns.h" #include "buffer_manager.h" #define SUCCESS 0x00 #define BUFFER_OVERFLOW 0xe0 #define PATH_ERROR 0xe1 +#define FORK_ERROR 0xe2 +#define PIPE_ERROR 0xe3 + +#define STDIN_WRITE_ERROR 0xe5 #define FAILED_TO_READ_FILE 0xed #define FAILED_TO_REALLOC_BUFFER 0xee #define FAILED_TO_ALLOCATE_BUFFER 0xef #define INSUFFICIENT_OUTPUT 0xf0 #define NEED_MORE_THAN_32_BITS_FOR_LENGTH 0xf1 +#define INPUT_DECODE_ERROR 0xf2 #define FILE_READ_ERROR 0xfe #define FILE_CLOSE_ERROR 0xff /** - * Function to read an entire file until EOF + * Function to read from a FILE* stream until EOF via buffered I/O. * Returns: * * 0x00 = Success @@ -115,45 +123,86 @@ uint8_t read_until_eof(FILE *file, size_t INITIAL_BUFFER_SIZE, char **buffer, si } /** - * FFI function to execute a command via popen and return its output. + * Write all bytes to a file descriptor, handling partial writes. + * Returns 0 on success, -1 on failure. + */ +static int write_all(int fd, const char *data, size_t len) +{ + size_t total_written = 0; + while (total_written < len) + { + ssize_t n = write(fd, data + total_written, len - total_written); + if (n < 0) + { + if (errno == EINTR) + continue; // Retry on interrupt + DEBUG_PRINTF("write_all: write() failed: %s\n", strerror(errno)); + return -1; + } + total_written += (size_t)n; + } + return 0; +} + +/** + * Close a file descriptor and log any errors (best-effort). + */ +static void safe_close(int fd) +{ + if (fd >= 0 && close(fd) != 0) + { + DEBUG_PRINTF("safe_close: close(%d) failed: %s\n", fd, strerror(errno)); + } +} + +/** + * FFI function to spawn a process, send input on its stdin, close the write + * end of the pipe (allowing the process to finish reading), and then read + * the process's stdout output. * - * Input: - * - commandIn: Null-terminated command string (must be absolute path) - * - clen: Length of command string - * - a: Output buffer - * - alen: Length of output buffer + * Input encoding (in commandIn, total length clen): + * [ ProcessPathLength : 4 Bytes (big-endian) ; + * ProcessPath : ProcessPathLength Bytes ; + * ArgString : remaining bytes (clen - 4 - ProcessPathLength) + * ] * * Output format in buffer 'a': * [ Success_Code : 1 Byte ; - * OutputLength : 4 Bytes (little-endian); - * OutputBuffId : 4 Bytes (little-endian); + * OutputLength : 4 Bytes (big-endian) ; + * OutputBuffId : 4 Bytes (big-endian) ; * ] * * Return codes: * 0x00 = Success * 0xe1 = Invalid path (must be absolute, no '..' allowed) - * 0xf0 = Insufficient space for output + * 0xe2 = Fork failed + * 0xe3 = Pipe creation failed + * 0xe4 = Exec failed (child could not execute process) + * 0xe5 = Failed to write input to child stdin * 0xf1 = Output too large (>UINT32_MAX bytes) - * 0xfe = Failed to open pipe or command execution error + * 0xf2 = Input decoding error (malformed input buffer) + * 0xfe = General I/O / read error * 0xff = Command execution failed (non-zero exit) * 0xed-0xef = Buffer allocation/read errors */ -void ffipopen_string(const char *commandIn, const long clen, char *a, const long alen) +void ffiexec_process_io(const char *commandIn, const long clen, char *a, const long alen) { const uint8_t RESPONSE_CODE_START = 0; const uint8_t RESPONSE_CODE_LENGTH = 1; const uint8_t OUTPUT_LENGTH_START = RESPONSE_CODE_START + RESPONSE_CODE_LENGTH; const uint8_t OUTPUT_LENGTH_LENGTH = 4; const uint8_t OUTPUT_BUFFER_ID_START = OUTPUT_LENGTH_START + OUTPUT_LENGTH_LENGTH; - const uint8_t OUTPUT_BUFFER_ID_LENGTH = 4; // Not used in this implementation, but reserved for future use + const uint8_t OUTPUT_BUFFER_ID_LENGTH = 4; const uint8_t HEADER_LENGTH = OUTPUT_BUFFER_ID_START + OUTPUT_BUFFER_ID_LENGTH; - // Input validation - if (commandIn == NULL || a == NULL || alen != HEADER_LENGTH || clen <= 0) + const uint8_t INPUT_PATH_LEN_SIZE = 4; // 4 bytes for process path length + + // ---------- Input validation ---------- + if (commandIn == NULL || a == NULL || alen < HEADER_LENGTH || clen <= 0) { - DEBUG_PRINTF("ffipopen_string: Invalid input parameters\n"); - DEBUG_PRINTF("ffipopen_string: commandIn: %p, clen: %ld, a: %p, alen: %ld\n", - commandIn, clen, a, alen); + DEBUG_PRINTF("ffiexec_process_io: Invalid input parameters\n"); + DEBUG_PRINTF("ffiexec_process_io: commandIn: %p, clen: %ld, a: %p, alen: %ld\n", + (const void *)commandIn, clen, (void *)a, alen); if (a != NULL && alen >= 1) { a[RESPONSE_CODE_START] = FILE_READ_ERROR; @@ -161,122 +210,252 @@ void ffipopen_string(const char *commandIn, const long clen, char *a, const long return; } - // Validate command length consistency - size_t actual_len = strlen(commandIn); - if (actual_len != (size_t)clen) + // Zero-initialize the output header + memset(a, 0, (size_t)alen); + + // ---------- Decode input: extract process path and arg string ---------- + if ((size_t)clen < INPUT_PATH_LEN_SIZE) { - DEBUG_PRINTF("ffipopen_string: Command length mismatch (expected %ld, actual %zu)\n", clen, actual_len); - a[RESPONSE_CODE_START] = PATH_ERROR; + DEBUG_PRINTF("ffiexec_process_io: Input too short to contain path length header\n"); + a[RESPONSE_CODE_START] = INPUT_DECODE_ERROR; + return; + } + + // Read process path length (big-endian, 4 bytes) + int process_path_len = qword_to_int((unsigned char *)commandIn); + if (process_path_len <= 0) + { + DEBUG_PRINTF("ffiexec_process_io: Invalid process path length: %d\n", process_path_len); + a[RESPONSE_CODE_START] = INPUT_DECODE_ERROR; + return; + } + + size_t path_end = (size_t)INPUT_PATH_LEN_SIZE + (size_t)process_path_len; + if (path_end > (size_t)clen) + { + DEBUG_PRINTF("ffiexec_process_io: Process path length (%d) exceeds input buffer (clen=%ld)\n", + process_path_len, clen); + a[RESPONSE_CODE_START] = INPUT_DECODE_ERROR; return; } - // Print debugging info - DEBUG_PRINTF("ffipopen_string: Command: %s\n", commandIn); - DEBUG_PRINTF("ffipopen_string: Command Length: %ld\n", clen); - DEBUG_PRINTF("ffipopen_string: Output buffer size: %ld\n", alen); + // Extract a null-terminated copy of the process path + char *process_path = malloc((size_t)process_path_len + 1); + if (process_path == NULL) + { + DEBUG_PRINTF("ffiexec_process_io: Failed to allocate process path buffer\n"); + a[RESPONSE_CODE_START] = FAILED_TO_ALLOCATE_BUFFER; + return; + } + memcpy(process_path, commandIn + INPUT_PATH_LEN_SIZE, (size_t)process_path_len); + process_path[process_path_len] = '\0'; + + // The remaining bytes are the argument / stdin input string + const char *arg_str = commandIn + path_end; + size_t arg_str_len = (size_t)clen - path_end; + + DEBUG_PRINTF("ffiexec_process_io: Process path: %s\n", process_path); + DEBUG_PRINTF("ffiexec_process_io: Arg string length: %zu\n", arg_str_len); - // Validate command path - reject relative paths and potentially dangerous patterns - if (commandIn[0] != '/' || strstr(commandIn, "..") != NULL) + // ---------- Validate process path ---------- + if (process_path[0] != '/' || strstr(process_path, "..") != NULL) { - DEBUG_PRINTF("ffipopen_string: Invalid path detected (must be absolute and not contain '..'): %s\n", commandIn); + DEBUG_PRINTF("ffiexec_process_io: Invalid path (must be absolute, no '..'): %s\n", process_path); + free(process_path); a[RESPONSE_CODE_START] = PATH_ERROR; return; } - // Open a pipe to the command - FILE *fp = popen((char *)commandIn, "r"); - if (fp == NULL) + // ---------- Create pipes ---------- + int stdin_pipe[2]; // Parent writes to [1], child reads from [0] + int stdout_pipe[2]; // Child writes to [1], parent reads from [0] + + if (pipe(stdin_pipe) != 0) + { + DEBUG_PRINTF("ffiexec_process_io: Failed to create stdin pipe: %s\n", strerror(errno)); + free(process_path); + a[RESPONSE_CODE_START] = PIPE_ERROR; + return; + } + + if (pipe(stdout_pipe) != 0) + { + DEBUG_PRINTF("ffiexec_process_io: Failed to create stdout pipe: %s\n", strerror(errno)); + safe_close(stdin_pipe[0]); + safe_close(stdin_pipe[1]); + free(process_path); + a[RESPONSE_CODE_START] = PIPE_ERROR; + return; + } + + // ---------- Fork ---------- + pid_t pid = fork(); + if (pid < 0) { - DEBUG_PRINTF("ffipopen_string: Failed to open pipe for command: %s\n", commandIn); + DEBUG_PRINTF("ffiexec_process_io: fork() failed: %s\n", strerror(errno)); + safe_close(stdin_pipe[0]); + safe_close(stdin_pipe[1]); + safe_close(stdout_pipe[0]); + safe_close(stdout_pipe[1]); + free(process_path); + a[RESPONSE_CODE_START] = FORK_ERROR; + return; + } + + if (pid == 0) + { + // ===== CHILD PROCESS ===== + // Redirect stdin to read end of stdin_pipe + close(stdin_pipe[1]); // Close write end (parent uses this) + if (dup2(stdin_pipe[0], STDIN_FILENO) < 0) + { + _exit(127); + } + close(stdin_pipe[0]); + + // Redirect stdout to write end of stdout_pipe + close(stdout_pipe[0]); // Close read end (parent uses this) + if (dup2(stdout_pipe[1], STDOUT_FILENO) < 0) + { + _exit(127); + } + close(stdout_pipe[1]); + + // Execute the process (no shell involved — direct exec) + execl(process_path, process_path, (char *)NULL); + + // If execl returns, it failed. + // Note: The error message is written to the child's stderr, which is not + // redirected or captured and therefore will appear on the parent's stderr. + fprintf(stderr, "ffiexec_process_io: execl failed for '%s': %s\n", + process_path, strerror(errno)); + _exit(127); + } + + // ===== PARENT PROCESS ===== + // Close pipe ends we don't use + safe_close(stdin_pipe[0]); // We don't read from child's stdin + safe_close(stdout_pipe[1]); // We don't write to child's stdout + + // We no longer need the path string + free(process_path); + process_path = NULL; + + // ---------- Write arg_str to child's stdin, then close ---------- + if (arg_str_len > 0) + { + if (write_all(stdin_pipe[1], arg_str, arg_str_len) != 0) + { + DEBUG_PRINTF("ffiexec_process_io: Failed to write input to child stdin\n"); + safe_close(stdin_pipe[1]); + safe_close(stdout_pipe[0]); + // Attempt to reap the child to avoid zombie + waitpid(pid, NULL, 0); + a[RESPONSE_CODE_START] = STDIN_WRITE_ERROR; + return; + } + } + + // Close write end → sends EOF to the child's stdin + safe_close(stdin_pipe[1]); + + // ---------- Read child's stdout ---------- + FILE *child_stdout = fdopen(stdout_pipe[0], "r"); + if (child_stdout == NULL) + { + DEBUG_PRINTF("ffiexec_process_io: fdopen failed on child stdout: %s\n", strerror(errno)); + safe_close(stdout_pipe[0]); + waitpid(pid, NULL, 0); a[RESPONSE_CODE_START] = FILE_READ_ERROR; return; } - // Read the output from the command into a buffer char *buffer = NULL; size_t output_length = 0; - uint8_t out_code = read_until_eof(fp, alen - HEADER_LENGTH, &buffer, &output_length); - DEBUG_PRINTF("ffipopen_string: Read %zu bytes from command output\n", output_length); + uint8_t out_code = read_until_eof(child_stdout, 4096, &buffer, &output_length); + DEBUG_PRINTF("ffiexec_process_io: Read %zu bytes from child stdout\n", output_length); + + // fclose also closes the underlying fd (stdout_pipe[0]) + fclose(child_stdout); + + // ---------- Wait for child to exit ---------- + int status = 0; + pid_t wp; + do + { + wp = waitpid(pid, &status, 0); + } while (wp < 0 && errno == EINTR); - // Close the pipe and check for command execution errors - int ret = pclose(fp); - if (ret != 0) + if (wp < 0) { - DEBUG_PRINTF("ffipopen_string: Command failed with exit code %d\n", ret); + DEBUG_PRINTF("ffiexec_process_io: waitpid failed: %s\n", strerror(errno)); + if (buffer != NULL) + free(buffer); + a[RESPONSE_CODE_START] = FILE_READ_ERROR; + return; + } + + // Check child exit status + if (WIFEXITED(status) && WEXITSTATUS(status) != 0) + { + DEBUG_PRINTF("ffiexec_process_io: Child exited with code %d\n", WEXITSTATUS(status)); + if (buffer != NULL) + free(buffer); + a[RESPONSE_CODE_START] = FILE_CLOSE_ERROR; + return; + } + else if (WIFSIGNALED(status)) + { + DEBUG_PRINTF("ffiexec_process_io: Child killed by signal %d\n", WTERMSIG(status)); if (buffer != NULL) - { free(buffer); - } a[RESPONSE_CODE_START] = FILE_CLOSE_ERROR; return; } - // Check if read_until_eof encountered an error + // ---------- Handle read errors ---------- if (out_code != SUCCESS) { - DEBUG_PRINTF("ffipopen_string: Error reading command output: %d\n", out_code); + DEBUG_PRINTF("ffiexec_process_io: Error reading child output: %d\n", out_code); if (buffer != NULL) - { free(buffer); - } a[RESPONSE_CODE_START] = out_code; return; } - // Ensure we have a valid buffer if (buffer == NULL) { - DEBUG_PRINTF("ffipopen_string: No buffer allocated despite SUCCESS status\n"); + DEBUG_PRINTF("ffiexec_process_io: No buffer allocated despite SUCCESS status\n"); a[RESPONSE_CODE_START] = FAILED_TO_ALLOCATE_BUFFER; return; } - // Cast the output length to a 32-bit integer, with error if too large + // ---------- Validate output length ---------- if (output_length > UINT32_MAX) { - DEBUG_PRINTF("ffipopen_string: Output length %zu exceeds UINT32_MAX\n", output_length); + DEBUG_PRINTF("ffiexec_process_io: Output length %zu exceeds UINT32_MAX\n", output_length); free(buffer); a[RESPONSE_CODE_START] = NEED_MORE_THAN_32_BITS_FOR_LENGTH; return; } - // uint32_t output_size = (uint32_t)output_length + HEADER_LENGTH; - - // // Check if we have enough space in the output array - // if (output_size > alen) - // { - // DEBUG_PRINTF("ffipopen_string: Insufficient space for output (need %u, have %ld)\n", output_size, alen); - // DEBUG_PRINTF("ffipopen_string: Output content (truncated): %.100s%s\n", - // buffer, output_length > 100 ? "..." : ""); - // free(buffer); - // a[RESPONSE_CODE_START] = INSUFFICIENT_OUTPUT; - // return; - // } - - // Store the buffer in our buffer manager - int buffer_id = set_new_buffer(output_length, buffer); - DEBUG_PRINTF("ffipopen_string: Successfully copying %zu bytes to buffer %d\n", output_length, buffer_id); - - // Store output length in the header (little-endian format) - // OUTPUT_LENGTH_START to (OUTPUT_LENGTH_START + OUTPUT_LENGTH_LENGTH) + // ---------- Store output in buffer manager and write response header ---------- + int buffer_id = set_new_buffer((long)output_length, buffer); + if (buffer_id < 0) + { + DEBUG_PRINTF("ffiexec_process_io: Failed to store output buffer (error %d)\n", buffer_id); + free(buffer); + a[RESPONSE_CODE_START] = FAILED_TO_ALLOCATE_BUFFER; + return; + } + + DEBUG_PRINTF("ffiexec_process_io: Stored %zu bytes in buffer %d\n", output_length, buffer_id); + assert(sizeof(uint32_t) == OUTPUT_LENGTH_LENGTH); assert(sizeof(uint32_t) == OUTPUT_BUFFER_ID_LENGTH); - int_to_qword(output_length, (unsigned char *)&a[OUTPUT_LENGTH_START]); + int_to_qword((int)output_length, (unsigned char *)&a[OUTPUT_LENGTH_START]); int_to_qword(buffer_id, (unsigned char *)&a[OUTPUT_BUFFER_ID_START]); - // for (int i = 0; i < OUTPUT_LENGTH_LENGTH; i++) - // { - // // Store the length of the payload, not including headers - // a[OUTPUT_LENGTH_START + i] = (output_length >> (i * 8)) & 0xff; - // } - // for (int i = 0; i < OUTPUT_BUFFER_ID_LENGTH; i++) - // { - // // Store the buffer ID in little-endian format - // a[OUTPUT_BUFFER_ID_START + i] = (buffer_id >> (i * 8)) & 0xff; - // } - - // Copy the buffer content to the output array + a[RESPONSE_CODE_START] = SUCCESS; - // Clean up and return - DEBUG_PRINTF("ffipopen_string: Function completed successfully\n"); - return; + DEBUG_PRINTF("ffiexec_process_io: Function completed successfully\n"); } \ No newline at end of file diff --git a/stubs/IO_Axioms.cml b/stubs/IO_Axioms.cml index 925f83e..5c784ff 100644 --- a/stubs/IO_Axioms.cml +++ b/stubs/IO_Axioms.cml @@ -49,9 +49,7 @@ structure IO_Axioms = struct (fn path => fn reqstr => (let (* val _ = print ("Sending a request to the FS: " ^ path ^ "\n") *) - val req_str = path ^ " \"" ^ (SysFFI.shellEscapeString reqstr) ^ "\"" - (* val _ = print ("Request string: " ^ req_str ^ "\n") *) - val resp = SysFFI.c_popen_string req_str + val resp = SysFFI.c_exec_process_io path reqstr (* val _ = print ("Got back a response from the ASP: \n" ^ resp ^ "\n") *) in (* TODO: Should really do some error handling in here! *)