3 ms·

Does it even matter when the attack surface is in userspace? Formally verifying seL4 against a potentially buggy specification does not provide any assurances a

by ryao 2y ago

Does it even matter when the attack surface is in userspace? Formally verifying seL4 against a potentially buggy specification does not provide any assurances about the user space code that must run on top to produce a working system. If you subscribe to the idea that the mere use of seL4 makes things more secure, you might use seL4 as a hypervisor beneath Linux on machines that would previously have run Linux on bare metal and then you would be using seL4, but you would not have made anything more secure. The increase in the TCB would suggest such a setup is less secure. The security of a machine using seL4 is dependent on what runs on top of it because seL4 is not the boundary between attackers and their targets. The only exception would be if you are a virtual machine provider and then seL4 would only be part of the boundary, rather than the whole boundary.

naasking 2y ago
> but you would not have made anything more secure. This is does not follow. Why do you think a hypervisor with no verification to a spec is necessarily more secure than a hypervisor with a verification to a spec? Can you somehow quantify the latent bugs in the non-verified code?
- ryao 2y ago
  The “that would previously have run Linux on bare metal” part of that sentence was important. Try reading it again. It never compared seL4 as a hypervisor to another hypervisor. It compared using seL4 as a hypervisor to not using a hypervisor at all on a machine that does not need a hypervisor. The addition of seL4 there is not only pointless, but possibly harmful if you consider the increased TCB size. By the way, seL4 as a hypervisor uses components that are not verified to a specification, so saying that it is verified to a specification is not quite correct. They also seem to be proof of concept examples rather than a production solution when I look at their documentation: https://docs.sel4.systems/projects/camkes-vm/ https://docs.sel4.systems/projects/camkes-vm/ https://docs.sel4.systems/projects/camkes-vm/centos https://docs.sel4.systems/projects/camkes-vm/centos Why is it that everyone on the “seL4 makes everything secure” bandwagon seems to have a tunnel vision that ignores that seL4 is useless without a large amount of unverified software that runs on top and that security will typically depend on that software, rather than seL4?

by ryao 2y ago

naasking 2y ago

> but you would not have made anything more secure. This is does not follow. Why do you think a hypervisor with no verification to a spec is necessarily more secure than a hypervisor with a verification to a spec? Can you somehow quantify the latent bugs in the non-verified code?

ryao 2y ago
The “that would previously have run Linux on bare metal” part of that sentence was important. Try reading it again. It never compared seL4 as a hypervisor to another hypervisor. It compared using seL4 as a hypervisor to not using a hypervisor at all on a machine that does not need a hypervisor. The addition of seL4 there is not only pointless, but possibly harmful if you consider the increased TCB size. By the way, seL4 as a hypervisor uses components that are not verified to a specification, so saying that it is verified to a specification is not quite correct. They also seem to be proof of concept examples rather than a production solution when I look at their documentation: https://docs.sel4.systems/projects/camkes-vm/ https://docs.sel4.systems/projects/camkes-vm/ https://docs.sel4.systems/projects/camkes-vm/centos https://docs.sel4.systems/projects/camkes-vm/centos Why is it that everyone on the “seL4 makes everything secure” bandwagon seems to have a tunnel vision that ignores that seL4 is useless without a large amount of unverified software that runs on top and that security will typically depend on that software, rather than seL4?