Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

thenewstack.io

Post reply on HN
Print view View original

51–60 of 100 posts

Re: Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

#51

Post by Veserv »

Sevii wrote: post #39
Veserv wrote: post #25

Cool. Is this going to require phasing out systems written in C/C++ with horrible security track records like Linux and Windows? Or are they going to get a "too critical to be improved" exemption?

Do you have an OS written in a memory safe language with a good security track record we can switch to? If we start building now we might have a prototype by 2030.

There are plenty with good security track records, formal specifications, formal proofs of various security properties, and decades of deployments.

SCOMP, GEMSOS, INTEGRITY-178, seL4.

Re: Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

#52

Post by anonymousiam »

hgs3 wrote: post #34
synergy20 wrote: post #15

that means you have to use rust for system level programming then? there is really no other alternative at system programming as far as memory safe is concerned, that uses no GC or VM.

You can have a systems programming language with garbage collection. Most concerns regarding GC are around unpredictable pauses, but you can absolutely design a predictable GC suitable for real-time applications. Rust is not the only option. The Ada programming language was developed in the early 1980s, primarily for the U.S. Department of Defense (DoD). Ada was designed for safety-critical embedded systems and real-…

I was going to post that the same sort of mandate had applied to Ada, and was eventually abandoned. I remember Ada the mandate, but I recall obtaining waivers from the mandate (on specific DoD programs) before 1991. I predict that this mandate will suffer the same fate as the previous one.

A quick search confirms my memory:

The DoD Ada language mandate, which required the use of the Ada programming language for most Department of Defense software projects, was established on March 30, 1987 through Department of Defense Directive 3405.2.

https://dl.acm.org/doi/10.1145/255471.255599

Re: Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

#53

Post by aithrowawaycomm »

This seems somewhat incoherent and is too focused on shallow claims about languages instead of trying to understand why the memory bugs happened in the first place.

Are unsafe code blocks in Rust or C# okay? Presumably yes if there are good reasons to do so, sometimes it is necessary. But then as a matter of policy, why is Rust meaningfully different than something like using Valgrind with C++? Of course there are substantive differences from a developer's perspective. But just as a stressed or cynical C++ developer might give up on solving the Valgrind error, a similar Rust developer might give up fighting the borrow checker and add "unsafe" to their buggy code. A federal impetus to switch from C++ to Rust would seem to incentivize this laziness further.

To be clear this isn't a criticism of Rust's design or implementation - demarcated blocks of unsafe code is pragmatic and sensible. The problem is how humans build software. In this sense I don't think we've really settled whether "rewrite the code in Rust" is actually safer than "redo our technical management to include automated memcheck testing and paired code reviews." At the very least, I don't think the latter is insufficient, and the feds are being too heavy-handed by making this about language recommendations.

[If it were up to me I would rewrite it in Rust! Saying "the feds made me" is an excellent excuse :) But I don't like the feds making such strong recommendations/demands when I feel the facts are still quite murky. There simply haven't been enough case studies.]

I also think the feds here (along with techies in general) are undervaluing formal specifications and underestimating the risk of undefined behavior.[1] Rust is very stable but it's not formally specified and until recently had known bugs in its very design, not merely in the rustc implementation. (I think those bugs finally got fixed this year.) Considering how cutting-edge Rust is I am sure there are other "theory bugs" somewhere. The point is that critical software also needs stability, and it is unwise to chase memory safety without considering the risks of being tied to an old version of a compiler, especially with unsafe code.

Again: not saying that Rust is automatically bad because it isn't formally specified. But these issues should at least get lip service.

[1] E.g. this fairly detailed document doesn't discuss this at all: https://www.cisa.gov/sites/default/files/2023-12/The-Case-fo...

Re: Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

#54

Post by erik_seaberg »

nanolith wrote: post #50
erik_seaberg wrote: post #47

Earlier quoted context omitted.

I'm a little familiar with TLA+ but it can't verify the actual code you want to run, only a restatement of your intended algorithm. Are there published model checkers that can check real C++? How would they catch double-free or use-after-free or double-throw?

Yep. ESBMC and PolySpace both work for C++. I use CBMC for C. They run an abstract machine model through an SMT solver. Among other things, this abstract machine model tracks memory usage, UAF, aliasing, etc. With custom assertions, it can also cover issues like casting safety, serialization issues, logic errors, etc. More or less, you can build up any proof obligations you need and run them through the model checker…

I'm definitely digging into this, thank you!

I'm a little concerned about ESBMC's "simulating a finite prefix of the program execution with all possible inputs" when important software like operating systems are intended to run indefinitely. Would they start with a valid state (filesystem, process list) and prove no invalid state is reachable within n syscalls or interrupts? Maybe I was hoping for proving invariants.

Re: Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

#55

Post by erik_seaberg »

aithrowawaycomm wrote: post #53

This seems somewhat incoherent and is too focused on shallow claims about languages instead of trying to understand why the memory bugs happened in the first place. Are unsafe code blocks in Rust or C# okay? Presumably yes if there are good reasons to do so, sometimes it is necessary. But then as a matter of policy, why is Rust meaningfully different than something like using Valgrind with C++? Of course there are su…

Rust's borrow checker proves some invariants that the code always upholds. Valgrind only checks that this run hasn't triggered some undefined behavior so far, it's always possible that (ab)using it further or another run with different input might.

Re: Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

#56

Post by jeethate88 »

gigel82 wrote: post #4

C++ is only "memory-unsafe" if you are hiring bottom of the barrel talent. Likely the same kind of folks for which we had to change car manuals from including schematics and repair instructions to including warnings about not drinking the coolant...

[flagged]

Re: Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

#57

Post by aithrowawaycomm »

erik_seaberg wrote: post #55
aithrowawaycomm wrote: post #53

This seems somewhat incoherent and is too focused on shallow claims about languages instead of trying to understand why the memory bugs happened in the first place. Are unsafe code blocks in Rust or C# okay? Presumably yes if there are good reasons to do so, sometimes it is necessary. But then as a matter of policy, why is Rust meaningfully different than something like using Valgrind with C++? Of course there are su…

Rust's borrow checker proves some invariants that the code always upholds. Valgrind only checks that this run hasn't triggered some undefined behavior so far, it's always possible that (ab)using it further or another run with different input might.

> But then as a matter of policy, why is Rust meaningfully different than something like using Valgrind with C++? Of course there are substantive differences from a developer's perspective.

I did not say they were the same or even equivalent, though I was sloppy with synecdoche and didn't specifically mean Valgrind. My point is that unsafe Rust without Valgrind is more dangerous than C++ with Valgrind, and the feds are not adequately considering this when thinking about how large organizations might rewrite their C++ applications.

"We will rewrite it in 100% safe Rust" is guaranteed way to eliminate virtually all C++ memory errors. It does not follow that "we will rewrite it in 95% safe Rust, except for the tricky bits" will eliminate 95% of C++ memory errors.

Re: Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

#59

Post by ArtixFox »

Veserv wrote: post #51
Sevii wrote: post #39

Earlier quoted context omitted.

Do you have an OS written in a memory safe language with a good security track record we can switch to? If we start building now we might have a prototype by 2030.

There are plenty with good security track records, formal specifications, formal proofs of various security properties, and decades of deployments. SCOMP, GEMSOS, INTEGRITY-178, seL4.

god seL4 everywhere would be awesome.

Re: Feds: Critical Software Must Drop C/C++ by 2026 or Face Risk

#60

Post by nanolith »

erik_seaberg wrote: post #54
nanolith wrote: post #50

Earlier quoted context omitted.

Yep. ESBMC and PolySpace both work for C++. I use CBMC for C. They run an abstract machine model through an SMT solver. Among other things, this abstract machine model tracks memory usage, UAF, aliasing, etc. With custom assertions, it can also cover issues like casting safety, serialization issues, logic errors, etc. More or less, you can build up any proof obligations you need and run them through the model checker…

I'm definitely digging into this, thank you! I'm a little concerned about ESBMC's "simulating a finite prefix of the program execution with all possible inputs" when important software like operating systems are intended to run indefinitely. Would they start with a valid state (filesystem, process list) and prove no invalid state is reachable within n syscalls or interrupts? Maybe I was hoping for proving invariants.

So, the way I deal with this is to provide an exit condition in the loop that is triggered in a non-deterministic finite way by the model checker but that is not triggered at runtime. This allows for termination, which is required as part of the model check, while maintaining the loop.

The best way that I've found to model check software is to decompose the software by function, defining function contracts and invariants along the way. To reduce complexity, shadow functions that follow the same function contracts and maintain the same invariants can be substituted. A shadow function uses non-determinism to exercise the same range of behaviors that the real function provides in a way that is simpler for the model checker to verify. When verifying a function with the model checker, you can substitute functions it calls with these shadow functions to reduce the complexity of the model check.

The example server I'm using for the book initiates a TLS connection with the client. Each connection is maintained by a fiber that enters into a command-response loop. When verifying this loop function in the model checker, I can shadow the functions that read the command and send the response. As long as these shadows follow the same function contract as the function, I can verify that the loop function is correct. For instance, the read command function returns a command in the output variable on success that must be freed by the caller. The dispatch function that dispatches the command and sends the response expects this command to be valid and treats it as read-only data with a lifetime that is beyond the lifetime of the dispatch function. Finally, the loop cleans up the command. All of this can be specified using the function contracts defined by this function as well as the semantics of the real functions and the shadow functions. We know based on the contracts that we expect this command object to be created on success, and we know based on the abstract model that it must be cleaned up. If, for instance, we freed it before calling dispatch, the abstract model would find a UAF counter-example.

If this sounds like a lot, there is a reason why I'm writing a book on the topic of practical model checking in C, with a mature well-worked example that mirrors a real-world application.

Post reply on HN