Prossimo – Memory safety for the Internet's most critical infrastructure(memorysafety.org)
memorysafety.org
Prossimo – Memory safety for the Internet's most critical infrastructure
https://www.memorysafety.org/
119 comments
oscargrouch(1)
I love that Rust has become a successful systems language with memory safety. And while I use many of these "coreutils replacements" frequently, they are mostly not equivalent to the originals, and I think it's disingenuous to claim that they are.
They aren't drop-in replacements, but I think "equivalents" is fair.
Your existing bash scripts don't work in an alternate universe where computers come with ripgrep not grep, but that universe isn't very different otherwise. Some things are a little easier to do, some things are a little harder to do, there are different bugs than in our universe, but it's way less strange than a universe where Lisp Machines still dominate, or even one where the Network uses X.25 rather than IP.
Your existing bash scripts don't work in an alternate universe where computers come with ripgrep not grep, but that universe isn't very different otherwise. Some things are a little easier to do, some things are a little harder to do, there are different bugs than in our universe, but it's way less strange than a universe where Lisp Machines still dominate, or even one where the Network uses X.25 rather than IP.
I think https://github.com/uutils/coreutils is aiming to provide drop-in replacements.
Good luck getting Google to fund that one particular go, heh. Even if they do fund Mozilla.
Eh, memory safety hasn't ever really been the problem with mod_tls, or curl, but it would be nice to have some solid examples for other projects to build on.
The Linux kernel project sounds interesting. It would be nice if there was an effort to purge as much C code as possible from the core of the kernel and really enforce standards such that even a maliciously designed kernel module should not be vulnerable to memory corruption bugs.
The Linux kernel project sounds interesting. It would be nice if there was an effort to purge as much C code as possible from the core of the kernel and really enforce standards such that even a maliciously designed kernel module should not be vulnerable to memory corruption bugs.
Here[1] is the ongoing list of "curl security problems." Note the several memory safety related issues. The two most recent are:
[1] https://curl.se/docs/security.html
May 26, 2021 CWE-416: Use After Free
May 26, 2021 CWE-457: Use of Uninitialized Variable
[1] https://curl.se/docs/security.html
Memory safety hasn't been a problem with mod_tls because mod_tls is the module written in Rust.
But likely you were thinking of mod_ssl. Except, mod_ssl is how Apache ends up using OpenSSL, where the famous Heartbleed bug is literally exactly the sort of memory unsafety that you'd never do in Rust.
But likely you were thinking of mod_ssl. Except, mod_ssl is how Apache ends up using OpenSSL, where the famous Heartbleed bug is literally exactly the sort of memory unsafety that you'd never do in Rust.
The author of curl wrote https://daniel.haxx.se/blog/2021/03/09/half-of-curls-vulnera... which fundamentally disagrees with your assertion about it.
[deleted]
Why not have all this Rust energy focused on a new kernel (not a toy/experiment), a kernel architect ed not evolved.
You would get better results and if you need Linux compatibility add support for it from the start in soem kind of emulation/compatibility layer.
Putting Rust into kernel seems to me that is a lot of effor for microscopic gains.
Putting Rust into kernel seems to me that is a lot of effor for microscopic gains.
Because ISRG is trying to direct funds to projects that will actually protect current Internet users; notably, this isn't a research project, but rather a funded engineering project, focusing on things that are already in wide use.
Redox OS
https://www.redox-os.org/
A new kernel has a massive uphill battle to fight to get to where Linux is today. Like, an absolutely huge battle to fight.
Although it would be great to eventually see it.
Although it would be great to eventually see it.
I know, but Linux will not be forever, someone will start a new kernel that will replace it. All this giant tech companies could afford to pay some experienced people to start working on it. The initial scope would be limited but if the architecture and the language combo would give it a performance and security boost then for sure it will be adopted and new contributors would appear. If the performance/security would be similar to Linux/BSD then for sure the progress would be very slow.
> Linux will not be forever
Linux is thirty years old. And Linux isn't something from whole cloth, it's a Unix, it didn't have some legal and technical baggage that UNIX® brand Unix had but it's a Unix. And Unix is over sixty years old.
We may very well be done. Unix isn't the best conceivable Operating System, but it seems like it's good enough, and in being good enough it became so enormously popular that any new alternative has to be night-and-day better or why bother?
I'm reminded of the Two's Complement Integer thing. Historically it was unclear if this was the "best" way for integers to work. Hardware existed, and sold well decades ago, with some other ideas for how integers could be represented and calculated. But, gradually, over time, even if Two's Complement wasn't clearly the best, it was clearly the most popular, and the others weren't clearly better so why fight it? Sure enough, "Two's Complement Integers" get to just be how integers work by default in newer languages.
If Linus and all the subsystems people were screaming "Nothing but C, under any circumstances" then perhaps you could imagine a competitor to Linux comes along in ten, twenty, thirty years. But so long as they remain open to changes that actually have good results, they're going to stay on top.
Linux is thirty years old. And Linux isn't something from whole cloth, it's a Unix, it didn't have some legal and technical baggage that UNIX® brand Unix had but it's a Unix. And Unix is over sixty years old.
We may very well be done. Unix isn't the best conceivable Operating System, but it seems like it's good enough, and in being good enough it became so enormously popular that any new alternative has to be night-and-day better or why bother?
I'm reminded of the Two's Complement Integer thing. Historically it was unclear if this was the "best" way for integers to work. Hardware existed, and sold well decades ago, with some other ideas for how integers could be represented and calculated. But, gradually, over time, even if Two's Complement wasn't clearly the best, it was clearly the most popular, and the others weren't clearly better so why fight it? Sure enough, "Two's Complement Integers" get to just be how integers work by default in newer languages.
If Linus and all the subsystems people were screaming "Nothing but C, under any circumstances" then perhaps you could imagine a competitor to Linux comes along in ten, twenty, thirty years. But so long as they remain open to changes that actually have good results, they're going to stay on top.
Rust has been prominent in Fuscia's userland (which is bigger proportionally because it's a microkernel), but not the kernel (Zircon) itself.
Considering Google's funding of these ISRG projects, I hope this changes.
Considering Google's funding of these ISRG projects, I hope this changes.
Li et al., "An Incremental Path Towards a Safer OS Kernel," HotOS 2021 (two weeks ago), is an academic paper arguing that putting Rust into an existing kernel will deliver you much more than microscopic gains and will yield better results than starting from scratch. https://sigops.org/s/conferences/hotos/2021/papers/hotos21-s...
I think they are complementary goals.
On aspect of the Rust-on-Linux worked I've helped out with is trying to make sure standard library abstractions aren't just suitable for userspace. I hope the medium term result of this is more comparability between bare metal projects on axes where they aren't trying to differentiate.
Longer term, I hope that means a corpus of driver that can be shared between kernels, revolutionizing kernel diversity the same way LLVM revolutionized programming language diversity.
On aspect of the Rust-on-Linux worked I've helped out with is trying to make sure standard library abstractions aren't just suitable for userspace. I hope the medium term result of this is more comparability between bare metal projects on axes where they aren't trying to differentiate.
Longer term, I hope that means a corpus of driver that can be shared between kernels, revolutionizing kernel diversity the same way LLVM revolutionized programming language diversity.
[deleted]
It looks to me an another attempt to force feed people Rust at any cost irrespective of the rationale.
All I keep seeing, is how rust is perfect for everything, will fix everything, should be everywhere, etc, etc. There's gotta be a profit motive involved. There must.
There is absolutely a profit motive involved! The less time you spend dealing with segfaults and inexplicable double-frees because you have no idea where the first free is, the more time you can spend working on features that impact the business's bottom line. The fewer emergency patches you have to deploy, the more uptime you have and the less you spend on the required ops work. The fewer zero-days you suffer, the fewer existential threats to your business. And so forth.
None of this would be happening if the market didn't care. I was one of the people who started the Linux kernel modules in Rust project (I'm credited in the announcement), but I started it because I thought it would be fun, and I have a day job that isn't related to Rust at all. So I've spent almost no time on it recently.
The corporate sponsors behind this effort are interested in this because they use Linux (and curl and so forth) at a large enough scale where this sort of thing matters. I would guess that, for instance, Google cares about getting Rust into Android's kernel because they want to credibly claim that Android has fewer zero-days than iOS, and they have a clear public agenda of wanting to get rid of zero-days (see e.g. https://googleprojectzero.blogspot.com/p/0day.html).
So that's their profit motive, and I'm very happy it exists, because this work is too important to rely on the free time of people like me.
(To be abundantly clear: I am not paid by any of the involved organizations, and I had no advance knowledge of this before the public announcement.)
None of this would be happening if the market didn't care. I was one of the people who started the Linux kernel modules in Rust project (I'm credited in the announcement), but I started it because I thought it would be fun, and I have a day job that isn't related to Rust at all. So I've spent almost no time on it recently.
The corporate sponsors behind this effort are interested in this because they use Linux (and curl and so forth) at a large enough scale where this sort of thing matters. I would guess that, for instance, Google cares about getting Rust into Android's kernel because they want to credibly claim that Android has fewer zero-days than iOS, and they have a clear public agenda of wanting to get rid of zero-days (see e.g. https://googleprojectzero.blogspot.com/p/0day.html).
So that's their profit motive, and I'm very happy it exists, because this work is too important to rely on the free time of people like me.
(To be abundantly clear: I am not paid by any of the involved organizations, and I had no advance knowledge of this before the public announcement.)
> Google cares about getting Rust into Android's kernel because they want to credibly claim that Android has fewer zero-days than iOS, and they have a clear public agenda of wanting to get rid of zero-days
It is going to be very hard to achieve this when iOS is moving into the direction to have 100% of userspace API available to Swift, while Android team forces us to use C and C++ for anything related with real time audio, machine learning and 3D API.
Now in Android 12 even Renderscript was replaced with C and C++ alongside Vulkan compute shaders.
The kernel can even be 100% Rust, it won't help those of us that are cloning Oboe or Vulkan github repo, dealing with JNI boilerplate, C and C++ toolchain issues on NDK.
It is going to be very hard to achieve this when iOS is moving into the direction to have 100% of userspace API available to Swift, while Android team forces us to use C and C++ for anything related with real time audio, machine learning and 3D API.
Now in Android 12 even Renderscript was replaced with C and C++ alongside Vulkan compute shaders.
The kernel can even be 100% Rust, it won't help those of us that are cloning Oboe or Vulkan github repo, dealing with JNI boilerplate, C and C++ toolchain issues on NDK.
Well, Google probably doesn’t control all the C++ standards committees. I don’t know how much control they have over commit rights to the Rust compiler. Given Mozilla’s client-patron relationship with Google, then I’d guess it’s possible.
But, yeah, a company whose business model is tricking old people into buying junk and surveilling their users probably shouldn’t be implicitly trusted.
But, yeah, a company whose business model is tricking old people into buying junk and surveilling their users probably shouldn’t be implicitly trusted.
Google, nor Mozilla, controls who has commit rights to the Rust compiler.
They just employ the people who do? And, until recently, the paid language evangelists?
Google employs a few people who have a commit bit, but they are handed out via consensus among the whole team, not by a single company or its employees.
Right, and at one point the whole team were all or mostly Mozilla employees (which, financially, is a client company of Google). So the core team is a group of Mozilla alumni and their friends. Unlike, say, C++ which is under diverse committees across multiple countries.
On the "critical infrastructure" front, I'd like to see a few "hard nuts" built. Not many. Just a few special purpose boxes, to start:
- A BGP server.
- A DNS/DNSSEC server.
- A WiFi/home network gateway.
Those are critical infrastructure. They're self-contained units which talk well-defined protocols. Their functions don't change much. The first two aren't that price-sensitive. They should be verified down to the bare metal.
Apply to DARPA or NIST or DHS for funding for such a project. You might get it.
- A BGP server.
- A DNS/DNSSEC server.
- A WiFi/home network gateway.
Those are critical infrastructure. They're self-contained units which talk well-defined protocols. Their functions don't change much. The first two aren't that price-sensitive. They should be verified down to the bare metal.
Apply to DARPA or NIST or DHS for funding for such a project. You might get it.
Good ideas!
We are already working on plans for DNS. BGP has been in the back of our minds for a while but we haven’t had the bandwidth to start seriously looking into that yet. If you have ideas get in touch!
We are already working on plans for DNS. BGP has been in the back of our minds for a while but we haven’t had the bandwidth to start seriously looking into that yet. If you have ideas get in touch!
I get why BGP sounds like a good target, since it's self-contained and high-importance, but I'd assume the most important BGP4 deployments on the Internet aren't in systems that can replace their BGP4 servers with anything that Cisco isn't itself shipping. Lots of people run little `birds` to advise their upstreams, but they're not running full-feed defaultless; they're minimally exposed. I think the win from a community-driven BGP4 project might be small compared to the investment. But you've been thinking about this already, so I'd love to hear about how wrong I am. :)
What you are describing matches my impression of things. It has been on the back burner because even if we had a great memory safe version of, say, openbgpd, I am not sure that would have particularly widespread impact. You are probably right that we would need to convince Cisco and friends to move to memory safe code.
we would need to convince Cisco and friends to move to memory safe code.
For BGP and DNS, probably. But a few big buyers pushing on that might get it.
An all-Rust home router with WiFi, cable, fiber. and DSL would be useful. The trouble is, if it's written by open source people, it will have zillions of versions and be configured by editing a text file.
For BGP and DNS, probably. But a few big buyers pushing on that might get it.
An all-Rust home router with WiFi, cable, fiber. and DSL would be useful. The trouble is, if it's written by open source people, it will have zillions of versions and be configured by editing a text file.
A bigger problem would probably be that consumer routers are built as quickly and as cheaply as possible. Every megabyte of additional storage costs cents on the dollar extra and even that gets shaved off if possible. All the router security research I've seen done by well-intending academics got turned away by manufacturers because they don't want to ship additional software in their already-constrained images.
Rust, on the other hand, has all the downsides of static compilation combined with the library bloat we see in nodejs.
For a home router to run Rust, you'd probably need to compile the entire router into a single firmware image doing everything or you'd need to build an extensive dynamic linking system on top of the existing Rust infrastructure. Or, alternatively, convince the router manufacturers to spend another dollar or two on their EEPROM, but good luck getting them to do that.
Finally, the core parts of the system (the drivers running the DSL/cable/fiber/wifi hardware) are all closed source blobs that the manufacturers (be it Broadcom, Intel, Cisco, or Qualcom) need you to load and execute, usually written in a language like C with none of the benefits of Rust. Unless you want to rewrite the drivers in Rust (and good luck to you reverse engineering all of those and fighting the cease and desist letters you receive), the core parts of the system are still vulnerable as all hell.
The configuration can be made reasonably simple; OpenWRT has a GUI that can easily be dumbed down enough so normal folk can use it. Even in consumer routers, a lot of configuration is still dumped to text files already, anyway.
Rust, on the other hand, has all the downsides of static compilation combined with the library bloat we see in nodejs.
For a home router to run Rust, you'd probably need to compile the entire router into a single firmware image doing everything or you'd need to build an extensive dynamic linking system on top of the existing Rust infrastructure. Or, alternatively, convince the router manufacturers to spend another dollar or two on their EEPROM, but good luck getting them to do that.
Finally, the core parts of the system (the drivers running the DSL/cable/fiber/wifi hardware) are all closed source blobs that the manufacturers (be it Broadcom, Intel, Cisco, or Qualcom) need you to load and execute, usually written in a language like C with none of the benefits of Rust. Unless you want to rewrite the drivers in Rust (and good luck to you reverse engineering all of those and fighting the cease and desist letters you receive), the core parts of the system are still vulnerable as all hell.
The configuration can be made reasonably simple; OpenWRT has a GUI that can easily be dumbed down enough so normal folk can use it. Even in consumer routers, a lot of configuration is still dumped to text files already, anyway.
Rust can work with dynamically linked code. It's just limited to the C ABI in most cases because Rust itself doesn't have an ABI that's stable across compiler versions.
A Rust or Go DNS server that served as a drop-in replacement for BIND or nsd, on the other hand, is a big win. :)
Many Chinese companies are building their own authoritative NS based on code from miekg/dns :)
Writing one importing that library is really simple, we should do it more often in the West too.
Right, I just ported our Rust DNS server (built with the equally excellent NLNet crate) to miekg/dns. It's great. But people tend to be writing "interesting" DNS servers, which is not the thing you actually need if you're trying to get rid of BIND and nsd; you need stuff that behaves exactly like BIND and nsd, just minus the memory corruption.
They have been adopting Python actually.
https://developer.cisco.com/docs/nx-os/#!languages-and-envir...
https://developer.cisco.com/docs/nx-os/#!languages-and-envir...
Big Internet BGP servers also aren't super exposed due to the common use of TCP MD5 (RFC 2385) or TCP AO (RFC 5925). The userspace daemon won't even see packets from attackers who don't have the shared secret for that peer link.
I also would like to see Azure Sphere adopt Rust.
It cannot be that they do all the marketing sales speech about about Azure Sphere is the future of security in IoT devices, and then offer a C only SDK as option.
They even went to the effort to try to turn this into a positive thing, when the obvious questions started raining on them, given the marketing sales pitch.
https://techcommunity.microsoft.com/t5/internet-of-things/de...
It cannot be that they do all the marketing sales speech about about Azure Sphere is the future of security in IoT devices, and then offer a C only SDK as option.
They even went to the effort to try to turn this into a positive thing, when the obvious questions started raining on them, given the marketing sales pitch.
https://techcommunity.microsoft.com/t5/internet-of-things/de...
For the home router? What becomes Rust? The DNS/NTP/DHCP stuff? That is some mature code, is it really a problem? Or those web-interfaces to set your WiFi passwords? Wouldn't you still use iptables/ipset for blocking/routing? Or do you rewrite kernel modules too?
you are aware of ironside? a dns server written in ADA, and at least parts verified in spark?
https://ironsides.martincarlisle.com/
https://ironsides.martincarlisle.com/
- BGP is beautiful yucky. It's a great solution to a problem that shouldn't exist.
- DNS/DNSSEC server is a centralized distributed contradiction
- WiFi/home network gateway is _where_ we fix these problems
- DNS/DNSSEC server is a centralized distributed contradiction
- WiFi/home network gateway is _where_ we fix these problems
GoBGP and RustyBGP are happening.
Very tangential, but the very slight angle on the “Memory Safety” highlight threw me for a loop. For a moment I wasn’t sure if it was actually slanted or not until I zoomed way in to confirm the slant.
That’s distracting as heck and I can’t think of a good reason to have such a weird highlight…
That’s distracting as heck and I can’t think of a good reason to have such a weird highlight…
JFWIW: the guidelines ask us not to write comments like this (CMD-F for "too common to be interesting").
https://news.ycombinator.com/newsguidelines.html
https://news.ycombinator.com/newsguidelines.html
Why the push to have RustTLS replace OpenSSL, instead of Go's TLS library (which is mature and widely used?)
This doesn't deserve the downmods; when one assumes good faith all we have here is a straightforward question.
Here is the answer; When you wish to provide a library that you intend for use in diverse applications[1] -- and OpenSSL is a excellent example of exactly this case -- you cannot choose a language with a complex runtime. Go has a complex runtime. There is no getting around this; any non-trivial software implemented in Go will require a number of runtime facilities and accommodating that becomes a burden for the library user.
Rust has about the same runtime burden as C/C++. It links the same way as C/C++ and imposes the minimum possible burden on the library user.
[1] diverse as in essentially all platforms, from microcontrollers to high performance systems at scale, over decades of evolution.
Here is the answer; When you wish to provide a library that you intend for use in diverse applications[1] -- and OpenSSL is a excellent example of exactly this case -- you cannot choose a language with a complex runtime. Go has a complex runtime. There is no getting around this; any non-trivial software implemented in Go will require a number of runtime facilities and accommodating that becomes a burden for the library user.
Rust has about the same runtime burden as C/C++. It links the same way as C/C++ and imposes the minimum possible burden on the library user.
[1] diverse as in essentially all platforms, from microcontrollers to high performance systems at scale, over decades of evolution.
Go's TLS is the right choice if you're working on a project that uses Go. Go is often a good choice if you're rewriting a whole project to be memory-safe. But if you're retaining a lot of your C/C++ code, and trying to surgically replace the attack-surfacey bits with memory-safe code, that's Rust's job, not Go's.
C -> Go FFI is a lot harder. Per their website, they are a big on a modular approach where libraries can be made memory safe concurrently.
Languages with non-trivial runtimes like Go or Haskell just don't support that same model. You would want to convert your libraries in a certain order so there is one continuous C vs non-C boundary.
Languages with non-trivial runtimes like Go or Haskell just don't support that same model. You would want to convert your libraries in a certain order so there is one continuous C vs non-C boundary.
I would guess because Go, having a garbage collector and green threads, has a heavier runtime than Rust and is therefore harder to embed into programs written primarily in other languages. Can anyone else speak more authoritatively on this?
Because these people are Rust partisans, who are hiding behind generalized language and confusing "About" pages to push their partisanship under the guise of benevolence, since shaming everyone who disagreed with them backfired.
They have more information on their website about how to give them money than they do about who they actually are. This makes it easier to route cash to rewrite-it-in-Rust efforts without having to defend these decisions.
They have more information on their website about how to give them money than they do about who they actually are. This makes it easier to route cash to rewrite-it-in-Rust efforts without having to defend these decisions.
I don’t understand this at all. MISRA C, model checkers and theorem provers all exist to provide some of these guarantees that are, to my knowledge, widely recognized in applications where “safety” actually entails life safety. F* is a very modern tool, I think, developed for precisely these use cases. I’m not aware that the rust compiler is proven or even specified. Avoiding its mechanisms for validating use-once memory isn’t even that uncommon, especially in low-level library code.
That Google is the man behind the curtain here also comes off as weird since they have not, to my knowledge, standardized their own critical infrastructure on Rust.
That Google is the man behind the curtain here also comes off as weird since they have not, to my knowledge, standardized their own critical infrastructure on Rust.
> MISRA C, model checkers and theorem provers all exist to provide some of these guarantees that are, to my knowledge, widely recognized in applications where “safety” actually entails life safety.
So, where do I get the version of curl or similar that in fact provides "some of these guarantees" ? Because ISRG isn't spending money on developing software for the Ford Bronco or US aircraft carriers, it is spending money on curl.
MISRA C like a long list of other projects for C or C++ including Bjarne's "Core Guidelines", goes like this:
1. Classify things people will end up needing to do as sinful.
2. Offer them a mechanism to obtain an indulgence, knowing this mechanism will quickly be exhausted.
3. When inevitably this results in tragedy point back at item (1) which absolves you of responsibility.
Example #1, MISRA says you mustn't have any unreachable code. Of course deciding whether code is actually reachable requires solving the Halting Problem, so your automated tooling doesn't do that and will either just flag code that might or might not really be unreachable (useless noise that reduces development velocity) or ignore MIRSA here and just leave your programmers to try not to do this, the status quo ante.
MISRA often needs to dish out "permits" to violate their guidelines because, in practice, the guidelines are too strict to be usable and somebody's workplace requires the guidelines so... the alternative is incredibly creaky and likely unsafe code that's "compliant" - or a "permit" to just ignore a guideline. This is most common when the language doesn't provide a sane way to do something.
Example #2, MISRA forbids hiding variables. If the inner scope has a variable named 'counter' and so does the outer scope, programmers are likely to get confused and mean one when the other is actually in scope, the language compiler won't stop this. But MISRA has to issue a permit because C macros routinely do this and so if your static analysis tool looks at the code it sees lots of such re-use that was (hopefully) harmless.
But if you have hygienic macros (Rust declarative macros) then this isn't a problem, the hygienic macro can't accidentally shadow variables. So you don't need these acrobatics in Rust, if you want to ban shadowing, you can do that and not have weird knock-on effects in macros.
Example #3 MISRA forbids invariants from appearing as conditionals. MISRA reasons that you couldn't possibly have meant to check that buffer != NULL because you know you set buffer in the constructor, and so this is a coding error. But of course you wrote that because you're worried that a bug elsewhere might null out the buffer and blow up the whole system... So now your static analysis tool is screaming that your defensive coding violate MISRA. Do you go ask the Boss for authority to ignore this rule? Or do you rip out the defensive checks?
Tools like F* and WUFFS are different because they've intentionally set their sights low. If you say you want to write the software for your Jet Fighter in WUFFS its authors will carefully explain that this can't be done, and they don't want to help you try. They solve small, well-specified problems in a constrained problem space. They do it very well, you should use them when they're appropriate. They can't be used to replace curl.
So, where do I get the version of curl or similar that in fact provides "some of these guarantees" ? Because ISRG isn't spending money on developing software for the Ford Bronco or US aircraft carriers, it is spending money on curl.
MISRA C like a long list of other projects for C or C++ including Bjarne's "Core Guidelines", goes like this:
1. Classify things people will end up needing to do as sinful.
2. Offer them a mechanism to obtain an indulgence, knowing this mechanism will quickly be exhausted.
3. When inevitably this results in tragedy point back at item (1) which absolves you of responsibility.
Example #1, MISRA says you mustn't have any unreachable code. Of course deciding whether code is actually reachable requires solving the Halting Problem, so your automated tooling doesn't do that and will either just flag code that might or might not really be unreachable (useless noise that reduces development velocity) or ignore MIRSA here and just leave your programmers to try not to do this, the status quo ante.
MISRA often needs to dish out "permits" to violate their guidelines because, in practice, the guidelines are too strict to be usable and somebody's workplace requires the guidelines so... the alternative is incredibly creaky and likely unsafe code that's "compliant" - or a "permit" to just ignore a guideline. This is most common when the language doesn't provide a sane way to do something.
Example #2, MISRA forbids hiding variables. If the inner scope has a variable named 'counter' and so does the outer scope, programmers are likely to get confused and mean one when the other is actually in scope, the language compiler won't stop this. But MISRA has to issue a permit because C macros routinely do this and so if your static analysis tool looks at the code it sees lots of such re-use that was (hopefully) harmless.
But if you have hygienic macros (Rust declarative macros) then this isn't a problem, the hygienic macro can't accidentally shadow variables. So you don't need these acrobatics in Rust, if you want to ban shadowing, you can do that and not have weird knock-on effects in macros.
Example #3 MISRA forbids invariants from appearing as conditionals. MISRA reasons that you couldn't possibly have meant to check that buffer != NULL because you know you set buffer in the constructor, and so this is a coding error. But of course you wrote that because you're worried that a bug elsewhere might null out the buffer and blow up the whole system... So now your static analysis tool is screaming that your defensive coding violate MISRA. Do you go ask the Boss for authority to ignore this rule? Or do you rip out the defensive checks?
Tools like F* and WUFFS are different because they've intentionally set their sights low. If you say you want to write the software for your Jet Fighter in WUFFS its authors will carefully explain that this can't be done, and they don't want to help you try. They solve small, well-specified problems in a constrained problem space. They do it very well, you should use them when they're appropriate. They can't be used to replace curl.
MISRA C is just a standard and developing a codebase in it can still result in memory safety issues. Rust has the guarantees built into the compiler, so if it compiles you have a reasonable standard of memory safety.
You would have to sanitize your entire dependency tree for unsafe invocations and also demonstrate that valid rust programs do, in fact, guarantee memory safety, which might be invalidated by previous or future compiler versions. That also ignores known soundness holes, compiler errors, and silliness like how rust binaries leak the file structure they were built on. I don’t see why that’s reasonable, but auto industry standards are not reasonable or a language with a garbage collector is not reasonable. The work happening in model checking is really incredible. Project Everest is focused on addressing exactly the same problems, and I don’t think the rust compilers guarantees have undergone nearly the rigor of that of F*.
Firstly, for any of the 4 projects that have been announced by Prossimo so far, a garbage collected language would be unsuitable as it would be rejected by almost all current users of the respective projects.
Given that, as you correctly point out there are still lots of options that could be used; for example, Ada/SPARK has been around and freely available via GNAT for a long time.
For example, here is a DNS server implemented in Ada/SPARK: http://ironsides.martincarlisle.com/
Latest download is 5 years old - can you find a single instance of IRONSIDES running in the wild?
IMHO the main advantage that Rust has over other approaches that would technically work to create sufficiently secure software is that it has much lower barriers to entry and a much larger community - the hardest part of getting a technology adopted is marketing, and Rust is currently the only option that can compete with C/C++ here.
There is already some promising work on formalizing the semantics of Rust, see for example https://plv.mpi-sws.org/rustbelt/popl18/ and https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf
Given that, as you correctly point out there are still lots of options that could be used; for example, Ada/SPARK has been around and freely available via GNAT for a long time.
For example, here is a DNS server implemented in Ada/SPARK: http://ironsides.martincarlisle.com/
Latest download is 5 years old - can you find a single instance of IRONSIDES running in the wild?
IMHO the main advantage that Rust has over other approaches that would technically work to create sufficiently secure software is that it has much lower barriers to entry and a much larger community - the hardest part of getting a technology adopted is marketing, and Rust is currently the only option that can compete with C/C++ here.
There is already some promising work on formalizing the semantics of Rust, see for example https://plv.mpi-sws.org/rustbelt/popl18/ and https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf
> That also ignores known soundness holes, compiler errors, and silliness like how rust binaries leak the file structure they were built on
All these issues I've encountered, or heard of, while working on MISRA-compliant code which is expected to run in cars for years without updates. We make do with C, and extensive tests + ASAN/UBSAN/TSAN can take us a long way, but my point is that Rust is a nice incremental step compared to C. I'm not excluding F* from the list of nice incremental steps, and if the developer ecosystem is there maybe that is a compelling option.
My other point is that MISRA C helps enforce standards in some of the nasty codebases that run in cars, and trust me they can be scary, but it is only a band-aid and I believe that Rust is generations ahead of it.
> but auto industry standards are not reasonable or a language with a garbage collector is not reasonable.
We avoided garbage collection because the run-time is harder to predict, and at the same time Java/Android is used a lot in the infotainment units which are now also running some safety-critical code - with a back-up computer thank you standards - and it makes it harder to allocate resources on the embedded system accordingly.
I will admit I'm all for Rust and will likely try to seek out jobs which I get to use it in.
All these issues I've encountered, or heard of, while working on MISRA-compliant code which is expected to run in cars for years without updates. We make do with C, and extensive tests + ASAN/UBSAN/TSAN can take us a long way, but my point is that Rust is a nice incremental step compared to C. I'm not excluding F* from the list of nice incremental steps, and if the developer ecosystem is there maybe that is a compelling option.
My other point is that MISRA C helps enforce standards in some of the nasty codebases that run in cars, and trust me they can be scary, but it is only a band-aid and I believe that Rust is generations ahead of it.
> but auto industry standards are not reasonable or a language with a garbage collector is not reasonable.
We avoided garbage collection because the run-time is harder to predict, and at the same time Java/Android is used a lot in the infotainment units which are now also running some safety-critical code - with a back-up computer thank you standards - and it makes it harder to allocate resources on the embedded system accordingly.
I will admit I'm all for Rust and will likely try to seek out jobs which I get to use it in.
> language with a garbage collector
That is reasonable. Rust is not the only safe option.
Re everything else....Rust should be seen as the beginning not the end. All those model checking and other "post-hoc" analyses come with major productivity pitfalls. (Wrestling with some solver that may or may not be happy for spooky reasons is profoundly disheartening compared to wrestling with something elegant and compositional like a type system.
Just as there is the ML family of languages and then SML with CakeML, Rust should continue being a fast-moving target where the occasional mistake might happen, but there is academic work revolving around the language which should create a CompCert/CakeML with time.
Some aviation/auto software regulation is a legit, but frankly a some of it doubles as regularity ossification the industry secretly like as it creates a mote around existing businesses that have "evolved" compliance from the get-go. In that case, unproductivity is a feature, not a bug.
I would not hold it up as a realistic model for these sorts of projects to aspire to. Without drastic changes to the way we found unprofitable FOSS foundation infrastructure, whenever productivity and security are at odds, the former will win over the latter.
That is reasonable. Rust is not the only safe option.
Re everything else....Rust should be seen as the beginning not the end. All those model checking and other "post-hoc" analyses come with major productivity pitfalls. (Wrestling with some solver that may or may not be happy for spooky reasons is profoundly disheartening compared to wrestling with something elegant and compositional like a type system.
Just as there is the ML family of languages and then SML with CakeML, Rust should continue being a fast-moving target where the occasional mistake might happen, but there is academic work revolving around the language which should create a CompCert/CakeML with time.
Some aviation/auto software regulation is a legit, but frankly a some of it doubles as regularity ossification the industry secretly like as it creates a mote around existing businesses that have "evolved" compliance from the get-go. In that case, unproductivity is a feature, not a bug.
I would not hold it up as a realistic model for these sorts of projects to aspire to. Without drastic changes to the way we found unprofitable FOSS foundation infrastructure, whenever productivity and security are at odds, the former will win over the latter.
Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc (which had a miscompilation bug until 1.52.1, has no specifications or alternative implementations, right?) will compile is productive? Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not? Furthermore, I’m not aware of any progress in “sealed rust” or “rust belt” other than raising grant money. I don’t think a certification is coming anytime soon. There are other verified compilers that could be used now, though.
This argument sounds like rust for rust’s sake.
This argument sounds like rust for rust’s sake.
> Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc .... will compile is productive?
The rewrite is a 1-time cost.
> Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not?
I am primarily a Haskell user, and I already said I have nothing against GC. Those other languages (except for F#) are great!
> has no specifications or alternative implementations
That is a major downside (I work on GHC and wish it wasn't the only game in town) and affects all of those. That's why I put out SML and the CakeML implementation. SML lacks shiny new stuff but the grunt work has been done.
I would certainly use SML over any variant of C for anything that needs dynamic allocation.
The rewrite is a 1-time cost.
> Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not?
I am primarily a Haskell user, and I already said I have nothing against GC. Those other languages (except for F#) are great!
> has no specifications or alternative implementations
That is a major downside (I work on GHC and wish it wasn't the only game in town) and affects all of those. That's why I put out SML and the CakeML implementation. SML lacks shiny new stuff but the grunt work has been done.
I would certainly use SML over any variant of C for anything that needs dynamic allocation.
> which had a miscompilation bug until 1.52.1,
All compilers have miscompilation bugs. Even ones that are proven correct.
> has no specifications or alternative implementations, right?
There is one alternative implementation that is good enough to bitwise reproduce rustc, there are a few other in-progress alternate implementations.
> I’m not aware of any progress in “sealed rust” or “rust belt”
That doesn't mean they haven't progressed. By the way, "Sealed Rust" is now called "Ferrocene" and is expected to GA in late 2022. https://ferrous-systems.com/ferrocene/
> There are other verified compilers that could be used now, though.
This is true, for sure. A compiler being verified is not a panacea.
All compilers have miscompilation bugs. Even ones that are proven correct.
> has no specifications or alternative implementations, right?
There is one alternative implementation that is good enough to bitwise reproduce rustc, there are a few other in-progress alternate implementations.
> I’m not aware of any progress in “sealed rust” or “rust belt”
That doesn't mean they haven't progressed. By the way, "Sealed Rust" is now called "Ferrocene" and is expected to GA in late 2022. https://ferrous-systems.com/ferrocene/
> There are other verified compilers that could be used now, though.
This is true, for sure. A compiler being verified is not a panacea.
A verified compiler is not panacea, but rust is because of unsubstantiated claims of its marketing professionals? This is total nonsense.
Where did I say Rust is a panacea? A verified Rust compiler is a verified compiler, and wouldn’t be one either.
The stated goal of the grant program is to rewrite stable software many people use in Rust with the implied context being that C can’t be trusted, but Rust can be. I’m surprised that a language with no specified guarantees is favored over well established methods of verification. When you poopoo formal methods and verified compilers, it’s very hard to find a coherent logic behind RIIR, which offers much less in terms of security.
Unless the exercise is a pretext to rationalize the grant money (which would be the real purpose).
Unless the exercise is a pretext to rationalize the grant money (which would be the real purpose).
The formal verification researchers I've worked with love Rust, because its type system nails the basics so they can focus on proving more interesting properties.
Rust and formal verification work really well together. You can formally verify properties in a small section of critical code, then use the type and lifetime systems to expand those properties to the whole codebase. It's not an either/or, it's a both/and.
Rust and formal verification work really well together. You can formally verify properties in a small section of critical code, then use the type and lifetime systems to expand those properties to the whole codebase. It's not an either/or, it's a both/and.
That's fascinating. Can you direct me to any of their papers or public work formally verifying a rust codebase? I haven't seen that before.
For some reason, the slight tilt to the text "Memory Safety" makes me feel queasy. But I guess maybe that's the point?
A comment on lobste.rs summed up my feelings perfectly. https://lobste.rs/s/hpk3lu/prossimo_memory_safety_project#c_...
[1] https://wiki.mozilla.org/Oxidation
[2] https://github.com/ibraheemdev/modern-unix