Hello, >From this document https://apps.dtic.mil/sti/pdfs/AD1027690.pdf <https://urldefense.com/v3/__https://apps.dtic.mil/sti/pdfs/AD1027690.pdf__;!!CzAuKJ42GuquVTTmVmPViYEvSg!OA6w8_lHRjrM8TZcgTlDhuMzVD4ZxpqVA9-0bFSmrkvdcTFG4hUtwcm2vBaB_ZLNQ0yWZWS_SPscy_pF$>, we figured out that system call APIs are verified (except for their composition with sel4 kernel proofs). However, we are not sure whether other process/thread-spawning APIs are also verified. We use the APIs (listed below) in our project, hoping to develop a formally verified root-of-trust architecture atop seL4. Could you let us know if they are all verified, and if so, could you also point out the resources we can cite in our paper?
Thanks, Seoyeon APIs used in our projects are: Initial Process-related APIs platsupport_get_bootinfo simple_default_init_bootinfo bootstrap_use_current_simple allocman_make_vka simple_get_cnode simple_get_pd Thread Spawning APIs vka_alloc_tcb vka_alloc_frame seL4_ARCH_Page_Map vka_alloc_page_table seL4_ARCH_PageTable_Map vka_alloc_endpoint vka_mint_object seL4_TCB_Configure seL4_TCB_SetPriority sel4utils_set_instruction_pointer sel4utils_set_stack_pointer seL4_TCB_WriteRegisters sel4runtime_write_tls_image sel4runtime_set_tls_variable seL4_TCB_SetTLSBase seL4_TCB_Resume Process Spawning APIs sel4utils_bootstrap_vspace_with_bootinfo_leaky vspace_reserve_range bootstrap_configure_virtual_pool process_config_default_simple sel4utils_configure_process_custom vka_cspace_make_path sel4utils_mint_cap_to_process sel4utils_create_word_args sel4utils_spawn_process_v IPC/System call APIs seL4_MessageInfo_new seL4_MessageInfo_get_length seL4_SetMR seL4_GetMR seL4_Call seL4_Recv seL4_Reply seL4_Wait seL4_Yield _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
