3 ms·

> 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 t

by 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.
  - Veserv 2y ago
    "process isolation is the bedrock of all other security guarantees" means process isolation is a necessary (in practice) condition, not a sufficient condition. "Tell me how process isolation prevents SQL injection." is a non-sequitur because that is only coherent if they claimed process isolation is a sufficient condition. To disagree with their position, you need to demonstrate a system where there is no process isolation and where maliciously crafted inputs intended to cause SQL injection can not result in undesired database access. So, one process gets to arbitrarily modify the contents of the SQL server process including changing the code and you need to prevent it from wrecking your database.
    - ryao 2y ago
      "process isolation is the bedrock of all other security guarantees" means process isolation is a necessary (in practice) condition, not a sufficient condition The attack surface of networked machines is unaffected by process isolation. It is only when you are already inside does process isolation have any use. Thus the idea that it is the bedrock is wrong. "Tell me how process isolation prevents SQL injection." is a non-sequitur because that is only coherent if they claimed process isolation is a sufficient condition. It is a counter example that shows that process isolation is not the bedrock that it was claimed to be. Id sequitur. To disagree with their position, you need to demonstrate a system where there is no process isolation and where maliciously crafted inputs intended to cause SQL injection can not result in undesired database access. So, one process gets to arbitrarily modify the contents of the SQL server process including changing the code and you need to prevent it from wrecking your database. Non sequitur applies here. The protection against SQL injection and process isolation have no link whatsoever. The fact that there is no link was my entire point. The example did not need to be SQL injection either. Telling me that I need to prove a link that is the opposite of what I was saying does not follow at all. As I previously said, I could have cited just about any common vulnerability and process isolation would have done nothing about it. For example: https://owasp.org/www-project-top-ten/ https://owasp.org/www-project-top-ten/ I only cited SQL injection because I could not think of any claim more absurd than the claim that process isolation is bedrock of guarantees against SQL injection, but if process isolation were the bedrock of all other security guarantees, then it would some relationship to protection against sql injection.
  - nickpsecurity 2y ago
    "Tell me how process isolation prevents SQL injection." You need process isolation to make the system secure enough to even require SQL injection. Otherwise, they can send packets to attack anything else on the system, get full privileges, and swap your SQL-enabled application with their own. While taking your database. Further, techniques to block SQL injection work even better when they're in an isolated partition the attacker can't escape from. Even better if data can only flow in a specific way. Even better if it can be reliably cut off and recovered upon detection of a failure. That's why high-assurance guards used to sit between sensitive systems and untrusted networks. They did all of these things. Now, for application-level issues. The Separation Kernel Protection Profile, which inspired designs like INTEGRITY-178B and seL4, called for secure middlewhere to protect communications between partitions or systems. That included message routers that enforced the security policy within the system. That would include protocol-level defenses, like for SQL requests, to protect communications outside the box. seL4's isolation was, by itself, never intended to stop unrelated attacks. The vision, described in NICTA's Trustworthy Embedded Systems program, was to combine many components to do that. I'll add that seL4 team did a great job documenting the many points they may fail in their Assumptions page. They were much more open about it than most competing projects.
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?

by mmooss 2y ago

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.
- Veserv 2y ago
  "process isolation is the bedrock of all other security guarantees" means process isolation is a necessary (in practice) condition, not a sufficient condition. "Tell me how process isolation prevents SQL injection." is a non-sequitur because that is only coherent if they claimed process isolation is a sufficient condition. To disagree with their position, you need to demonstrate a system where there is no process isolation and where maliciously crafted inputs intended to cause SQL injection can not result in undesired database access. So, one process gets to arbitrarily modify the contents of the SQL server process including changing the code and you need to prevent it from wrecking your database.
  - ryao 2y ago
    "process isolation is the bedrock of all other security guarantees" means process isolation is a necessary (in practice) condition, not a sufficient condition The attack surface of networked machines is unaffected by process isolation. It is only when you are already inside does process isolation have any use. Thus the idea that it is the bedrock is wrong. "Tell me how process isolation prevents SQL injection." is a non-sequitur because that is only coherent if they claimed process isolation is a sufficient condition. It is a counter example that shows that process isolation is not the bedrock that it was claimed to be. Id sequitur. To disagree with their position, you need to demonstrate a system where there is no process isolation and where maliciously crafted inputs intended to cause SQL injection can not result in undesired database access. So, one process gets to arbitrarily modify the contents of the SQL server process including changing the code and you need to prevent it from wrecking your database. Non sequitur applies here. The protection against SQL injection and process isolation have no link whatsoever. The fact that there is no link was my entire point. The example did not need to be SQL injection either. Telling me that I need to prove a link that is the opposite of what I was saying does not follow at all. As I previously said, I could have cited just about any common vulnerability and process isolation would have done nothing about it. For example: https://owasp.org/www-project-top-ten/ https://owasp.org/www-project-top-ten/ I only cited SQL injection because I could not think of any claim more absurd than the claim that process isolation is bedrock of guarantees against SQL injection, but if process isolation were the bedrock of all other security guarantees, then it would some relationship to protection against sql injection.
- nickpsecurity 2y ago
  "Tell me how process isolation prevents SQL injection." You need process isolation to make the system secure enough to even require SQL injection. Otherwise, they can send packets to attack anything else on the system, get full privileges, and swap your SQL-enabled application with their own. While taking your database. Further, techniques to block SQL injection work even better when they're in an isolated partition the attacker can't escape from. Even better if data can only flow in a specific way. Even better if it can be reliably cut off and recovered upon detection of a failure. That's why high-assurance guards used to sit between sensitive systems and untrusted networks. They did all of these things. Now, for application-level issues. The Separation Kernel Protection Profile, which inspired designs like INTEGRITY-178B and seL4, called for secure middlewhere to protect communications between partitions or systems. That included message routers that enforced the security policy within the system. That would include protocol-level defenses, like for SQL requests, to protect communications outside the box. seL4's isolation was, by itself, never intended to stop unrelated attacks. The vision, described in NICTA's Trustworthy Embedded Systems program, was to combine many components to do that. I'll add that seL4 team did a great job documenting the many points they may fail in their Assumptions page. They were much more open about it than most competing projects.

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?