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
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
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.
On 24 Jan 2023, at 14:58, Demi Marie Obenour demiobenour@gmail.com wrote:
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.
It depends on the definition of critical, i.e. what safety or security property you're trying to enforce. For example, that would usually not be that the user sees the website they requested in a browser, but that whatever any website does, it cannot compromise the rest of the machine. That property does not depend on the human user.
I don't know Qubes in detail, but I'd think the code that needs to be at the highest criticality level for that property to hold is relatively small. It'd mainly be the component that is responsible for starting up and isolating new components. That could be one central component or an architecture where things can be created recursively in containers. I'd give drivers and other hardware access the next level of criticality (high, but maybe not formal-verification high), probably also communication code between partitions, and would treat anything else (Linux, user code, etc) as entirely untrusted. "Untrusted" wouldn't mean "doesn't work", only "is not required to work for security to hold".
My point is that once you have defined what critical means, even in a dynamic system, the number of critical components is not usually unbounded (maybe the number of instances, but not the code).
Conversely, if you can't define what critical means, you can't really design for it. For example, in the extreme, critically important for one system purpose might be actively damaging for another system purpose.
Of course there other properties where that doesn't work as well, I'm not saying there is a silver bullet. It just works in more cases than one might initially think.
Cheers, Gerwin
In Qubes OS the critical component is the hypervisor and all the derived code that is involved in isolation. If you achieve a "trusted isolation" then you have 95% of the job done. Attackers can still break the system but they would need to focus on the 5% that involves code in the isolated environments. This is, by far, much less interesting to top adversaries and usually requires a tailored development for specific targets, something hated by such top adversaries (attackers like profitable, reliable exploits of core components).
El mar., 24 ene. 2023 5:55, Gerwin Klein kleing@unsw.edu.au escribió:
On 24 Jan 2023, at 14:58, Demi Marie Obenour demiobenour@gmail.com wrote:
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.
It depends on the definition of critical, i.e. what safety or security property you're trying to enforce. For example, that would usually not be that the user sees the website they requested in a browser, but that whatever any website does, it cannot compromise the rest of the machine. That property does not depend on the human user.
I don't know Qubes in detail, but I'd think the code that needs to be at the highest criticality level for that property to hold is relatively small. It'd mainly be the component that is responsible for starting up and isolating new components. That could be one central component or an architecture where things can be created recursively in containers. I'd give drivers and other hardware access the next level of criticality (high, but maybe not formal-verification high), probably also communication code between partitions, and would treat anything else (Linux, user code, etc) as entirely untrusted. "Untrusted" wouldn't mean "doesn't work", only "is not required to work for security to hold".
My point is that once you have defined what critical means, even in a dynamic system, the number of critical components is not usually unbounded (maybe the number of instances, but not the code).
Conversely, if you can't define what critical means, you can't really design for it. For example, in the extreme, critically important for one system purpose might be actively damaging for another system purpose.
Of course there other properties where that doesn't work as well, I'm not saying there is a silver bullet. It just works in more cases than one might initially think.
Cheers, Gerwin
Devel mailing list -- devel@sel4.systems To unsubscribe send an email to devel-leave@sel4.systems
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 kleing@unsw.edu.au wrote:
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
On 1/26/23, Sashidhar Jakkamsetti sjakkams@uci.edu wrote:
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).
Please briefly describe the use case for this implementation.
Thank you, Zenaan
Say we have two actors: (1) the device, aka prover, installed with sel4 and our attestation service, and (2) the device owner, aka, the verifier.
Verifier decides what applications can run on the prover. For example, there are two applications: app1 and app2. Once configured, the verifier deploys the prover at a remote location. Now when the verifier wants to connect to app1 to request a service, it sends an attestation request to our attestation process to check the status of app1, i.e., whether app1 is running and in good condition. As a response to the request, the verifier gets a signature indicating that app1 is alive and healthy, and also an encryption key that the verifier can use to further communicate with app1. Similarly, the same goes for app2.
We imagine attestation to be implemented like this: signature_app1 = ECDSA{signing_key, nonce, SHA2(binary_of_app1) || SHA2(encryption_key_of_app1)}, where signing_key is the secret key of the attestation process.
On Wed, Jan 25, 2023 at 2:05 PM Zenaan Harkness zenaan@gmail.com wrote:
On 1/26/23, Sashidhar Jakkamsetti sjakkams@uci.edu wrote:
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://urldefense.com/v3/__https://arxiv.org/pdf/1703.02688.pdf__;!!CzAuKJ4... ,
which discusses a basic version of attestation (but without formal guarantees though).
Please briefly describe the use case for this implementation.
Thank you, Zenaan
On 1/25/23 12:08, Sashidhar Jakkamsetti wrote:
- In general OS, it is not possible to modify the code section of a
process (which is read-only) at runtime.
Is this accurate? I guess you’re assuming no mmap/mprotect? In general, it _is_ possible to modify code at runtime on most OSes. Maybe you can’t literally modify your ELF code section which may be mapped immutably RX, but you can allocate new RWX memory and then jump into it. This is how JIT engines used to work. Nowadays they generally allocate something RW, write code into it, flip to RX, then jump into it. So slightly safer, but you still have dynamically modified code.
I agree that _not_ having this “feature” seems to make sense for your use case though. One of the tricky things you may end up having to deal with is memory aliasing. To prove the contents of an RX page is never modified, you unfortunately also need to prove no RW alias mappings of it exist or that no writes to them occur.
Thank you for that explanation of the attestion process, I appreciate your clairty.
Do you have a real world use case you can share please?
Thank you, Zenaan
On 1/26/23, Sashidhar Jakkamsetti sjakkams@uci.edu wrote:
Say we have two actors: (1) the device, aka prover, installed with sel4 and our attestation service, and (2) the device owner, aka, the verifier.
Verifier decides what applications can run on the prover. For example, there are two applications: app1 and app2. Once configured, the verifier deploys the prover at a remote location. Now when the verifier wants to connect to app1 to request a service, it sends an attestation request to our attestation process to check the status of app1, i.e., whether app1 is running and in good condition. As a response to the request, the verifier gets a signature indicating that app1 is alive and healthy, and also an encryption key that the verifier can use to further communicate with app1. Similarly, the same goes for app2.
We imagine attestation to be implemented like this: signature_app1 = ECDSA{signing_key, nonce, SHA2(binary_of_app1) || SHA2(encryption_key_of_app1)}, where signing_key is the secret key of the attestation process.
On Wed, Jan 25, 2023 at 2:05 PM Zenaan Harkness zenaan@gmail.com wrote:
On 1/26/23, Sashidhar Jakkamsetti sjakkams@uci.edu wrote:
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://urldefense.com/v3/__https://arxiv.org/pdf/1703.02688.pdf__;!!CzAuKJ4... ,
which discusses a basic version of attestation (but without formal guarantees though).
Please briefly describe the use case for this implementation.
Thank you, Zenaan
-- Sashidhar Jakkamsetti University of California Irvine, Ph.D. https://sites.uci.edu/sashidharjakkamsetti/
A very recent use case where attestation is used is in Intel SGX https://www.intel.com/content/www/us/en/developer/tools/software-guard-extensions/attestation-services.html. SGX is used on some Intel servers where the data in compute needs to be secure. Another example is TPM https://en.wikipedia.org/wiki/Trusted_Platform_Module, extensively used in Windows machines https://learn.microsoft.com/en-us/windows/security/information-protection/tpm/trusted-platform-module-overview .
We plan to implement similar functionalities on embedded platforms with formal guarantees. Especially on ARM-based processors, such as Sabrelite.
Hope this helps. Please let me know if you have any further questions.
On Wed, Jan 25, 2023 at 4:09 PM Zenaan Harkness zenaan@gmail.com wrote:
Thank you for that explanation of the attestion process, I appreciate your clairty.
Do you have a real world use case you can share please?
Thank you, Zenaan
On 1/26/23, Sashidhar Jakkamsetti sjakkams@uci.edu wrote:
Say we have two actors: (1) the device, aka prover, installed with sel4
and
our attestation service, and (2) the device owner, aka, the verifier.
Verifier decides what applications can run on the prover. For example, there are two applications: app1 and app2. Once configured, the verifier deploys the prover at a remote location. Now when the verifier wants to connect to app1 to request a service, it sends an attestation request to our attestation process to check the status of app1, i.e., whether app1
is
running and in good condition. As a response to the request, the verifier gets a signature indicating that app1 is alive and healthy, and also an encryption key that the verifier can use to further communicate with
app1.
Similarly, the same goes for app2.
We imagine attestation to be implemented like this: signature_app1 = ECDSA{signing_key, nonce, SHA2(binary_of_app1) || SHA2(encryption_key_of_app1)}, where signing_key is the secret key of the attestation process.
On Wed, Jan 25, 2023 at 2:05 PM Zenaan Harkness zenaan@gmail.com
wrote:
On 1/26/23, Sashidhar Jakkamsetti sjakkams@uci.edu wrote:
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://urldefense.com/v3/__https://arxiv.org/pdf/1703.02688.pdf__;!!CzAuKJ4...
,
which discusses a basic version of attestation (but without formal guarantees though).
Please briefly describe the use case for this implementation.
Thank you, Zenaan
-- Sashidhar Jakkamsetti University of California Irvine, Ph.D. https://sites.uci.edu/sashidharjakkamsetti/
-
Demi Marie Obenour -
Gerwin Klein -
Hugo V.C. -
Matthew Fernandez -
Sashidhar Jakkamsetti -
Seoyeon Hwang -
Zenaan Harkness