| |
| ▲ | kragen a day ago | parent [-] | | Another new kernel might be 1/6000 the size of Linux and therefore have 1/600 times the exploitable bugs—or none, using formal methods. The question is how much a new user-mode kernel can shield Linux from attacks. Usually the new kernel depends on Linux to separate it from the malicious code! | | |
| ▲ | Imustaskforhelp a day ago | parent | next [-] | | > Another new kernel might be 1/6000 the size of Linux and therefore have 1/600 times the exploitable bugs—or none, using formal methods. The question is how much a new user-mode kernel can shield Linux from attacks. Usually the new kernel depends on Linux to separate it from the malicious code! Is there any new language close to rust which can help being verified using formal methods or would some other language be more suitable for this job? Maybe using verus + rust, it seems that atmosphere[0] is an interesting project in this space [0]: https://mars-research.github.io/projects/atmo/ | | |
| ▲ | kragen a day ago | parent [-] | | Of established languages, Rust, OCaml, F#, and Lean seem to be promising for this kind of thing, but people seem to be vibecoding a lot of new languages right now with this use in mind. |
| |
| ▲ | asdfsa32 16 hours ago | parent | prev [-] | | You writing that in response to a vibecoded kernel. | | |
| ▲ | kragen 15 hours ago | parent [-] | | No, I writing that in response to "If you can't trust Linux because it is gigantic, you can't trust a whole another new kernel. Userspace is not blackmagic." The nature of Ginux is irrelevant to that proposition, and, as I think I have clearly shown, it is not well thought out. | | |
| ▲ | asdfsa32 13 hours ago | parent [-] | | The context is not another kernel as an abstract idea here, it is specifically a linux userland kernel. You can't take stuff out of context and make pointless general assertions. | | |
| ▲ | kragen 10 hours ago | parent [-] | | Whether your general assertion was pointless or not, it was false, evidently because you didn't think about which facts about the situation at hand were relevant enough to mention. I'm not convinced that you would have made it to a true statement by doing so, and your efforts in the comments above don't seem to be headed in the direction of a correct thesis, but if you bother to explain what you mean in a coherent way, I'll be happy to engage with that instead. But I'm not going to try to guess what you wanted to say and then discuss that, because I'll probably guess wrong. Instead of complaining when people point out that what you said was false, you should thank them for taking the time to correct you and take the opportunity to learn from it. Then, be more careful about what you say next time, so that you say things that are true instead of false. | | |
| ▲ | asdfsa32 9 hours ago | parent [-] | | No, your assertion that you can bolt a userspace kernel on top of an insecure and bloated kernel to make it secure is false. A userspace kernel is just a vm like any other, in fact, a less secure vm at best. So you should carefully read and consider the conversation before you write, least you come across as arrogant and foolish. | | |
| ▲ | kragen 9 hours ago | parent [-] | | I haven't previously made an "assertion that you can bolt a userspace kernel on top of an insecure and bloated kernel to make it secure", but, as it happens, you can; that's how web browsers execute JavaScript, how Cloudflare Workers run Wasm, and how Firecracker runs virtual machines on Linux, for example. Whether this works or not—or, more defensibly, how great the risk is—depends a great deal on the details. I'm not really interested in how I appear to you, so I recommend you don't waste your time telling me about it. | | |
| ▲ | asdfsa32 9 hours ago | parent [-] | | But those are not Linux kernels and have very different memory model, hardware access, and so on and so on. But I don't think this is a technical conversation anymore, you have some other problems to address and it is best you do that. |
|
|
|
|
|
|
|
|
