Even without Fil-C I do not think it is even clear that new software should be written in Rust. It seems to have a lot of fans, but IMHO it is overrated. If you need perfect memory safety Rust has an advantage at the moment, but if you are not careful you trade this for much higher supply chain risks. And I believe the advantage in memory safety will disappear in the next years due to improved tooling in C, simply by adding the formal verification that proves the safety which will work automatically.
back
3 comments
Memory safety is absolute table stakes when it comes to formal verification. You can't endow your code with meaningful semantics if you don't have some way of ensuring memory safety.
That's far from trivial in Rust because of 'unsafe' blocks. There are approaches to verifying unsafe code in Rust, but formally verifying a Rust program is still likely to be significantly more complex than formally verifying, say, a Java program.
(And before someone says it: no you don't only have to verify the small amount of code in 'unsafe' blocks. Memory safety errors can be caused by the interaction of safe and unsafe code.)
At least you can grep for unsafe/system/unchecked in several alternative systems languages.
For C and C++, we have to hope the static analysis tool actually found all possible spots.
Despite the way it is going on as a drama between WG21 and community, C++ might eventually get Ada style profiles in C++29, lets see how it plays out.
Then you also would have something to grep for, [[profile:...]]
C? Same business as usual.
Grepping for unsafe blocks doesn’t help that much for formal verification, because you have to verify all of the code.
The easiest way to see this is to note that ‘unsafe’ itself doesn’t have any semantics, so it can’t possibly allow anything to be proved that couldn’t have been proved otherwise.
It helps finding locations for possible flaws outside the type system soundness.
Now if we go discussing formal verification in general, even something like Dafny or Lean may fail, if the proofs aren't correctly written for the deployment scenario.
Just like one may still die while wearing helmets, airbags, and security belts, yet the casualties amount is much worse without them.
It helps a human armed with only a tool as crude as grep. But if Rust didn't have the requirement to mark unsafe operations with the 'unsafe' keyword, that information could trivially be added back automatically. If you're doing correctness proofs of realistic Rust code, you'd better already have tools that are at least capable of looking through your codebase for any instances of raw pointer access, etc.
There's a lot of mythology around Rust unsafe blocks. They're a useful lint, but they don't alter the fundamental safety properties of the language.
The mythology of unsafe blocks goes all the way back to ESPOL on Burroughs, still sold nowadays by Unisys, for customers that want OS security as the number one feature, before anything else.
It was also adopted by several systems and application programming languages outside C geology, until C# came to be, which is probably the first curly brackets language with unsafe code blocks.
The first error naysayers make on the eyes of SecDevOps, thus losing credibility points, is to focus too much on Rust, and too little on history of secure systems.
The first fundamental rule is to reduce attack surface, on C, and C++ (until and if profiles come to be), it is all over the place.
I don't see folks that usually post on HN or Reddit going to buy Astrée licenses, or integrate Frama-C into their development process.
Indeed, and this is why people who care about this are also proving memory safety in C. The issue is that we do not have good open-source tooling that specifically focuses on formal verification of memory safety in C.
The same risks as everyone that uses system installers for their C and C++ binary libraries, without spending one second looking into source code.
The commercial world of C and C++ is pretty much focused on binary libaries, and in many occasions access to source code is extra.
These are not the "same risks" at all.
> simply by adding the formal verification that proves the safety which will work automatically
"simply" and "formal verification" are usually oxymorons, never mind "automatically"
Fair enough, but I have seen how it works and for just temporal memory safety, it could be simple.