Hi >> 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).
The report above only talks about the lowest libsel4 layer, i.e. the C language bindings of the seL4 ABI. In that sense you can view the entire kernel API as verified, in particular the kernel API presented by the non-MCS configurations listed in https://github.com/seL4/seL4/tree/master/configs The proofs mentioned in the report are not maintained and do not apply to the current version of seL4 any more, so strictly speaking the verification goes to the kernel ABI level only, but the libsel4 language binding process has not fundamentally changed since then and can still be counted as high assurance. Some of the functions you listed below that (e.g. "vka_alloc_frame", or anything that does not start with "seL4_") are not the kernel API. Instead they are from user-level convenience libraries that are low assurance and without any verification at all. As the "About" tab on https://github.com/seL4/seL4_libs says: "No-assurance libraries for rapid-prototyping of seL4 apps." The functions starting with "seL4_..." in that list look like they are direct seL4 API calls and are therefore probably in the verified set (if they are indeed seL4 API calls, not something with the same name). Whether verification is necessary for these calls depends on the system you are building and its architecture. Usually the point of isolating components from each other on top of a microkernel is that you can have low-assurance components in the system without compromising overall security. Our main user-level verification efforts tend to focus on a small number of critical components and on initialising access control authority in the system correctly so that these critical components cannot be compromised or circumvented by other components. Cheers, Gerwin _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
