Isn't this a bait and switch, that all the c kernel devs were complaining about? That it wouldn't be just drivers but also all new kernel code? The lack of candor over the goal of R4L and downplaying of other potential solutions should give any maintainer (including potential rust ones) pause.
Anyway, why just stop at rust? If we really care about safety, lets drop the act and go make everyone do formal methods. Frama-C is at least C, has a richer contract language, has heavy static analysis tools before having to go to proofs, is much more proven, and the list goes on. Or, why not add Spark to the codebase if we are okay with mixing langs in the codebase? Its very safe.
Frama-C doesn't actually prove memory safety and has a huge proof hole due to the nature of UB. It gives weaker guarantees than Rust in many cases. It's also far more of a pain to write. The Frama-C folks have been using the kernel as a testbed for years and contributing small patches back. The analysis just doesn't scale well enough to involve other people.
Spark doesn't have an active community willing to support its integration into the kernel and has actually been taking inspiration from Rust for access types. If you want to rustle up a community, go ahead I guess?
No, it can track pointer bounds and validity across functions. It also targets identifying cases of UB via eva. Both rust and frama-C rely on assertions to low level memory functions. Rust has the same gaping UB hole in unsafe that can cross into safe.
If we are talking about more than memory, such as what greg is talking about in encoding operational properties then no, rust is far behind both frama-C, Spark, and tons of others. They can prove functional correctness. Or do you think miri, kani, cruesot, and the rest of the FM tools for Rust are superfluous?
My mocking was that that the kernel devs have had options for years and have ignored them out of dislike (ada and spark) or lack of effort (frama-C). That other options provide better solutions to some of their intrests. And that this is more a project exercise in getting new kernel blood than technical merits.
For it to be bait and switch someone should've said "Rust will forever be only for drivers". Has anyone from the Linux leadership or R4L people done that? To my knowledge it has always been "for now".
"But for new code / drivers..." encompasses more than just "drivers" and refers to all new code. I doubt it's a mistake either due to the way the rest of the email is written. And Greg said "no one sane ever thought that (force anyone to learn rust)" just 5 months ago (https://lkml.org/lkml/2024/8/29/312). But he is now telling his C devs they will need to learn and code rust to make new code in the kernel.
> But he is now telling his C devs they will need to learn and code rust to make new code in the kernel.
I don't think this is accurate, Rust is still totally optional. Also, the Rust folks are supposed to fix Rust code whenever it breaks due to changes on the C side. If they fail to do this, the newly-broken Rust code is supposed to be excluded from the build - up to and including not building any Rust at all.
Yes, I know the policy that has been stated and the recent docs on it (https://rust-for-linux.com/rust-kernel-policy). A good portion of the R4L group were trying to avoid this scenario due the toxicity of such a change (especially at this early contentious point, and despite what their online advocates want). I don't think the policy will immediatly change because of his statements, but I find it pretty clear that this is where he wants the project to go.
I'm no kernel dev, but I assume that DMA bindings (what this round of drama was originally all about) fall squarely into "stuff that drivers obviously need".
If you look at the CVE lists, about 70-80% of all c memory bugs are related to OOB Read and Write. Additionally, like rust, fbounds-safety can remove redundant checks if it can determine the bounds. My question is how likely can it be adopted in the kernel (likely high).
I will need to read their conversations more to see if it's the underlying fear, but formalization makes refactoring hard and code brittle (ie. having to start from scratch on a formal proof after substantially changing a subsystem). One of the key benefits of C/Kernel have been their malleability to new hardware and requirements.
> My question is how likely can it be adopted in the kernel (likely high).
My guess is, it cannot. The way -fbounds-safety works, as far as I understand, is that it aborts the program in case of an out-of-bounds read or write. This is similar to a Rust panic.
Aborting or panicking the kernel is absolutely not a better alternative to simply allowing the read/write to happen, even if it results in a memory vulnerability.
Turning people's computer off whenever a driver stumbles on a bug is not acceptable. Most people cannot debug a kernel panic, and won't even have a way to see it.
Rust can side-step this with its `.get()` (which returns an Option, which can be converted to an error value), and with iterators, which often bypass the need for indexing in the first place.
Unfortunately, Rust can still panic in case of a normal indexing operation that does OOB access; my guess is that the index operation will quickly be fixed to be completely disallowed in the kernel as soon as the first such bug hits production servers and desktop PCs.
Alternatively, it might be changed to always do buf[i % buf.size()], so that it gives the wrong answer, but stays within bounds (making it similar to other logic errors, as opposed to a memory corruption error).
Upstream fbounds in xnu has options for controlling if it panics or is just a telemetry event. They are in a kernel situation and have the exact same considerations on trying to keep the kernel alive.
Ah, thank you. If it can just do the equivalent of WARN_ON_ONCE(…) and continue, and the check wouldn’t be slow enough to make people disable it, then yeah, that sounds really good.
Supposedly ~5% (1-29%), but I'm testing my own projects to verify (my guess is higher at 10-20%, but will depend on the code). Supposedly it's to land in gcc at some point but I dunno the time table.
For GCC I have a patch (maybe 10 lines of code) that emits a warning whenever the compiler inserts a trap. You could use a sanitizer, i.e. bounds checking or signed overflow, add code that turns the warning into an error, and so ensure that your code does not have a signed overflow or OOB.
For many use cases, blowing up loudly is strongly preferable to silently doing the wrong thing. Especially in the presence of hostile actors, who are trying to use your out -of-bounds error for their own gain.
One of those things might allow attacker to get access to data they should not have access to or to run arbitrary code on your server. The other does not.
Well, it will be really funny when the executive branch starts firing all the judiciaries security (USMS JSD, under DoJ) to save costs. But secondary outcomes have either not dawned or dissuaded the recent courts on their path to increasing executive power.
Of course they are. Any rational person not blinded by partisanship would be infuriated by this development and immediately demand that DOGE be restrained. Even most partisans would blanch and demand accountability. DOGE advocates know this. Their only recourse is to try to hide it or distract everyone with tangential arguments like they are doing in this thread.
Not shocked at all. The US Gov right now is crazy, and I wouldn't go back with a crazy ex without a huge overhaul first.
And yup, it's about as disrespectful a dismissal as you'd expect from a Musk "plan". I'm not surprised they are having trouble
>"Please work with your supervisors to send this information (once you get it) to people's personal contact emails," the memo added.
Wait, they don't keep personal emails on record? I have to fill that out for every single job I apply to. Pretty sure USAJobs and my State job board required it to.
I guess they either aren't answering or these were more senior personell than I thought.
>Despite having the words "National" and "Security" in its title, it was not getting an exemption for national security
Yeah, they're firing all the probation employees and NNSA got caught in the net.
Probation employees btw include some recently promoted senior employees.
And probation is just the first status.
This is a plan designed to progressively cull employees by status - there'll be another round after this.
Not to fully encapture C's variadic printf, but on the macro front, I've been having fun creating type checking for macros by a constexpr allocation from a _generic switch type check of the args and then checking the result with static_asserts. I think there was a hack before as you mentioned but would have to dig through my tests to find it, but the C23 version is quite clean. Might want see if I can get it to be clean for a variadic printf version.
I wish they would have gone more indepth about the current compiler work, such as stack defenses or fbounds-safety. It should cover OOB read and write safety, which is 70-80% of C's memory vulnerabilities, for a marginal performance overhead and with abi compatibility.
Since the rest of the advisory is demanding full scale rewrites into a new language based on llvm that has officially nuetered it's gcc port, I don't think they really care about those sorts of concerns. Hence my annoyance at their proposal. The fbounds devs do, as the design allows for modified source to be still compilable in alternative toolchains that do not support fbounds (you can remove them via macros) and they are working to add it to gcc. And I don't think its going to matter much soon if it's limited to gcc/llvm, as all the proprietary vendors left and right are dropping their 30+ year compilers to piggyback off llvm (I don't exactly agree with this btw, but it is what it is).
I know this article is more a buisness case presentation than a full demonstration of the field but the TR also misses some points.
Why remove the refrences in the TR to frama-C, cbmc, etc. from the opinion report? They are easier to adopt than the heavier tooling of coq, etc. I'm always suprised to see those tools ignored or downplayed, when it comes to these discussions. I do agree with the TR's sentiment that we need to improve accessibility and understanding of these tools, but this is not a great showing for that sentiment.
Additionally, both articles miss that compiler modified languages/builds are a path, such as fbounds-safety. They will be part of the solution, and frankly, likely the biggest part at the rate we are going. Eg. current stack defenses for C/C++/Rust, unaddressed in safe language design, are compiler based. The compiler extension path is not particularly different than cheri, which requires a recompile with some modifications, and the goal of both approaches is to allow maintainers to band aid dependencies with minimal effort.
The TR handwaves away the question of the complexity of the development of formal method tools for Rust/Unsafe Rust and C++. Ie. rust really only has two tools at the moment: miri and kani (which is a cbmc wrapper). Heavier tools are in various states of atrophying/development. And C++ support from the c family of formal tools such as frama-C, is mostly experimental. It's not assured, that with the continued language development rate of both languages and the complexity of the analysis, that the tools for these languages will come forth to cover this gap anytime soon.
I do not think the claim in the TR that the current unsafe/safe seperation will result in only requiring formal analysis of the unsafe sections is true, as logical errors, which are normal in safe rust, can cross the boundries to unsafe and cause errors, thus nessecitating whole program analysis to resolve if an unsafe section could result in errors. Perhaps it will decrease the constants, but not the complexity. If rust does further restricts perhaps more of the space could be covered to help create that senario, but the costs might be high in both usability and so on.
I'm confused over lines such as "Profiles have to reject pointer arithmetic, because there’s no static analysis protection against indexing past the end of the allocation." Can't frama-c/etc do that? Additionally, section 2.3 is narrower than what is implied by the words "safe" and "out-of-contract" and is more concerned with what C/C++ call "undefined behavior" requirements than contract correctness. Ie. An integer which is defined to wrap overflows and violates the requirement of the function contract, which I can cause in a safe release build rust.
How is it supposed to do that (in the general case)? If I write a C++ program that will index out of bounds iif the Riemann hypothesis is true, then frama-c would have to win the millennium prize to do its job. I bet it can’t.
Often when I look into questions like this I discover the general case is impossible, but simple hysterics can get 99.999% of the cases and so I can get almost all the benefit even though some rare cases are missed.
My own semi-random guess is that "simple hysterics" is indeed how a vast majority (if perhaps not quite 99.999%) of C/C++ devs approaches the code correctness problem - which is why safety mechanisms like the one proposed by OP may in fact be urgently needed. Simple heuristics are likely to be significantly more worthwhile, if appropriately chosen.
If it requires the programmer to bear the responsibility for proper usage (eg. must use checked_add not rely on panic), how's that different than the issues with undefined behavior? I'm also concerned with the differing functional behavior between debug and release, and the mistaken impression it could create (eg. code handles overflow in debug fine due to panic but blows up on release as the proper solution is not used). And a resulting propagation of the overflow error to a precondition of an unsafe call that modifies memory.
> If it requires the programmer to bear the responsibility for proper usage (eg. must use checked_add not rely on panic), how's that different than the issues with undefined behavior?
It comes down to the blast radius for a mistake. A mistake involving UB can potentially result in completely arbitrary behavior. A mistake in the safe subset of a language is still a mistake, but the universe of possible consequences is smaller. How much smaller depends on the language in question.
> I'm also concerned with the differing functional behavior between debug and release
IIRC this was a compromise. In an ideal world Rust would always panic on overflow, but the performance consequences were considered to be severe enough to potentially hinder adoption. In addition, overflow checking was not considered memory safety-critical as mandatory bounds checks in safe code would prevent overflow errors from causing memory safety issues in safe Rust.
I believe at the time it was stated that if the cost of overflow checking ever got low enough checking may be (re)enabled on release builds. I'm not sure whether that's still in the cards.
It's not ideal and can lead to problems as you point out when unsafe code is involved (also e.g., CVE-2018-1000810 [0]), but that's the nature of compromises, for better or worse.
Thanks for the input and links. I'll need to test out the costs of the mitigations.
BTW, I found one of the rust rfc documents helpful for understanding the borrow checker. Do you know if there is a similar rust RFC document for the upcoming polonius borrowchecker, even if it's just a working copy? I'm having trouble finding anything beyond some blog posts.
Unfortunately I'm not super-familiar with developments around Polonius, so chances are what I can point you towards are the same things you found when searching. The most relevant bits appear to be the Polonius book [0] linked from the repo [1], but I don't know how up to date the book is or if there are more up-to-date resources. The RFC book [2] doesn't seem to have anything obviously about Polonius either.
The reviewer's criticism didn't stop the article from being published. Sure, they didn't recommend it initially but that happens.
I'd call it somewhat mild attention to other factors from the one reviewer. The pointing out of issues in data balance, why an nn model, are also good criticism. Here's the review page if anyone wants to read it.
So the question becomes, is his claim of leaving out other factors not greatly influencing and it's just a grift and/or is nature's review process a dog and pony show?
Anyway, why just stop at rust? If we really care about safety, lets drop the act and go make everyone do formal methods. Frama-C is at least C, has a richer contract language, has heavy static analysis tools before having to go to proofs, is much more proven, and the list goes on. Or, why not add Spark to the codebase if we are okay with mixing langs in the codebase? Its very safe.