Note that this is done for “existing formally verified C codebases” which is a lot different from typical systems C code which is not formally verified.
replies(8):
It frustrates me more than it should, I admit, that people always mention Rust when they talk about safety, but never Ada / SPARK. You want formal verification? Use Ada / SPARK. It has been battle-tested. It has been used for critical systems for a really long time now.
(And a compiler being formally verified vs. being able to write formally verified code means two different things.)
Formal verification is verifying a mathematical model of the program correct, according to certain mathematical correctness properties. That model may not actually represent the real world, or the correctness properties may not actually be the properties that you want to guarantee. Famously, there was the formally verified Java LinkedList implementation that was buggy due to the formal model not taking into account integer overflow.
There are parts of the Rust language and standard library that have been formally verified. That helps provide confidence that the basic model, of having safety properties upheld by unsafe core functions, to be sound.
But the big advantage of Rust, especially for everyday open source code that the world widely depends on, is that it strikes a good balance between a language that people actually want to use, and which can provide good practical safety guarantees.
Rust is far, far safer than C and C++. Most other memory-safe languages also are, but trade that off for lower performance, while Rust provides a similar level of performance as C and C++. And additionally, it's a language that people actually want to use for writing a lot of the core infrastructure.
As far as I know, I have never use any open source software written in Ada/SPARK. People just don't do it. The only reason they generally do is if they need to for functional safety reasons, in a high-criticality system, and they find it easier to get their software certified by writing it that way.
And even in safety critical systems, most people find using a subset of C, with restrictive rules, static checkers to check those, code review, and extensive testing, done by independent teams and testing on real hardware with requirements based tests that achieve 100% coverage at the MC/DC level is considered to be the gold standard of verification.
Formal verification can not possibly provide some of the safety guarantees that testing on real hardware based on actual system level requirements can provide.
Formal verification is one tool in a toolbox. It is useful for providing certain guarantees. But it's less important than many other factors for the actual improvements in safety that Rust can provide; by actually being used, in critical software that is exposed to potential network based exploitation, a memory-safe language like Rust makes a much better foundation than C or C++, and more people will actually use it in such a context than Ada/SPARK.
Now that Rust is becoming more popular, it would be nice to be able to re-use these formally verified parsers in Rust, where your entire language is memory safe. The formally verified parsers can still be helpful, because the formal verification can ensure that you also won't crash (in safe Rust, you can still crash, you just won't be subject to arbitrary memory corruption).
But just using the C libraries from Rust is unsatisfactory, now you need to go through an unsafe interface which introduces a potential place to introduce new bugs. And there are existing C to Rust translators, but they generate unsafe Rust.
So this demonstrates a way to translate from C to safe Rust, though with constraints on the existing C code. It's both useful in that it means that you can translate some of these already formally verified libraries to safe Rust, and this research could be used as part of later work for a more general tool, that could potentially translate more C code to safe Rust while falling back to unsafe in cases that it can't reason about.
Anyhow, not all academic work like this ends up being used practically in the real world, but some of it can be, or some of it can be put into practice by other tools later on. Rust came about that way; much of its reason for existence is trying to put decades of academic research into a practical, real-world usable language, since there was lots of academic work that had never really been used in industry as much as it should be.