Verify the Rust's Standard Library's 7,500 Unsafe Functions - and Win 'Financial Rewards' (devclass.com) 85
The Rust community has "recognized the unsafety of Rust (if used incorrectly)," according to a blog post by Amazon Web Services.
So now AWS and the Rust Foundation are "crowdsourcing an effort to verify the Rust standard library," according to an article at DevClass.com, "by setting out a series of challenges for devs and offering financial rewards for solutions..." Rust includes ways to bypass its safety guarantees though, with the use of the "unsafe" keyword... The issue AWS highlights is that even if developers use only safe code, most applications still depend on the Rust standard library. AWS states that there are approximately 7.5K unsafe functions in the Rust Standard Library and notes that 57 "soundness issues" and 20 CVEs (Common Vulnerabilities and Exposures) have been reported in the last three years. [28% of the soundness issues were discovered in 2024.]
Marking a function as unsafe does not mean it is vulnerable, only that Rust does not guarantee its safety. AWS plans to reduce the risk by using tools and techniques for formal verification of key library code, but believes that "a single team would be unable to make significant inroads" for reasons including the lack of a verification mechanism in the Rust ecosystem and what it calls the "unknowns of scalable verification." The plan therefore is to turn this over to the community, by posing challenges and rewarding developers for solutions.... A GitHub repository provides a fork of the Rust code and includes a set of challenges, currently 13 of them... The Rust Foundation says that there is a financial reward tied to each challenge, and that the "challenge rewards committee is responsible for reviewing activity and dispensing rewards." How much will be paid though is not stated.
Despite the wide admiration for Rust, there is no formal specification for the language, an issue which impacts formal verification efforts.
Thanks to Slashdot reader sean-it-all for sharing the news.
So now AWS and the Rust Foundation are "crowdsourcing an effort to verify the Rust standard library," according to an article at DevClass.com, "by setting out a series of challenges for devs and offering financial rewards for solutions..." Rust includes ways to bypass its safety guarantees though, with the use of the "unsafe" keyword... The issue AWS highlights is that even if developers use only safe code, most applications still depend on the Rust standard library. AWS states that there are approximately 7.5K unsafe functions in the Rust Standard Library and notes that 57 "soundness issues" and 20 CVEs (Common Vulnerabilities and Exposures) have been reported in the last three years. [28% of the soundness issues were discovered in 2024.]
Marking a function as unsafe does not mean it is vulnerable, only that Rust does not guarantee its safety. AWS plans to reduce the risk by using tools and techniques for formal verification of key library code, but believes that "a single team would be unable to make significant inroads" for reasons including the lack of a verification mechanism in the Rust ecosystem and what it calls the "unknowns of scalable verification." The plan therefore is to turn this over to the community, by posing challenges and rewarding developers for solutions.... A GitHub repository provides a fork of the Rust code and includes a set of challenges, currently 13 of them... The Rust Foundation says that there is a financial reward tied to each challenge, and that the "challenge rewards committee is responsible for reviewing activity and dispensing rewards." How much will be paid though is not stated.
Despite the wide admiration for Rust, there is no formal specification for the language, an issue which impacts formal verification efforts.
Thanks to Slashdot reader sean-it-all for sharing the news.
7500 sounds like a lot. (Score:3)
Has an audit been conducted to see which of these functions could be reworked in a 'safe' manner or those which are only present for interoperability with C?
New paradigms and what not...
Need list of payout amounts (Score:2)
Where's the list of payouts for the bug types found?
Re: (Score:3)
I think that very few of the unsafe functions in the standard library are unsafe because of C interoperability.
You need unsafe where ever you can't know for sure if data exists or not -- so that's Vec and most of the data structures that have unsafe in them. And you also need unsafe if you are manipulating data that is supposed to be in some format but might not be -- so that is String, and transmuting.
As far as I can see, only the CStr verification challenge is actually for C interop.
On the more general qu
Bug bounty (Score:4, Funny)
Pardon me while I go and write myself a minivan [snbforums.com].
Pay some workers? (Score:3, Insightful)
If Amazon wants to have verify the safety of Rust functions, why don't they do it themselves? Is it to much to ask that businesses actually hire workers to do the work that they want done? I feel like this is rich man begging that the poor contribute to do work for free so that the rich man can afford another private jet.
Re:Pay some workers? (Score:5, Informative)
Is it to much to ask
In this case, yes. The skills involved are not easily hirable. It's rarified talent: elite programmers that can comprehend "unsafe" and all of it's implications in the Rust language (which are subtle, despite what the prevailing peanut gallery around here thinks,) have a deep understanding of one or more platform (winapi, posix, etc.) APIs that unsafe is frequently used with, deep experience with one or more CPU architecture memory models and synchronization primitives, knowledge of and the ability to analyze compiler behavior, and other non-work-a-day "application" programmer caliber skills. The cohort of people capable of all of this is small and already well engaged elsewhere. Further, it's the sort of mentality that doesn't emerge with any frequency from employer provided education and training.
By offering bounties, Amazon can leverage these skills beyond its own payroll.
Re: (Score:3)
Problem is, the people that can do this competently do not usually work for "bounties" (i.e. peanuts).
Re: (Score:2)
Re: (Score:2)
Very easy to hire: make the bounty prize as a work contract.
FREE LABOR? (Score:2)
So you volunteer your time to attempt to understand and solve problems for free. If you manage to find a solution that they deem good enough to use, then they pay you something for your effort. Meanwhile everybody else who attempts gets nothing even if they succeed, only the one deemed best and first wins.
This is apposed to paying employees for their work until they eventually find solutions or give up. Even outsourced workers are paid.
Academics will do so to get published and they'll try to find somethin
Re: (Score:2)
At the end of the day, this is all volitionary. Nobody is being coerced into anything they haven't chosen themselves. The rest is whatever collection of grievances you choose to indulge for whatever reasons you have.
Who wrote those 7500 functions? (Score:3, Insightful)
-ffs, stop clowning around with community rules and do the work you claim you have done.
Re: (Score:2)
Security and safety is a process, not a destination. How do you have a five digit id here and know nothing about technology?
Re: (Score:1)
How do you have a five digit ID and don't recognize a pointed comment.
The gist is that Rust is no better than C if you have to worry about programming around unsafe primitives. In fact it's far worse. A perceived guard rail will tend to make programmers act with more disregard for security.
The better paradigm is to use C and program it safely. Take away the pablum and guard rails and safety net and add a little healthy fear and you'll end up with better code.
Perceived safety is more dangerous than known
Re:Who wrote those 7500 functions? (Score:5, Funny)
It's difficult to take you seriously after you fail to count up to 6. Off-by-one errors are exactly the kind of mistakes C programmers make that are easily caught by Rust and most other languages. Maybe you're not as smart as you think you are.
Re: (Score:1)
If that's the kind of thing that Rust programmers depend on, then maybe it's a good thing they don't use C. Maybe they can continue playing with duplo.
That's actually kind of a good analogy. Writing complex software in Rust is like building a Millennium Falcon with duplo. It's either going to be a simplistic approximation, or oversized, or dependent on pre-fabricated detail work pieces in the form of calling on libraries written in real languages.
Re: (Score:2)
Maybe you should play with those duplos. You've not demonstrated the ability to count, which is paramount to making safe C code.
Re: (Score:2)
That is the kind of mistake _bad_ C programmers make. But you know what? Bad coders write bad code in _any_ language.
Re: (Score:2)
Bad coders write bad code in _any_ language.
Fifty percent of all programmers writing production code today are worse than average programmers. Ninety percent of all programmers writing production code today think they're better than average and the other ten percent think they never make a mistake ever.
Re: Who wrote those 7500 functions? (Score:2)
Yes, bad programmers gonna write bad code.
The question is, what happens after that?
Does the bad code result in a compile-time error, forcing the bad programmer to fix his mistake before he can continue, or will it result in a subtle runtime bug that alienates users and then costs the company weeks of sqa and developer time to find and fix?
Sane people prefer the former.
Re: (Score:2)
You seem to be under the illusion that bad compilers can find logical errors and the like. They cannot.
Re: (Score:2)
You seem to be under the illusion that bad compilers can find logical errors and the like. They cannot.
They can't find all logical errors, true. But the ones that can be found by a compiler, should be.
Re: (Score:2)
Bad coders write bad code in _any_ language.
With C, bad programmers write buggy code.
With Rust, bad programmers are unproductive.
Re: (Score:2)
You wish. Well, maybe there will be some effect because rust is hard to learn. Other than that, most security bugs these days are not things Rust could have prevented.
Re: (Score:2)
The borrow-checker will not stop this. However, access to arrays by index is pretty unusual in Rust. To sum the elements in an array you would use an iterator.
So, a language feature does avoid that class of errors in many common situations.
Re: (Score:2)
I wasn't talking about C++ at all, but the key point here that we seem to be agreeing on is language features can effectively prevent certain classes of error; the particular off-by-one error has been avoidable using the `foreach` loop in many languages for a while. It is great that C++ has this and not that much of a surprise; Rust has borrowed (erm) many things from other languages.
I don't know why you find people screaming at you a lot and I can't answer for them, of course. Did you start of by calling t
Re: (Score:2)
let total: u32 = data.iter().sum();
Re: (Score:2)
you "can't make bugs in Rust" fanbois are just full of shit.
Rust programs can have bugs.
But certain classes of bugs, including memory errors and race conditions, are much less common in Rust.
Re: (Score:2)
> Maybe you're not as smart as you think you are.
https://www.youtube.com/watch?... [youtube.com]
Re: (Score:2)
Indeed. Probably the only reason we do not see widespread problems with Rust is because it is so rarely used at all.
Re: (Score:2)
I think you need to work on your sarcasm...
Re: (Score:3)
That is why Rust requires the use of "unsafe". The guard rails do not just magically disappear you have to request them.
And the whole point of this effort is to make sure that those parts of the standard library that use unsafe, they do have those guard rails.
Re: (Score:3)
Inside an unsafe block you can perform operations that you are disallowed elsewhere, so this is why they want to provide formal verification inside these blocks in the standard library for use in CI environments.
That is an advance. The problem is that formal verification is quite a lot of work to set up and also requires quite a lot of CPU. Otherwise, it would be good to build it into the language and the compiler. But for now having those tools inside the standard library would be a good thing. Outside the
Re: (Score:2)
The standard library is exactly where you would expect to see the biggest use of unsafe. This is where the safe abstractions that you need the most are built. Consider the Vec which is Rust's list type. You need to manipulate pointers and space that is potentially empty, hence the need for unsafe. You see the same thing in Python and Java with the list and array implementations; both are implemented in "unsafe" python or Java" which is the role C plays in these languages. If you do the standard library well
Re: (Score:2)
It is true with all "memory safe" languages that they are built on some part that is not itself memory safe. It is possible, for example, in Python to cause an out of bounds memory access or buffer overflow with a list; all you need is the right bug in the C implementation of that list.
Safe rust can guarantee that certain errors cannot happen but is dependent on the safe abstractions over unsafe operations fulfilling their contracts. So, you can buffer overflow a Rust vec; all you need is the right bug in t
Re: (Score:2)
Okay, so that is the conclusion you draw from an article about the attempts of the Rust foundation to address the problem that you can't check every issue at compile time and to secure the standard library using static validation running during testing.
To me, I conclude that the Rust foundation is aware of the limitations of its safety and is attempting to apply more complex technology to address this. All of which is enabled by a language feature that limits the amount of code that you need to do this to,
Re: (Score:2)
Not actually safer you say? Huh, imagine that. (Score:1)
Re: (Score:2)
Alas, this is pretty much what slashdot and large parts of the internet have become aggressive, hostile and full of ad hominem. I am sure that it used to be better in the past, but perhaps that is me getting old.
The commit you referenced was for checking there is any accidental leetspeak in the Rust core. In practice this just avoided using a Javaism. How is this "woke" in some sense?
Re: (Score:2)
Yes, both "babe" and "cafe" are a words. That is what they are looking for.
Re: (Score:1)
That is not surprising, as we have to deal with so many people who do not know what an Ad Hominem is.
You feel "insulted"? You shouldn't! You should feel dumbfolded.
Re: (Score:2)
Typical Rust proponent, aggressive, hostile, ad hominem attacks. Maybe Rust would be safer if their programmers weren't making it woke. https://github.com/rust-lang/r... [github.com]
The commit you mentioned is actually a good one. I tried imagining me using 0xcafebabe as a hex string, but this somehow doesn't work. Why would I ever use hex-words in code? And regardless of its origin it is a good thing to remove such stuff from a codebase since it has no point in being there in the first place.
Woke in itself is a far greater danger than people tend to realize. Take a look at the Stallmann-report and what and who caused it, it is directly linked to the people behind the covenant code of
Re: (Score:2)
The commit is actually rather dumb. Using monotonic sequences like 0x12345678 has a higher rate of false matches. For example, 0x12345678 has the same difference between successive bytes (0x22 = 34 decimal), so it is more likely to occur by coincidence. Three of the bytes are also normal printing characters.
If you cannot imagine yourself using hex that spells words, well, that shows a failure of imagination and limited thinking on your part rather than the original code being bad.
Re: (Score:2)
The commit is actually rather dumb. Using monotonic sequences like 0x12345678 has a higher rate of false matches. For example, 0x12345678 has the same difference between successive bytes (0x22 = 34 decimal), so it is more likely to occur by coincidence. Three of the bytes are also normal printing characters.
If you cannot imagine yourself using hex that spells words, well, that shows a failure of imagination and limited thinking on your part rather than the original code being bad.
While the first part of your explanation is a good start for a discussion, I don't get why you feel the need to end it with an ad hominem attack. Which immediately disgraces the validity of your initial argument and kills every possibility of a useful discussion.
I don't imagine myself using hexwords not because I lack imagination but because I am very reluctant to use profanity in code. It is like trying to read a good technical documentation that constantly uses smear words or tries to drive a political ag
Re: (Score:2)
Stupid people should be called out so that they realize when they are being stupid. They're stupid, and will not realize it otherwise.
None of these words are profane. The point of these magic values is not to write them multiple times in code. Guess what: You are still stupid.
Re: (Score:2)
You realize that by using ad hominem you are actually the one who calls himself out as the stupid one?
Re: (Score:2)
That is something a stupid parent would tell a stupid child. It's too bad that you don't understand why it is entirely wrong.
Re: (Score:2)
That is something a stupid parent would tell a stupid child. It's too bad that you don't understand why it is entirely wrong.
Since you are in no way interested in a reasonable talk about the real issue at hand I refrain from this discussion, as there is nothing to be gained.
Re: (Score:2)
I am interested in reasonable talk. I am not interested in pretending a string of vacuous comments is anything else in order to coddle a fragile fool who thinks "cafe babe" and "dead food" are profanity.
Re: (Score:2)
I am interested in reasonable talk. I am not interested in pretending a string of vacuous comments is anything else in order to coddle a fragile fool who thinks "cafe babe" and "dead food" are profanity.
You are kidding, right? Every single comment you made was the complete opposite of "reasonable talk". And in this one you still go down and call me a "fragile fool". Where exactly is the "reasonable talk"?
There were many possibilities for engaging in "reasonable talk". Initially I made the point of showing the origin of the 0xcafebabe. Which in itself is quite interesting. I also pointed out that I deem Wokeness as a dangerous thing. Also something on can have a reasonable talk about. I said that I don't li
Re: (Score:1)
Security and safety is a process, not a destination.
While this is true, it's also not a reasonable answer to the GP comment, as it doesn't address the Rust devs (and various other proponents) claiming that Rust has reached a point which it hasn't.
Re: (Score:2)
Re: (Score:2)
For your safety, we have added this steel safety rail to the termite ridden observation platform.
Next week: Man falls to his death. He was found at the bottom of the canyon still clutching the steel safety rail.
Re: (Score:2)
This is why safety rails are not on their own enough. You also need building standards and regular inspections.
Translating the analogy to coding: test sets, continuous integration and, maybe, formal verification of the bits that you can't do otherwise.
Re:Who wrote those 7500 functions? (Score:4, Insightful)
These are functions already marked as being unsafe, meaning they already can be misused, and that's ok. Say for example Vec::get_unchecked(), which lets you get a value from a specified index without doing a bounds check. The compiler leaves it up to the programmer to ensure that they aren't doing out of bounds access, and no sane programmer would do this unless there was really some compelling reason to (which is rare, hence in the Rust community any use of unsafe generally carries whiff of code stench with it.)
Some unsafe functions are less obvious in the way they may be misused compared to a bounds check, like say std::mem::transmute. A lot of thought about that already has been done, so what's needed is a bit more creativity to find ways that these functions can be automatically checked for soundness (with some existing tooling, like say clippy or plain ol' check.) They specifically enumerate 13 of them, with transmute being the first. Not much different from the reasoning behind bug bounties: Anybody can make a security or safety scheme that they themselves can't break. Making one that nobody can break needs a much broader set of input that any one team is unlikely to deliver.
This is exactly why sites like bugcrowd exist. Though somebody has to fund it. This is exactly what they're doing. I actually reported a vulnerability in Windows Hello last year that I found somewhat on accident, but probably wouldn't have bothered reporting if there was no bounty involved because that required actually building a proof of concept exploit kit (which I wrote in rust, by the way) just to even get credit for the CVE.
Re: (Score:2)
The statement "if used incorrectly" applies to those sections of Rust which are marked as unsafe. But they are marked as unsafe and they are only a percentage of the whole library, so presenting a smaller surface for formal verification outside the normal compiler checks than otherwise.
That isn't true in C/C++.
Re: (Score:2)
I thought the point of Rust was all this safety, and now they are revealing that their standard library isn't even audited?
At least they're trying.
Meanwhile, C just gave up and let footguns like strncpy() fester in their standard library for half a century.
Re: Who wrote those 7500 functions? (Score:2)
Re: (Score:2)
That's hilarious, nobody learns C in computer science.
Re: (Score:2)
Re: (Score:2)
Re: (Score:2)
Verified not audited.
This is about producing or using tools that can formally verify those parts of the code that the normal type system cannot, and integrated these tools into the standard CI system for the rust standard library.
Re: (Score:2)
Even if they were audited, are they formally verified? Probably not. Are the C library function they may end up calling in many cases formally verified? Most certainly not. Though, you could be using CompCert for compiling them, but it doesn't stop you from compiling garbage.
Audition isn't a silver bulletâ"and actually formal verification isn't either, if you are verifying the wrong thing. But the bar for formal verification is a very high and the results increase the trustworthiness of the code by a l
Reminder (Score:4, Insightful)
Re: Reminder (Score:3)
The point of programming is to automate processes so that they can be done quickly, cheaply, and reliably by a computer, rather than slowly and inconsistently by a human being. If you consider process automation to be a bad thing because your salary depends on manually re-performing the same operations instead of automating the ones that can be automated, then you have missed the point. Verification of code safety is one such process, and Rust is designed to make that process easier to automate.
Re: Reminder (Score:2)
Rust needs formal behavioral verification tools (Score:2)
Re: (Score:2)
Kinda?
Rust didn't obviate the need for testing: the borrow checker prevents memory errors which is necessary but not sufficient for correct code. You still need to know if your code is doing the right thing.
If you want to prove behavioral correctness, Ada spark is right over there. Notev that they have apparently taken inspiration from rust recently and introduced a borrow checker is order to allow a number is pointer based things which were previously forbidden.
Of course you then need to verify that your c
Sounds like a sketchy raffle (Score:2)
Re: Sounds like a sketchy raffle (Score:2)
Re: (Score:2)
I cant understand that from the knowledge the Rust foundation is supporting an initiative to use formal verification of their standard library, that you would conclude their QC is broken. My own conclusions would be that if someone wishes to go the hassle of formal verification, then they probably already have good QC, but aware that all testing and all QC has limitations.
Paper on Rust security (Score:2)