This is a happy news!
I hope it comes with GNU/Linux support! EDIT Ops, yes it does.
Many years passed since when I used to play, but back then I definitely needed to use Wine.
Nowadays I would not even install it like that, as I would never trust a closed source program. This solves the trust problem and might solve the portability one EDIT definitely it does)
Nowadays I would not even install it like that, as I would never trust a closed source program.
This is mostly an issue with the UNIX design.
It is fairly safe to run closed source programs under seL4, as they can never exceed their capabilities.
As Linux’s security model is fairly weak, and the kernel isn’t even formally verified to enforce this weak model and cannot be (due to sheer size), everything running under Linux has to be considered part of the trusted computer base.
Closed source programs can’t be trusted, as you point out, and thus can’t be allowed to reside within the TCB.
Fortunately, it is a resolved problem. Use seL4. The whitepaper covers (Chapter 7) how this can be done progressively, with minimum hassle.
What saddens me is the amount of effort put into the wrong approach, when the right approach exists.
This is akin to making a building “a little higher” again and again, into a seriously unstable large tower, just by carefully adding to the top of it, when the foundation and structure was not made for the purpose.
The cost in man hours to each of these “little changes” in Linux pains me to read about, when considering how much progress would be made if this effort was put into the right approach, where the cost of progressing is orders of magnitude lower, thanks to fitness for purpose.
Fortunately, building regulations prevent this. In computing, however, we’re not as fortunate.
You keep pushing seL4, as though it were some kind of panacea. But consider:
It doesn’t, and can’t, protect against the well-known hardware vulnerabilities in all modern x86 and ARM chips.
It doesn’t even support PowerPC architecture, which is currently the most practical “safe” alternative architecture.
It supposedly supports 64-bit RISC-V (yay!) … but, can you even buy a practical RISC-V PC? Not yet.
You need a PhD in CS and a few weeks of intensive study just to actually understand the claim of that the formal proof makes. Much more work to really understand the proof itself. So, it’s rather more “faith based” than the marketing would suggest.
As a microkernel, it provides very much less functionality than we are conditioned to expect from Linux or BSD. You’d need to supplement it with something like big chunks of Gentoo to even get a baseline usable system. Is any part of Gentoo formally verified?
Most serious, real-world vulnerabilities aren’t in the kernel anyway, they are in applications (and occasionally device drivers and similar), so adopting seL4 wouldn’t help with that directly.
But most importantly, hobbyists and academics can more or less follow their hearts, but businesses and militaries pull much more weight, and they adopt things incrementally for (broadly) economic reasons, involving all sorts of messy things like liability and licensing and training costs. Network effects dominate decision making for reasons that have perfectly rational game-theoretic explanations. It is often wiser to stick with the devil you know. Until you understand how and why the world works like that, I imagine you will continue to be confused, frustrated, angry, and sad. That was my journey, anyway. I feel much more at peace now. :-)
I’ll be blunt; I think seL4 is an extremely expensive toy. It’s a highly subsidized research project that (to my knowledge) hasn’t ever been deployed in a genuinely high-assurance system, much less at scale. I’d love to see that change, but I’m not exactly holding my breath.
Ask a few random bystanders about microkernels (nevermind seL4, which they’ll likely never have heard about), and they’ll likely either not have a clue whatsoever, or just spit a bunch of misinformation showing their ignorance, such as references to the Tanenbaum-Torvalds debate being somehow “won” by Linus, or a blanket statement that “microkernels are slow” or “nice and academic, but do not work in practice”.
Awareness helps. The starting point here is that of believing a bunch of non-facts as facts, thus quite severe and much worse than mere ignorance. It is an uphill battle.
It doesn’t, and can’t, protect against the well-known hardware vulnerabilities in all modern x86 and ARM chips.
It’s merely out of scope. Basically, seL4 is software. What you’re doing is pointing at hardware being shit as justification for software being shit.
If you’re actually referring to seL4 not implemeting Meltdown, Spectre and such, then that’s plain wrong. seL4 does indeed implement many such mitigations. Again, it is unfortunate hardware sucks so much, but the hardware is indeed out of scope. Other teams elsewhere are working on fixing that problem.
One of the advantages of having proofs is that the assumptions are stated explicitly. By doing this, families of problems are prevented. Refer to 3.1. Proof assumptions in the seL4 whitepaper.
You need a PhD in CS and a few weeks of intensive study just to actually understand the claim of that the formal proof makes.
The same could be said about open source. But we both know it is a net positive, even if we don’t personally read every line of code that we use, directly or indirectly.
Network effects dominate decision making for reasons that have perfectly rational game-theoretic explanations. It is often wiser to stick with the devil you know.
The old “Nobody has ever been fired for using IBM”, in new incarnations. The LAMP stack, Docker, AWS, x86 and so on.
Until you understand how and why the world works like that, I imagine you will continue to be confused, frustrated, angry, and sad. That was my journey, anyway. I feel much more at peace now. :-)
I’ve been through that. It’s better, but I sadly can’t help but feel at least a little sick about how poorly everything is being done, and how often the wrong tool gets picked for the job, and incompetence is rewarded.
It’s a highly subsidized research project that (to my knowledge) hasn’t ever been deployed in a genuinely high-assurance system, much less at scale.
Refer to first paragraph of section 2.2. seL4 Is a microkernel, not an OS.
seL4 is but the successor of OKL4, a microkernel with the reputation from real world deployment that you seek. To my knowledge, and feel free to correct me if I am wrong, no microkernel has a comparable level of deployments, nor reputation.
seL4 is written by essentially the same people, who by now have plenty of experience, and is dramatically better, in no small way because of this experience.
The things you’re fighting about aren’t the problem, it’s the fighting and identifying that’s holding us back. No need for apologies tho, it gets us all from time to time.
Where’s the equivalent of Kubernetes for seL4? How do I write a simple config file like I can in Docker or Nix and produce a secure, reproducible environment that can then be deployed to dozens of systems? It would cost millions and years to build something like that? We don’t even know exactly what something like that would look like, and how to manage it so that it’s not a giant pain in the ass to administer?
The problem’s not resolved, then. Sure we know, in theory, how to resolve it, and have that theory put into practice in some sorts of systems – the ones I’ve heard about have been high-reliability embedded systems, which are relatively small and have a lot of effort put into them. But all the technology to use it at, if you forgive me the buzzword, “web scale” has yet to actually be built. You’re right, the technology should be built, but here we are.
Like I said, global warming is mostly an issue with cars and power plants. We know how to build wind farms and electric cars, so the problem is resolved, right?
These are component frameworks, covered briefly in 3.2.
Kubernetes, or docker, are the heavyweight workarounds (I also like to call them hacks) detailed in section 4.2. These really are toys, next to capabilities as implemented by seL4.
How do I write a simple config file like I can in Docker or Nix and produce a secure, reproducible environment that can then be deployed at massive scale?
No. You actually cannot in Docker or Nix. These are toys, as they rely upon the aforementioned ugly hacks Linux provides, and any claims of these providing “security” are not to be taken seriously. In some contexts, they are criminally irresponsible. And I am saying this despite doing this for a living.
For the state of the art, refer to Genode’s Sculpt. It isn’t even limited to static scenarios like the ones you described, but also supports dynamic ones.
You’re right, the technology should be built, but here we are.
We are in a much better position now than a few years ago, thanks to the current state of seL4, both technical (release 6.0 and ongoing work) and organizational (seL4 foundation has been established, and there is commercial and government participation).
It would cost millions and years to build something like that?
Would you rather put the manpower into running a fool’s errand? The popular ecosystem you’ve referenced is fundamentally broken. It cannot be fixed. No real progress can be made without a reset. Thus, leaving aside those who work on these on their free time, it is a large waste of resources to try and advance these deadend systems.
Like I said, global warming is mostly an issue with cars and power plants. We know how to build wind farms and electric cars, so the problem is resolved, right?
I see you agree with me ultimately. Doing things wrong is not the right way to do things. Yes, I also see the redundancy here.
We, um, don’t seem to have a
pascaltag. So, there’s that I guess.Wow! I wonder how many games on Steam are written in Pascal.
Why? It is a mature and tried language. It’s not fancy enough. Unlike Rust. /s
at least now we have the possibility to rewrite it in rust!11
This is a happy news! I hope it comes with GNU/Linux support! EDIT Ops, yes it does.
Many years passed since when I used to play, but back then I definitely needed to use Wine.
Nowadays I would not even install it like that, as I would never trust a closed source program. This solves the trust problem and might solve the portability one EDIT definitely it does)
This is mostly an issue with the UNIX design.
It is fairly safe to run closed source programs under seL4, as they can never exceed their capabilities.
As Linux’s security model is fairly weak, and the kernel isn’t even formally verified to enforce this weak model and cannot be (due to sheer size), everything running under Linux has to be considered part of the trusted computer base.
Closed source programs can’t be trusted, as you point out, and thus can’t be allowed to reside within the TCB.
This is entirely true, but makes it sound like a small problem. It’s like saying “global warming is mostly an issue with cars and power plants”. ;-)
Fortunately, it is a resolved problem. Use seL4. The whitepaper covers (Chapter 7) how this can be done progressively, with minimum hassle.
What saddens me is the amount of effort put into the wrong approach, when the right approach exists.
This is akin to making a building “a little higher” again and again, into a seriously unstable large tower, just by carefully adding to the top of it, when the foundation and structure was not made for the purpose.
The cost in man hours to each of these “little changes” in Linux pains me to read about, when considering how much progress would be made if this effort was put into the right approach, where the cost of progressing is orders of magnitude lower, thanks to fitness for purpose.
Fortunately, building regulations prevent this. In computing, however, we’re not as fortunate.
You keep pushing seL4, as though it were some kind of panacea. But consider:
It doesn’t, and can’t, protect against the well-known hardware vulnerabilities in all modern x86 and ARM chips. It doesn’t even support PowerPC architecture, which is currently the most practical “safe” alternative architecture. It supposedly supports 64-bit RISC-V (yay!) … but, can you even buy a practical RISC-V PC? Not yet. You need a PhD in CS and a few weeks of intensive study just to actually understand the claim of that the formal proof makes. Much more work to really understand the proof itself. So, it’s rather more “faith based” than the marketing would suggest. As a microkernel, it provides very much less functionality than we are conditioned to expect from Linux or BSD. You’d need to supplement it with something like big chunks of Gentoo to even get a baseline usable system. Is any part of Gentoo formally verified? Most serious, real-world vulnerabilities aren’t in the kernel anyway, they are in applications (and occasionally device drivers and similar), so adopting seL4 wouldn’t help with that directly.
But most importantly, hobbyists and academics can more or less follow their hearts, but businesses and militaries pull much more weight, and they adopt things incrementally for (broadly) economic reasons, involving all sorts of messy things like liability and licensing and training costs. Network effects dominate decision making for reasons that have perfectly rational game-theoretic explanations. It is often wiser to stick with the devil you know. Until you understand how and why the world works like that, I imagine you will continue to be confused, frustrated, angry, and sad. That was my journey, anyway. I feel much more at peace now. :-)
I’ll be blunt; I think seL4 is an extremely expensive toy. It’s a highly subsidized research project that (to my knowledge) hasn’t ever been deployed in a genuinely high-assurance system, much less at scale. I’d love to see that change, but I’m not exactly holding my breath.
I see this as necessary.
Ask a few random bystanders about microkernels (nevermind seL4, which they’ll likely never have heard about), and they’ll likely either not have a clue whatsoever, or just spit a bunch of misinformation showing their ignorance, such as references to the Tanenbaum-Torvalds debate being somehow “won” by Linus, or a blanket statement that “microkernels are slow” or “nice and academic, but do not work in practice”.
Awareness helps. The starting point here is that of believing a bunch of non-facts as facts, thus quite severe and much worse than mere ignorance. It is an uphill battle.
It’s merely out of scope. Basically, seL4 is software. What you’re doing is pointing at hardware being shit as justification for software being shit.
If you’re actually referring to seL4 not implemeting Meltdown, Spectre and such, then that’s plain wrong. seL4 does indeed implement many such mitigations. Again, it is unfortunate hardware sucks so much, but the hardware is indeed out of scope. Other teams elsewhere are working on fixing that problem.
One of the advantages of having proofs is that the assumptions are stated explicitly. By doing this, families of problems are prevented. Refer to 3.1. Proof assumptions in the seL4 whitepaper.
The same could be said about open source. But we both know it is a net positive, even if we don’t personally read every line of code that we use, directly or indirectly.
The old “Nobody has ever been fired for using IBM”, in new incarnations. The LAMP stack, Docker, AWS, x86 and so on.
I’ve been through that. It’s better, but I sadly can’t help but feel at least a little sick about how poorly everything is being done, and how often the wrong tool gets picked for the job, and incompetence is rewarded.
Refer to first paragraph of section 2.2. seL4 Is a microkernel, not an OS.
seL4 is but the successor of OKL4, a microkernel with the reputation from real world deployment that you seek. To my knowledge, and feel free to correct me if I am wrong, no microkernel has a comparable level of deployments, nor reputation.
seL4 is written by essentially the same people, who by now have plenty of experience, and is dramatically better, in no small way because of this experience.
This whole OT thread is why we can’t have nice things.
But this is my nice thing! You’re so right about it being a lousy place for it, though. Sorry about that.
The things you’re fighting about aren’t the problem, it’s the fighting and identifying that’s holding us back. No need for apologies tho, it gets us all from time to time.
We are celebrating Soldat’s open sourcing, in our own way.
I’ll pay that.
Where’s the equivalent of Kubernetes for seL4? How do I write a simple config file like I can in Docker or Nix and produce a secure, reproducible environment that can then be deployed to dozens of systems? It would cost millions and years to build something like that? We don’t even know exactly what something like that would look like, and how to manage it so that it’s not a giant pain in the ass to administer?
The problem’s not resolved, then. Sure we know, in theory, how to resolve it, and have that theory put into practice in some sorts of systems – the ones I’ve heard about have been high-reliability embedded systems, which are relatively small and have a lot of effort put into them. But all the technology to use it at, if you forgive me the buzzword, “web scale” has yet to actually be built. You’re right, the technology should be built, but here we are.
Like I said, global warming is mostly an issue with cars and power plants. We know how to build wind farms and electric cars, so the problem is resolved, right?
These are component frameworks, covered briefly in 3.2.
Kubernetes, or docker, are the heavyweight workarounds (I also like to call them hacks) detailed in section 4.2. These really are toys, next to capabilities as implemented by seL4.
No. You actually cannot in Docker or Nix. These are toys, as they rely upon the aforementioned ugly hacks Linux provides, and any claims of these providing “security” are not to be taken seriously. In some contexts, they are criminally irresponsible. And I am saying this despite doing this for a living.
For the state of the art, refer to Genode’s Sculpt. It isn’t even limited to static scenarios like the ones you described, but also supports dynamic ones.
We are in a much better position now than a few years ago, thanks to the current state of seL4, both technical (release 6.0 and ongoing work) and organizational (seL4 foundation has been established, and there is commercial and government participation).
Would you rather put the manpower into running a fool’s errand? The popular ecosystem you’ve referenced is fundamentally broken. It cannot be fixed. No real progress can be made without a reset. Thus, leaving aside those who work on these on their free time, it is a large waste of resources to try and advance these deadend systems.
I see you agree with me ultimately. Doing things wrong is not the right way to do things. Yes, I also see the redundancy here.
I do try and not defend the wrong approaches.
Woah! Didn’t know Soldat was made in Pascal!
Another excellent game written in FreePascal is DoomRL: https://drl.chaosforge.org/
Currently closed source though, I believe. Ah well.It has been opened: https://github.com/ChaosForge/doomrl
Thanks! I’d forgotten about that.