Post B4sys3z8qTALO4y4UC by linear@nya.social
(DIR) More posts by linear@nya.social
(DIR) Post #B4svAu3pZIluIDtCEK by cwebber@social.coop
1 likes, 1 repeats
Significant raise of reports (on the Linux Kernel Mailing List) https://lwn.net/Articles/1065620/Here's something I think we all will have to contend with, whether you're an AIgen enthusiast or not: attacking is easier than defending, and these things don't get tired and they *are* very good at finding exploits. None of us will be able to ignore that, and we will probably have to listen to real genuine reports from them, even if we reject AIgen input.However, I don't think that's actually the right solution, and I don't think it's sustainable. 🧵
(DIR) Post #B4svAugpEJxoFA8L0i by cwebber@social.coop
0 likes, 0 repeats
The fact of the matter is, most vulnerabilities fall under extremely common patterns, with known solutions:- Confused deputies: capability security can fix/contain this in many cases, more on that later- Injection attacks: primarily caused by string templating, using structured templating also fixes this (quasiquote, functional combinators, etc)- Memory vulnerabilities: solved by memory-safe languages, and yes that includes Rust, but it also includes Python, Scheme/Lisp, etc etc etcThere are other serious vulnerabilities, such as incorrectly written or used cryptography, and others from there, but my primary point is: most damage can be either avoided in the first place or contained (especially in terms of capability security for containment)And... patching AIgen patches is going to get tough and tiring... (cotd...)
(DIR) Post #B4svAvKAs1RIDCXlLM by cwebber@social.coop
0 likes, 0 repeats
I don't think human reviewers are going to be able to keep up with the number of vulnerabilities we're seeing appear. I really don't. Humans won't be able to review at scale, and I also think that there's serious risks for blindly accepting AIgen patches, which for critical infrastructure could also be a path to *inserting new* vulnerabilities.We need to attack this systemically.I have more to say. More later. But that's the gist for now.
(DIR) Post #B4sys3z8qTALO4y4UC by linear@nya.social
1 likes, 0 repeats
@cwebber@social.coop we need microkernel based operating systems with capability-based security enforcement, isolation of components from each other as a baseline assumption, and formal verification of the whole thing at both the code and spec level, and we need all of this quite urgently
(DIR) Post #B4syvj16kMcNVudLZA by linear@nya.social
0 likes, 0 repeats
@cwebber@social.coop things like genode/sculpt are looking more enticing every day that passes by
(DIR) Post #B4sz8EnoOX4HZONgZs by ska@social.treehouse.systems
1 likes, 0 repeats
@dalias For complex objects, the main problem I've identified is the coupling of storage and structure. When storing data in the structure, it's easy to free when you shouldn't and vice-versa.Decoupling storage from structure is the best practice I've learned over the past 15 years, and it's applicable even when you can't reserve your storage in advance.Storage provisioning is useful, but it's mostly useful with another safety aspect: failing as early as possible and avoiding resource allocation in critical moments.
(DIR) Post #B4szGdEjQtZnfSyWjQ by jmax@mastodon.social
1 likes, 0 repeats
@cwebber - I'd be curious about whether LLMs are better than straight up fuzzing. (My suspicion is not, but people are throwing more resources at the LLM efforts.)
(DIR) Post #B4t05uTt4tbbv3W1D6 by dlakelan@mastodon.sdf.org
0 likes, 0 repeats
@linear @cwebber I'd set aside the formal verification requirement to get the rest of it. I really do think microkernels were the right way to go, it's just that in 1992 or whatever the consumer hardware wasn't up to the task. I think probably around 2005 or so the hardware started to be able to afford to do that. But that's approximately the time that VMs and containers took off. Now we have this giant mess.
(DIR) Post #B4t05ufwM5FMWR9dzs by linear@nya.social
0 likes, 0 repeats
@dlakelan@mastodon.sdf.org @cwebber@social.coop i do not think that setting aside the formal verification is wise, and i also do not think it poses a technical barrier that we cannot surpass. especially since we already have formally verified microkernels with capability-based security that can be used today within full desktop operating systemswhat needs to happen is for people to put the pieces together and polish it into a system regular folks can actually use
(DIR) Post #B4t13LeFiMSXGJhpTM by dlakelan@mastodon.sdf.org
0 likes, 0 repeats
@linear @cwebber If you mean formally verifying the microkernel itself... yeah. I'm good with that. Isn't L4 formally verified? If you mean formally verifying every userspace daemon... Nice to have but I'm not holding my breath.
(DIR) Post #B4t13LoX68gNmCW2Uq by linear@nya.social
0 likes, 0 repeats
@dlakelan@mastodon.sdf.org @cwebber@social.coop kernel is the bare minimum, i'd also want verification of at least specs around the hardware abstraction layer and how hardware related daemons talk to everything else. but it should definitely be possible for common system components and daemons as well, and i think should be mandatory for trusted daemons that supervise or manage other untrusted onesi doubt everything will be formally verified, but it is nonetheless a goal that should be worked towards, while finding ways to develop standard practices and make it easier to apply everywhere
(DIR) Post #B4t1eiw65sSECcsIT2 by linear@nya.social
0 likes, 0 repeats
@dlakelan@mastodon.sdf.org @cwebber@social.coop i'm glossing over a lot with the "trusted" vs "untrusted" here, and i recognize that. i've been thinking about this for the better part of a decade and conveying my mental model for this is not possible in a few pots in a social media threadi just have not had the motivation or resources to spend on taking existing work in seL4/genode and assembling it with other pieces into the thing i'd like, writing specs, finding people to collaborate with on this, etc. life is busy and i already have so many projects
(DIR) Post #B4t3NOlq10Aee6wUjI by BetaRays@p.changeme.fr.eu.org
0 likes, 0 repeats
@linear @cwebber SeL4?
(DIR) Post #B4t3NOwpM8xfCC5GrI by linear@nya.social
0 likes, 0 repeats
@BetaRays@p.changeme.fr.eu.org @cwebber@social.coop this would be part of my vision, yes
(DIR) Post #B4t3Vo1S0tEFHPFotk by navi@social.vlhl.dev
0 likes, 0 repeats
@ska @dalias "decouple storage from structure" is one of the best things but when i first started trying to think about it more, it was hard to wrap my head around how to design things to work like thati feel like a page of example apis or a book or smth would be very helpful for new folks not familiar with it
(DIR) Post #B4t3VoBNPzAVmBtkMy by ska@social.treehouse.systems
1 likes, 0 repeats
@navi @dalias Yeah, the way most people write C with pointers everywhere - because that's what they've been taught - isn't very compatible with that. Again, it comes down to: the way we teach C is really, really bad.Will you co-author my C book, that I'll write when I retire from coding? (that probably means in two decades or more 😝)
(DIR) Post #B4t4IUIU8k66ICR2S8 by dlakelan@mastodon.sdf.org
0 likes, 0 repeats
@linear @cwebber I agree it would be nice to have, but I honestly think it primarily prevents progress. We'd be wildly better off with microkernel OSes that are at the same level of hackiness as the Linux kernel, and maybe have decent interfaces that could get replaced piecemeal as people came up with alternative implementations in memory safe languages, and then maybe formally verified at a later date. Right now, you have to be comfortable working in kernel space to even do anything
(DIR) Post #B4t4IUWJJL9kz4u50C by linear@nya.social
0 likes, 0 repeats
@dlakelan@mastodon.sdf.org @cwebber@social.coop right now, this minute, you can go download SculptOS and have a microkernel-based OS with capability security that can run on a laptop and use its iGPU and run a web browser and virtualize linux and build itself using the Genode framework it is based on. and you can use that framework to swap out the process-level-virtualization-based default microkernel (NOVA iirc) with the formally verified seL4 (or other L4 family kernels) and never have to care about the API/ABI differences between microkernels because it abstracts that for you, nor the code inside the kernel.
(DIR) Post #B4t4cIUfjbVBTba6wC by btel@mastodon.social
1 likes, 0 repeats
@cwebber "- people will finally understand that security bugs are bugs, and that the only sane way to stay safe is to periodically update, without focusing on "CVE-xxx""I am not sure how this is going to work. How can be sure that the newest update is not a troyan horse (cf. recent axios breach)?
(DIR) Post #B4t5AD2iVVhqPtfypk by linear@nya.social
0 likes, 0 repeats
@dlakelan@mastodon.sdf.org @cwebber@social.coop this is to say, what you are asking for exists, and has existed in a usable state for well over a decade, and is in some cases more feature complete than some other open source operating systems that people use and even daily driveyou can run it on a pinephone, too
(DIR) Post #B4t5EevUmLvM3QQ6tc by dlakelan@mastodon.sdf.org
0 likes, 0 repeats
@linear @cwebber That's cool! I honestly had not followed any of this. I might have to dedicate an older laptop I have no real use for to this just for fun.
(DIR) Post #B4tdf6UYJK6jW9bCk4 by teajaygrey@snac.bsd.cafe
0 likes, 0 repeats
(se)L4 I think fits such criteria? It is already widely deployed (e.g. Apple's Secure Enclave).Problematically? I don't think any of the L4 kernels were "self hosting" last I checked? Maybe that has changed.BS such as that, would have received failing grades in the 1980s.Alas, we live in a different era now, where cross compiling is de rigueur even if it is awful in practice.If I had a wish granting fairy or whatever? I would totally task someone(s) to make the L4 microkernel family self-hosting, so it doesn't need a Linux to boot strap.CC: @cwebber@social.coop
(DIR) Post #B4tdf6ol6CGqWp3LEm by linear@nya.social
0 likes, 0 repeats
@teajaygrey@snac.bsd.cafe @cwebber@social.coop yes, see further downthread
(DIR) Post #B4tdhwaJbLIFezeI9w by linear@nya.social
0 likes, 0 repeats
@teajaygrey@snac.bsd.cafe @cwebber@social.coop and go learn about Genode / SculptOS
(DIR) Post #B4tdmgxt6Qq4fEwGie by cwebber@social.coop
0 likes, 0 repeats
@linear @dlakelan I am aware of Sculpt / Genode and have run it on physical hardware before! I am also working on tech that is also part of the answer.There is real work happening! It's going to take multiple efforts from multiple angles to get there