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