Using seL4 as a secure bootloader

[arturkow2000]

Hello

We are considering using seL4 as a secure bootloader in the Fobnail project
We'd like to use it as mini OS that would communicate with a device called Fobnail Token in order verify integrity of the target OS and boot it if verification passes.

We need the following things to use seL4 as mini OS

• seL4 must be able to run in DLME
• a single seL4 should be able to run on any ACPI enabled x86 platform (without recompiling)
• USB host drivers with USB EEM driver and network stack
• TPM support
• ability to chainload another OS, we know about seL4_DebugRun but we'd prefer something protected with capability to allow only one service to do that.

Could you take a look at our research regarding seL4? Is there anything more we should know?

[kent-mcleod]

Could you take a look at our research regarding seL4? Is there anything more we should know?

What you have already documented appears correct. Most of the functionality you require would need to be implemented as user level components which you would need to support yourself or otherwise find another member of the community to help provide support.

I'm not aware of any projects that have directly run seL4 as a DLME. The closest I've seen was a presentation (from slide 32 onwards) about launching seL4 via a DRTM secure loader SABLE so it seems possible to at least use a small loader to setup and launch seL4 if seL4 cannot be launched directly.

Adding "kexec" functionality would be quite hard under the existing verified design as the kernel is expected to execute forever. Adding functionality that ended the kernel's execution would likely require a lot of work. I am not an expert on this, but @lsf37 may be able to comment further.

[lsf37]

kexec would not make much sense in the model of the verified kernel, but I guess you could add a syscall in an unverified config that is still protected by a capability. Security properties would obviously not hold any more since they'd now depend on the code that is being called.

[kent-mcleod]

kexec would not make much sense in the model of the verified kernel, but I guess you could add a syscall in an unverified config that is still protected by a capability. Security properties would obviously not hold any more since they'd now depend on the code that is being called.

Slightly off topic, but this would be also useful to somehow do upgrades of the kernel for version or config changes without doing a full reset.

[DemiMarie]

kexec would not make much sense in the model of the verified kernel, but I guess you could add a syscall in an unverified config that is still protected by a capability. Security properties would obviously not hold any more since they'd now depend on the code that is being called.

Could one add “this capability is not used” as a precondition, and prove that kexec() cannot be invoked without authorization?

[lsf37]

Could one add “this capability is not used” as a precondition, and prove that kexec() cannot be invoked without authorization?

That would be possible, but not simple to state. It would also considerably weaken the functional correctness theorem, because it would then depend on user behaviour, whereas now it holds regardless of what user-level code tries to do.

We do these kinds of preconditions for the security proofs (not "is not used", but "cap is not present in the system" or "cap is not available to the current thread"), but you don't need the security theorems to always hold, you only need them to hold for untrusted actors, e.g. after system setup. You do want the functional correctness theorems to always hold, because otherwise you have no basis to reason about what the system does, even for trusted actors.

[DemiMarie]

Could one add “this capability is not used” as a precondition, and prove that kexec() cannot be invoked without authorization?

That would be possible, but not simple to state. It would also considerably weaken the functional correctness theorem, because it would then depend on user behaviour, whereas now it holds regardless of what user-level code tries to do.

I am not sure that this weakening is meaningful in practice. In any realistic system I can think of, the TCB includes not only the kernel, but also the bootloader and highly-privileged userspace. Said userspace might not be able to get kernel privilege directly, but it can replace the kernel image on persistent storage and reboot, which has the same effect. Of course, one can arrange for the necessary caps to be dropped after setup, but one can do the same with kexec().

It is true that such attacks can be blocked by firmware-enforced secure boot. However, this requires that the firmware contain the needed device drivers to load seL4. In some systems, these drivers might be simple enough to formally verify, but in the systems I work with, they are not. Having seL4 support kexec() allows it to be used in the firmware itself, which in turn provides the same benefits for firmware that seL4 already provides for the OS.

We do these kinds of preconditions for the security proofs (not "is not used", but "cap is not present in the system" or "cap is not available to the current thread"), but you don't need the security theorems to always hold, you only need them to hold for untrusted actors, e.g. after system setup. You do want the functional correctness theorems to always hold, because otherwise you have no basis to reason about what the system does, even for trusted actors.

I think the best approach would be to not avoid kexec(), but rather to explicitly state what it does, and what exactly the environment the new kernel is launched in. In particular, it ought to be possible to match the postconditions of kexec() to the preconditions of kernel launch, so that if the new kernel is itself a verified build of seL4, the proofs hold for it as well.