But there's a non-zero chance that someone could develop a skillset for iteratively cleaning up into something tolerable.
And then there are non-goal things that could grow out of the project, e.g. some form of linter feedback "can't translate into tolerable rust because of x, y and z". C people could look into that, and once the code is translatable into good rust, why translate.
If that was an outcome of the project, some people might find it easier to describe their solution in runnable C and let the "translator/linter" guide them to a non-broken approach.
I'd certainly consider all these positive outcomes quite unlikely, but isn't it pretty much the job description of DARPA to do the occasional dark horse bet?
If you give developers a shitty codebase then those developers will leave to work somewhere else.
After a few years of working on this codebase we had 88% turnover. 1 in 10 developers remembered the original project's design philosophy and intention.
It wasn't a good situation.
No chance. CBMC is amazing, but have you actually tried formally verifying a "real" program?
I agree replacing with a hand-architected Rust version is clearly the better solution but also more expensive. I think they're going for an RLBox style "improve security significantly with little-to-no effort" type product here. That doesn't mean you shouldn't do a full manual rewrite if you have the resources, but it's better than nothing if you haven't.
Yes. Every day. It's actually quite easy to do. Write shadow methods covering the resources and function contracts of called functions, then verify the function. Repeat all of the way up and down the stack. It adds about 30% overhead over just TDD development.
The biggest issue you will run into with bounded model checking is recursion and looping. In these cases, you want to refactor the code to make it easier to formally verify outside of the loop. Capture and assert on loop variants / invariants, and feed these forward in assertions on code.
There's no way I can capture all of this in an HN comment, but to get CBMC to work, you need to break down your code.
Think of shadow functions as the specifications that you are building. Unlike proof assistants or Frama-C, you write specifications in C itself, and they work similarly to code. Often, the same contracts you write in these specifications can be shared by both the shadow functions and the real functions they shadow.
I take a bottom-up approach to model checking. I'll start by model checking the lowest level code, then I'll shadow this code to model check code that depends on it. In this way, I can increase the level of abstraction for model checking, focusing just on the side effects and contracts of functions I shadow, and move up the stack toward more and more general code.
There is no such mentality anywhere. There is a ton of software that's much better off left alone in a dynamic language, or a statically typed language with a garbage collector (like Golang). Good engineers understand the idea of using the right tool for the job.
The push is to start reducing those memory safety CVEs because they have been proven to be a real problem, many times over.
> mechanical translation is a poor means of doing so
Agreed. If we could automatically and reliably translate C/C++ to Rust it would have been done already.
> Spend the time planning better architecture and designing a better software system, and find a way to replace it piece by piece.
OK, I am just saying that somewhere along that process people might get a bout of confidence and tell themselves "oh, we're doing C much better now, we no longer write memory safety bugs, can't we stop here?" and they absolutely will. Cue another hilarious buffer overflow CVE 6 months later.
> I think a far better and more mature process is to update C to modern C and use a model checker such as CBMC to verify memory, resource, and integer math safety.
A huge investment. If you are going to do that then you might as well just move to Rust.
> One gets the same safety as a gradual Rust rewrite
Maybe, but that sounds fairly uncertain or far from a clear takeaway to me.
My experience tells me that if a tech stack supports certain safety guarantees by default that this leads to measurable reduction of those safety problems when you switch to the stack. People love convenient defaults, that's a fact of life.
The apparently inconvenient truth is that most programmers are quite average and you can't rely on them going above and beyond to reduce memory safety errors.
So I don't buy the good old argument of "just hire better C programmers". We still have a ton of buffer overflow CVEs regardless.
And I never "pretended it's impossible to avoid safety issues in C". I'll appreciate if you don't clump me in some imaginary group of "Rust proponents".
What I'm saying is this: use the right tool for the job. The C devs have been given decades and yet memory safety CVEs are still prevalent.
What conclusion would you arrive at if you were in my place -- i.e. not coding C for a living for like 18 years now but still witnessing it periodically crapping the bed?
I'm curious of your take on this. Again, what other conclusion would you arrive at?
For example, let's look at the "hire better C programmers does not work" argument. Like every good propaganda it starts with a truism: In this case that even highly skilled C/C++ programmers will make mistakes that could lead to exploitable memory safety issues. The problem comes from exaggerating this to the idea that "all hope is lost and nothing can be done". In reality one can obviously do a lot of things to improve safety in C/C++. And even one short look at CVEs should make it clear that there is often huge room for improvements even with relatively simple measures. For example, a lot of memory safety bugs in C/C++ come from open-coded string or buffer manipulation. But it is not exactly rocket science to abstract this away behind a safer interface. But once this is understood, the obvious conclusion is that addressing some of these low-hanging fruits would be far more effective in improving safety than wasting a lot of time and effort in rewriting in Rust.
That's not "in reality", that's "in theory". Because in actual reality, people still write the good old buffer overflow bugs to this day.
I don't think anyone reasonable is disputing that we indeed can improve C/C++ programming. The argument of myself and many others like myself is: "a lot can be done but for one reason or another it is STILL NOT being done". Likely the classic cost cutting but there are likely other factors at play as well.
> But once this is understood, the obvious conclusion is that addressing some of these low-hanging fruits would be far more effective in improving safety than wasting a lot of time and effort in rewriting in Rust.
Explain why this has not been done yet. Explain why Microsoft, Google and various intelligence agencies attribute memory safety bugs to between 60% to 75% of all CVEs and demonstrable exploits that they are aware of.
Please do, I am listening. Why has almost nothing been done yet?
Secondly, "wasting a lot of time and effort in rewriting in Rust" is an empty claim. To demonstrate why, I ask you this: at which point the continued cost of investing in endlessly patching C/C++ and all its glorious foot-guns becomes bigger than the cost a rewrite?
Surely at one point just endlessly throwing money at something that gives you a 1% return of investment (in terms of getting more stable and less dangerously buggy) does indeed get more expensive than starting over?
I have no clear answer because it depends on the organization, the tenure of C/C++ and the devs in the org, and many others. It's strange that you pretend to have the answer.
That's because while the technology exists, it is not widely communicated. That's not a fault of C, and that's not something that any language can solve.
> Explain why this has not been done yet.
See above.
The technology to make C and C++ safer is not yet widely used. But, it exists and it is being used. I use it on every firmware and OS project that I currently work on. The code we produce is free of memory errors, integer errors, API misuse errors, resource management errors, cryptography errors, confused deputization errors, and a host of other errors that our specifications are designed to catch. That goes well beyond what Rust or any other language can provide on its own. But, to be fair, Rust developers can do this using similar tooling.
It's laudable that you wish to rid the world of memory errors. I want to normalize going three or four steps further. Rust by itself won't get us there.
If you say so. Rust clearly does, and before you go saying "but `unsafe` exists!" I'll have to remind you that (1) scarcely any Rust devs reaches for that and (2) it still keeps quite a lot of guarantees and only relaxes some. Some, not all. Not even most.
> It's laudable that you wish to rid the world of memory errors. I want to normalize going three or four steps further. Rust by itself won't get us there.
Well now we are on the same page. I never said "ONLY Rust will save us", I am saying that Rust clearly can get us further than we are right now. If there's something even more accessible, less verbose, and with not such a cobbled together Frankenstein async implementation like Rust, I'll start using it tomorrow.
Until it exists at the kernel layer, the firmware layer, the runtime library layer, and the application layer, these issues still exist. CVEs come out weekly for memory errors in Linux, in firmware, in operating system libraries, and in application libraries. We need to think beyond rewriting code in one language or platform, and instead think about technologies that we can apply to all languages and platforms, including C and Rust.
> I am saying that Rust clearly can get us further than we are right now.
As can bounded model checking, without having to teach developers a new language with new idioms.
> If there's something even more accessible, less verbose, and with not such a cobbled together Frankenstein async implementation...
Indeed there is. Reach for the bounded model checker that works with your existing language or platform. Pour over the manual, and look at existing practical examples.
If you like Rust, feel free to use it. But, if you prefer C/C++, Pascal, Ada, Python, C#, Java, or Modula2, that's fine. Either use an existing bounded model checker for that language or port CProver / GOTO to that platform. Rust developers ported CProver to Rust via Kani, because they also recognize that writing safer code can't be done by language alone.
I don't think it's necessary to push people to use different languages or platforms to write safer code. They just need to use or port existing tooling and learn safer coding practices. If I come at firmware developers or old school OS developers with "we need to use Rust", the conversation is immediately shut down and I'm considered a fool. If, instead, I show them tooling that allows them to maintain their existing code base and make it safer, I get much further.
CBMC translates C -- the same language -- to an SMT solver. A different target but the same language.
It is true that new idioms will often be discovered along the way of converting existing C to pass the bounded model checker in every branch condition and in every case. However, software that is already relatively safe will require very little modification. I've seen it go both ways. Simpler code bases can pass model checks relatively unscathed. More complex code bases require refactoring to pass model checking.
To my point, the code base can remain in C, and can be model checked gradually. It doesn't have to be ported to a different language or platform. But, it will require added assertions and some refactoring to make the execution of code more clear. It's still in C. The specifications are specified in C using regular assertions. The only thing that changes is that one will often use shadow methods -- still written in C but simpler than the functions they are shadowing -- in order to model check other functions.
Other bounded model checkers like JBMC, Kani, or PolySpace work in similar ways.
Better process and better tooling allows us to write better software. Bounded model checking is an incredibly useful bit of tooling that allows us, within context of the software, to demonstrate that certain conditions do not arise. This includes memory errors, resource errors, and other classes of errors. The limitation is the faithfulness of the translation to SMT and the complexity of the code being modeled. The former has gotten quite good with CBMC 6, and the latter can be managed through careful refactoring and shadow function substitution.
Is it magic? There is no such thing. But, it is a practical tool that is available for use today.
One need not wait until an entire web browser is verified using it. It can scale to this, but given the unreasonable size and scope of web browsers with respect to this challenge, which are basically operating systems and suites of software in one these days, that's like saying, "verify all software then blog about it."
Solaris has already been doing it since 2015, ARM more recently, we have Microsoft putting the big buckets into CHERI (including custom FPGA boards for testing), the new CoPilot+ PCs architecture with Pluton, and while AMD/Intel attempts weren't quite right like MPX, they will surely do something for x64 as well.
How, because other solutions are being explored? That's not due to a failure of one thing, but because both defense in depth and a desire to fix existing systems with no additional engineering are paths that security researchers and vendors explore. Not everyone will converge on a single solution, even when that solution is practical.
Just because something is not being used universally doesn't mean that it has failed. Moreso, it is not widely known about, and there persists rumors that it requires extraordinary effort, often reinforced by well meaning, but rather outdated advice.
Hardware security is complementary to software security. Mitigations at the hardware level, the hypervisor level, and the operation system level complement architectural, process, and tooling decisions made at the software level.
Defense in depth is a good thing. There can always be errors in one layer or another, regardless of software solution, operating system, hypervisor, or hardware. I can wax poetic about current CPU vulnerabilities that must be managed in firmware or operating systems.
Many of the issues caused by C, are solved by Modula-2, Object Pascal and Ada, we didn't need to wait for Rust. But those aren't the languages that come for free with UNIX.
Or even better, they would be solved by C itself, if WG 14 cared even a little about providing proper support for slices, proper arrays and proper string types, or even as library vocabulary types.
But what to expect, when even Dennis Ritchie wasn't able to get his approach to slices being worked on by WG 14.
So hardware memory tagging, and sandboxed enclaves it is.
I make extensive use of bounded model checking in my C development. I also use privilege separation, serialization between separate processes, process isolation, and sandboxing. That's not because bounded model checking has somehow failed, but because humans are fallible. I can formally verify the code I write, but unless I'm running bare metal firmware, I also have to deal with an operating system and libraries that aren't under my direct control. These also have vulnerabilities.
That's not a trivial thing. The average software stack running on a server -- regardless of whether it is written in C, Rust, Modula-2, Pascal, Ada, or constructively proven Lean extracted to C++ -- still goes through tens of millions of lines of system software that is definitely NOT safe. All of that code is out of a developer's control for now. Admins can continually apply patches, but until those projects employ similar technology, they are themselves a risk.
One day, hopefully, all software and firmware will go through bounded model checking as a matter of course. Until then, we work with what we can, and we fix what we can. We can also rely on hardware mitigations where applicable. That's not failure as you have claimed, but practical reality.
I would absolutely love it if you were the majority, alas you are not.
I emulate exhaustive pattern matching in my main language of choice because it does not have it (it's not Rust or OCaml or Haskell) but because I saw how beneficial and useful it is. And sadly, many of the other devs using that language don't do so, and I have made a good buck going after them and fixing their mistakes.
I don't doubt your abilities as a person. I doubt the abilities of the corpus of C/C++ devs at large.
I can say, without ego, that I'm a reasonably good software developer. But, it is the tooling and process that I use that allows me to build safer software and that makes me a reasonably good developer. The same is true of Rust developers.
I can teach these skills to other developers, and in fact, I have plans to do so.
I don't expect things to change overnight, any more than I expect things to be rewritten in Rust overnight. C++ has been around for nearly 40 years, and software is still written in C. But, we can do better, and we must do better.
We both want the same thing: safer software.
I, too, enjoy sci-fi.
> Just because something is not being used universally doesn't mean that it has failed.
You are only correct in the dictionary sense of these words. Fact is that a lot of the programmers are vain creatures prone to ego, and they make their chosen technical stack part of their core identity. This prevents them from being flexible, they get rigid as they age and they become part of the problems they so passionately wanted to fix when they were young.
None of that is made easier by the managerial class that absolutely loves and financially stimulates the programmers who don't want to rock the boat.
So I'd say if the said CBMC, and likely other tools in the same area, has more or less failed if it could not convince a critical mass of C/C++ devs to use it and finally start keeping up with Rust (and the other languages @pjmlp mentioned).
> Moreso, it is not widely known about, and there persists rumors that it requires extraordinary effort, often reinforced by well meaning, but rather outdated advice.
The victims of Heartbleed and many other CVEs don't care. The breaches happened anyway.
I am amazed at your desire to downplay the problem and keep claiming that eventually stuff will work out.
I disagree. And I'll repeat a very core part of my argument: C/C++ devs were handed a monopoly in their areas for decades and they still can't arrive at a set of common techniques that reduce or eliminate memory safety bugs.
I am not impressed. And I am not even a particularly good programmer. Just a diligent guy with average programming ability whose only unique trait is that he refuses to accept the status quo and always looks at how can stuff be improved. But this has taken me a long way.
I was characterizing these hardware changes as being fantasy, so I'm glad you agree.
> So I'd say if the said CBMC, and likely other tools in the same area, has more or less failed if it could not convince a critical mass of C/C++ devs to use it
So, in the same vein, Rust has failed because it has only been around for a similar amount of time and people still use C/C++?
> The victims of Heartbleed and many other CVEs don't care. The breaches happened anyway.
I fail to see how a CVE that occurred due to poor engineering practices has anything to do with the adoption of good engineering practices and tooling. Yes, Heartbleed is why we need this tooling.
You are simultaneously arguing that if we could just adopt Rust, our problems would be solved, but since another technology has not yet been adopted, it has failed. Rust isn't adopted due to programmer ego, but the use of tooling that does the same thing as Rust and more has not yet been adopted because it has failed. Do you not see the logical inconsistency in your position?
Yes, it kind of failed there indeed. And I even hinted at why: Rust is far from perfect and its async implementation is a cobbled together mess. Golang's model reads much better, though I hate their foot-guns quite a lot (like writing to a closed channel leads to a panic; who thought that was a good idea?).
> I fail to see how a CVE that occurred due to poor engineering practices has anything to do with the adoption of good engineering practices and tooling. Yes, Heartbleed is why we need this tooling.
You can't see it? But... the good practices do lead to less of these CVEs as you yourself seem to realize? I don't get this part of your comment.
> You are simultaneously arguing that if we could just adopt Rust, our problems would be solved, but since another technology has not yet been adopted, it has failed.
You have answered it yourself: a lot of people see manual wrangling of `void**` as a badge of honor and their ego takes over (and the fear of being displaced, of course). I claim that Rust is not being more widely adopted due to programmer ego and fear of being obsolete. The fear of the end of nice salaries because they belong to a diminishing cohort of old-school cowboys.
Who would not fear that? Who would want that to end?
> Do you not see the logical inconsistency in your position?
No, and I don't get your argument. The reasons for C/C++ devs not improving the memory safety of their code, and the reasons for them not adopting Rust are very different. Not only is the analogy bad, it is plain inapplicable.
---
But it also does not help that HN reacts like a virgin schoolgirl pinched on the arse when Rust is mentioned. I've coded it for a few years, I loved it, I hated the bad parts and called them out, but even to this day I very quickly and easily get branded as a Rust fanboy even if my comment history shows balanced criticisms towards it. People don't care. People are emotional and are quick to put you in a camp that's easy to hate.
That is the part that I truly hate. No objective debate.
Too expensive to move to Rust? GOOD! That's an amazing argument, we can talk that for weeks and get very interesting insights in both directions.
People unwilling to get re-trained? Also a good argument, with big potential for interesting insights!
But most of everything else is at the level of a heated table debate after the 11th beer. Pretty meh and very uninteresting. No idea why I keep engaging, I think I am just bitter that people who REALLY should know better are reacting on emotion and not on merit. But that's on me. We all have our intolerances to the reality we inhabit. This is one of mine.
People say that, but the people who say this rarely have any practical experience using CBMC. It's very straight-forward to use. I could teach a developer to use it reliably, on practical software, in a month.
What I am saying is that if it were as simple as "just learn CBMC" then maybe Microsoft and Google would have not published their studies demonstrating that 60% - 75% of all CVEs are memory safety errors like buffer under-/over-flows.
There definitely is. Mainstream and official Rust community material is generally sane, but the meme did not come from nowhere. The rewrite-everything people are out there.
Meh, there are zealots in every community -- we're not even talking programming language communities only. Not even programming either. Everywhere.
No idea why people over-reacted so much to one particular 0.1% fanatics. It's a pretty normal state of affairs. Point me at your hobby group and even if it is only 20 people I can bet my balls at least 1 of them is a fanatic.
CVE database proves that those kind of errors keep coming up in 2024, regardless of those changes.
Not only do they keep coming up, the monetary cost of fixing those issues has raised up to a level that now even governments are looking into this.
There are more slaves in the world now than ever before in history, but global society has still made great progress on eliminating it in the last thousand years.
Not that it matters, but isn't that technically ANSI C(89)? If I remember correctly, the first ISO C standard is instead C90, which is basically identical to C89.
I could not find an open-source static analyzer (including -analyzer) that would actually pick up the flaw before someone tries to exploit it.
And that's a simple example.
We can't tame the dragon C is, empirically nobody can.
Practical formal methods using a tool like CBMC can make C safer. The existing code base can be made safer without porting it to a new language or using experimental mechanical translation. This isn't just something for C. Such tools exist for many languages now, including Rust, so that even Rust can be made safer.
WG14 can solve those problems, they decided it isn't their priority to fix C.
That's like saying, "Getting everyone to use Rust or TDD or X is like trying to boil the ocean."
It's impossible to solve all things for all people at once. But, that doesn't mean that we can't advocate for tooling that can be used today to build safer software. This goes beyond C, as such tools and techniques are being ported to many languages and platforms.
Rust is a solution that works for some people. Modern C with bounded model checking is another solution that works for some other people. I'm certainly not going to change the minds of folks who have decided to port a project to Rust and who are willing to spend the engineering budget for this. But, hopefully, I can convince someone to try bounded model checking instead of maintaining the status quo. Because, the status quo is where we are with projects like the Linux kernel. Linux may pay lip service to Rust folks and allow them to write some components in that language, but the majority of the kernel is still in C and is not being properly vetted for these vulnerabilities, as we can see with the stream of CVEs coming out weekly.
> WG14 can solve those problems, they decided it isn't their priority to fix C.
WG14 must maintain some semblance of backwards compatibility with previous versions of C. It's no good to make a feature that breaks older code. This happens from time to time -- old school K&R C won't work in a C18 or C23 compliant compiler -- but efforts are made to keep that legacy code compiling, for good or ill.
I prefer to work toward fixing what is. We are unlikely to see things like array slices in C, and even if such features were added, this does nothing to fix the billions of lines of legacy code out there.
I think a far better and more mature process is to update C to modern C and use a model checker such as CBMC to verify memory, resource, and integer math safety. One gets the same safety as a gradual Rust rewrite, but the code base, knowledge base, and developers can be maintained.