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:
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.
"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.
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.
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:
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.
"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.
"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:
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.
You do not appear to understand the difference between "necessary" and "sufficient".
Process isolation is not sufficient (i.e. adequate on its own) to make a SQL server secure against maliciously crafted inputs intended to cause SQL injection for the purpose of undesired database access because it does not sprinkle magical security pixie dust on it.
Process isolation is necessary (in practice) to make a SQL server secure against maliciously crafted inputs intended to cause SQL injection for the purpose of undesired database access because otherwise a attacker can just modify the code of the SQL server to directly do the undesired database accesses. Without process isolation your SQL server security/design can be bypassed.
The amazing thick walls of your castle do not matter if you built it on sand. The amazing solid bedrock is not sufficient to claim your castle is defensible if your castle is a wooden shack, but it is necessary for building a defensible castle.
A lack of process isolation does not allow your SQL server security to be bypassed when the adversary is not on the machine in the first place. The adversary would usually fill out a field on a form, which is where SQL injection attacks usually occur:
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.