On 1/23/23 22:40, Gerwin Klein wrote: > 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
What is the appropriate design for dynamic systems with a potentially unbounded number of critical components? In Qubes OS, for example, there is no way to know what is and is not critical, as that depends on the (human) user. -- Sincerely, Demi Marie Obenour (she/her/hers) _______________________________________________ Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
