Hi Gerwin,
I am Sashi, a Ph.D. student at the University of California, Irvine, and
one of the authors working with Seoyeon. Thanks a lot for your response.
This is very helpful and clarifies a lot of questions we have on seL4.
To briefly introduce what we are working on: We aim to build a remote
attestation service for the processes running atop seL4, and for that, we
are planning to spawn a separate (formally-verified) process that handles
attestation. This attestation process needs to be high-assurance for
obvious reasons because it contains a secret key that is used for
implementing digital signatures. For more details on this, please refer to
one of our old papers: https://arxiv.org/pdf/1703.02688.pdf,
which discusses a basic version of attestation (but without formal
guarantees though).
Based on your response, we now understand that the system calls such as
seL4_call, seL4_recv, ..... are verified, however, other user-utility APIs
are not. In our case, we are using the system-call APIs, especially the
ones implementing IPC, to communicate with the attestation process.
Ideally, we want to verify this attestation process, and hence, to best
argue the security and assurance properties, we require the APIs it is
using to be also verified, which they are.
If you don't mind, we have a few more questions on seL4 that will help us
in our project, would you be able to clarify them?
1. We know that seL4 can load and spawn processes at boot time when the
initial process executes. However, is it possible to load and spawn a
process at runtime, i.e, dynamic loading? In particular, can a process,
spawned by the initial process at boot, spawn another process by itself
using utility APIs?
2. In general OS, it is not possible to modify the code section of a
process (which is read-only) at runtime. Is it the same case on seL4 too?
The reason for this question is: we would like to know if it is safe to
assume that the binary of a process, after loading, will not change as long
as the system is not reset (assuming we are running seL4 on ARM-based
Sabrelite platforms for embedded applications). In other words, is there a
way to modify or update the binary of a process at runtime via remote
means, other than by physically reprogramming the device and rebooting it?
3. We are using HACL* implementation (from https://hacl-star.github.io/) to
implement digital signatures in the attestation process. In short, our
attestation process implementation contains a few calls to seL4 IPC APIs to
receive/send the attestation request/response and one call to HACL* API to
compute a signature. For this, we are trying to figure out what is the best
way to compose proofs across APIs written in different formal verification
languages (seL4 written in Isabelle and HACL* written in F*). If you have
any insights on this, it would help us a lot.
We really appreciate your time. Thanks a lot for your responses! Looking
forward to hearing from you.
Best regards,
Sashi
On Mon, Jan 23, 2023 at 7:40 PM Gerwin Klein
Hi
From this document https://urldefense.com/v3/__https://apps.dtic.mil/sti/pdfs/AD1027690.pdf__;!... < https://urldefense.com/v3/__https://apps.dtic.mil/sti/pdfs/AD1027690.pdf__;!... , 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://urldefense.com/v3/__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://urldefense.com/v3/__https://github.com/seL4/seL4_libs__;!!CzAuKJ42Gu... 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
-- Sashidhar Jakkamsetti University of California Irvine, Ph.D. https://sites.uci.edu/sashidharjakkamsetti/