3 ms·

What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software. Indeed, each release is expected to introdu

What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software. Indeed, each release is expected to introduce new bugs and vendors typically sell service contracts based on the perpetual brokenness of existing software engineering processes. Whereas formally verified software typically has single digit numbers of bugs ... ever. Sure, you get to score rhetorical points about the proof being incorrect once. But this bridge is now fixed and won't fail that way again in the same way. Cartels and governments regularly hack phones and spy on and even kill activists. The current processes you are defending get people killed and are undermining civil society. SeL4 is a big deal and definitely worth the investments needed to make such reliability the norm instead of accepting the continual bridge collapses that occur in Linux land.

mmooss 2y ago
> Cartels and governments regularly hack phones and spy on and even kill activists. Your comment implies SeL4 will prevent these things from happening. Isn't that going way too far? It's a nice start, but we're nowhere near securing things on that level. Without looking into it, I'd put more faith in iPhone's lockdown mode.
- indolering 2y ago
  We have a long way to crawl, but process isolation is the bedrock of all other security guarantees.
  - ryao 2y ago
    Tell me how process isolation prevents SQL injection. I could ask about any of a great variety of security issues, but I think SQL injection is a great choice for debunking “process isolation is the bedrock of all other security guarantees”. We do not have to worry because we have process isolation is basically this: https://web.archive.org/web/20240123122515if_/https://www.syslog.com/~jwilson/pics-i-like/kurios119.jpg https://web.archive.org/web/20240123122515if_/https://www.sy... I suspect you did not mean to say that, but your comments can be interpreted to mean that, especially when you suggest people will die if seL4 is not used as if nothing else matters, and inject that into a discussion of whether seL4’s is free of flaws (it is not). Using seL4 is like flattening the ground on which a building foundation will sit. Just because the ground was flattened to within microns of flatness does not mean there is nothing else wrong with the foundation and building that are built on it. Perhaps I am being pedantic, but you deserve this after suggesting the mere act of giving an opinion on seL4 made me an accessory to murder.
    - throwway120385 2y ago
      The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. And they really mean _reliability_ as in reliably wrong or reliably right. So being able to adjust the spec and fix the system is actually a feature because it means your prover acts as a high-quality test. As always, with systems like this if you use a formally-proven operating system kernel you will probably assess which other code paths in your application code are on the critical path and use formal methods on those components. And you will also be doing other less formal work like FMEA to complement. So you're not reliant on any one single method of assessing whether the system works, whether it meets the specification, and whether it can be relied upon to do the right thing in a bad situation.
      - ryao 2y ago
        The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. The other guy mentioned phones, which run UNIX clones. It is fairly obvious that we were talking about computing in general, which includes all of the things you claim to be out of scope. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. Most embedded systems (e.g. the RP2040, the MSP430, etcetera) do not even have virtual memory protection, which makes seL4 a non option for them. When seL4 is an option, it is a tiny fraction of the code needed for the machine. All of that other code matters, especially since it is where the attack surface area is. seL4 on such machines is like the admin account in this picture; compromising what actually matters does not require compromising seL4: https://xkcd.com/1200/ https://xkcd.com/1200/ While seL4 is good at what it does, what seL4 does is extremely minimal and it is increasingly obvious that a vocal minority overrates it. Using seL4 is not going to stop vulnerabilities in userspace or even in drivers that were previously in kernel space, or in VMs running on top of it, but people who claim systems are insecure without seL4 insinuate that it will. They are like the Apple Store employee who once suggested to me that if I run Windows on Apple hardware, it will have none of the problems Windows normally has.
- naasking 2y ago
  What? You'd put more faith in a kernel that has no formal verification of its conformance to a secure spec and has orders of magnitude more code in it that can go wrong? What is the basis for this confidence?
  - 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?
ryao 2y ago
What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software. They can be reintroduced into seL4 too. Just have an amendment to the specification adding a new feature say the bug is okay without anyone realizing it does. Sure, you get to score rhetorical points about the proof being incorrect once. But this bridge is now fixed and won't fail that way again in the same way. The proof itself proved something other than what was advertised, which allowed for this issue to exist. If you look at the bug tracker, it appears that this has happened more than one time. While seL4 is an amazing achievement, it is clear that it is not the bulletproof software that people thought it was. There is no proof that the specification is problem free after all. Cartels and governments regularly hack phones and spy on and even kill activists. The current processes you are defending get people killed and are undermining civil society. This is a gross misrepresentation of what I said. Having an objective evidence based opinion that seL4 is not as good as advertised has nothing to do with people dying. SeL4 is a big deal and definitely worth the investments needed to make such reliability the norm instead of accepting the continual bridge collapses that occur in Linux land. seL4 does not achieve this. It is the equivalent of less than 0.001% of all of the code run on machines. It makes no guarantees that the >99.999% that people use is okay.

mmooss 2y ago

> Cartels and governments regularly hack phones and spy on and even kill activists. Your comment implies SeL4 will prevent these things from happening. Isn't that going way too far? It's a nice start, but we're nowhere near securing things on that level. Without looking into it, I'd put more faith in iPhone's lockdown mode.

indolering 2y ago
We have a long way to crawl, but process isolation is the bedrock of all other security guarantees.
- ryao 2y ago
  Tell me how process isolation prevents SQL injection. I could ask about any of a great variety of security issues, but I think SQL injection is a great choice for debunking “process isolation is the bedrock of all other security guarantees”. We do not have to worry because we have process isolation is basically this: https://web.archive.org/web/20240123122515if_/https://www.syslog.com/~jwilson/pics-i-like/kurios119.jpg https://web.archive.org/web/20240123122515if_/https://www.sy... I suspect you did not mean to say that, but your comments can be interpreted to mean that, especially when you suggest people will die if seL4 is not used as if nothing else matters, and inject that into a discussion of whether seL4’s is free of flaws (it is not). Using seL4 is like flattening the ground on which a building foundation will sit. Just because the ground was flattened to within microns of flatness does not mean there is nothing else wrong with the foundation and building that are built on it. Perhaps I am being pedantic, but you deserve this after suggesting the mere act of giving an opinion on seL4 made me an accessory to murder.
  - throwway120385 2y ago
    The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. And they really mean _reliability_ as in reliably wrong or reliably right. So being able to adjust the spec and fix the system is actually a feature because it means your prover acts as a high-quality test. As always, with systems like this if you use a formally-proven operating system kernel you will probably assess which other code paths in your application code are on the critical path and use formal methods on those components. And you will also be doing other less formal work like FMEA to complement. So you're not reliant on any one single method of assessing whether the system works, whether it meets the specification, and whether it can be relied upon to do the right thing in a bad situation.
    - ryao 2y ago
      The systems we're talking about don't use SQL to communicate. They use data structures in a wire format of some sort because they are embedded systems. Don't pretend like we're talking about web development here, because we're not. The other guy mentioned phones, which run UNIX clones. It is fairly obvious that we were talking about computing in general, which includes all of the things you claim to be out of scope. SeL4 is designed for hard real time embedded systems and uses formal methods, which have and continue to be a mainstay approach in places which value security and reliability. Most embedded systems (e.g. the RP2040, the MSP430, etcetera) do not even have virtual memory protection, which makes seL4 a non option for them. When seL4 is an option, it is a tiny fraction of the code needed for the machine. All of that other code matters, especially since it is where the attack surface area is. seL4 on such machines is like the admin account in this picture; compromising what actually matters does not require compromising seL4: https://xkcd.com/1200/ https://xkcd.com/1200/ While seL4 is good at what it does, what seL4 does is extremely minimal and it is increasingly obvious that a vocal minority overrates it. Using seL4 is not going to stop vulnerabilities in userspace or even in drivers that were previously in kernel space, or in VMs running on top of it, but people who claim systems are insecure without seL4 insinuate that it will. They are like the Apple Store employee who once suggested to me that if I run Windows on Apple hardware, it will have none of the problems Windows normally has.
naasking 2y ago
What? You'd put more faith in a kernel that has no formal verification of its conformance to a secure spec and has orders of magnitude more code in it that can go wrong? What is the basis for this confidence?
- 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?

ryao 2y ago

What's odd about this argument is that such bugs would be at risk of reintroduction in any other piece of software. They can be reintroduced into seL4 too. Just have an amendment to the specification adding a new feature say the bug is okay without anyone realizing it does. Sure, you get to score rhetorical points about the proof being incorrect once. But this bridge is now fixed and won't fail that way again in the same way. The proof itself proved something other than what was advertised, which allowed for this issue to exist. If you look at the bug tracker, it appears that this has happened more than one time. While seL4 is an amazing achievement, it is clear that it is not the bulletproof software that people thought it was. There is no proof that the specification is problem free after all. Cartels and governments regularly hack phones and spy on and even kill activists. The current processes you are defending get people killed and are undermining civil society. This is a gross misrepresentation of what I said. Having an objective evidence based opinion that seL4 is not as good as advertised has nothing to do with people dying. SeL4 is a big deal and definitely worth the investments needed to make such reliability the norm instead of accepting the continual bridge collapses that occur in Linux land. seL4 does not achieve this. It is the equivalent of less than 0.001% of all of the code run on machines. It makes no guarantees that the >99.999% that people use is okay.