Safety in an `unsafe { world }` | joshlf.com

Skip to main content

This post is a nearly verbatim adaptation of my RustConf 2024 talk. I've kept everything in the present tense as it was in September 2024. Towards the end, I've also included a bit of content that I had planned on presenting but had to skip during the presentation for time.

Watch the talk · See the slides · See the full references

Netstack3

So what is this talk about? Well, I'm going to bury the lede a bit.

First, let's talk about Netstack3. Netstack3 is Fuchsia's next-generation, pure-Rust networking stack. It aims to replace Netstack2, which is written in Go.

I started Netstack3 about six years ago, and led its development for four years, and then for the past two years it's been led by a different team. I haven't been on the project for two years, so obviously this is beyond me now – it's a huge team effort – I'm going to be bragging a lot about those folks. There are some really good engineers who work on that now.

Writing a networking stack is a serious undertaking. It's responsible for almost all network traffic in the entire operating system. It implements dozens of protocols, each of which is specified in documents that can run into the hundreds of pages. And it's the first line of defense against any attacker who isn't physically sitting in front of a device.

It's also just big. As I said a second ago, it's taken us six years to get to this point, there have been plus or minus ten developers that whole time, and it's split across 63 crates totaling 192,000 lines of code. That's more code than the top ten crates on crates.io combined.

Over the past year, the team has been preparing to launch Netstack3. Those of you with networking backgrounds will know that you don't just deploy networking code into production.

Networking code is famously difficult to test, and so you have to assume that, despite your best efforts, your code is riddled with bugs.

For a project of this scale — deploying an entirely new, ground-up rewrite of a netstack — you would expect to dogfood in the field for months or maybe even years before shipping to real users. In that time, you would expect to uncover tens to hundreds of bugs that you hadn't seen during development. And only once you had burned down most of those bugs and seen relatively stable behavior for a while, only then would you finally deploy to real users.

So let's talk about what the process has looked like for Netstack3. For 11 months, the team has been ramping up a dogfooding program. At peak, that program has seen about 60 devices running nearly 24/7 in developers' homes.

Again, if this were any other netstack, we would have expected to uncover a giant mountain of bugs in that time. So, over the past year, how many bugs did the team uncover in the field?

Three.

Note from the future : As of posting, Netstack3 is now in production, running on millions of devices. Immediately after its first deployment, the team observed a ~20x lower rate of crashes per million devices per day and a 50% reduction in memory usage compared to its predecessor, Netstack2.

So this talk is going to be something of a flashback.

Netstack3 was designed around a particular methodology for how to architect robust systems. Hopefully I've convinced you that we did at least something right on the robustness front.

In a sentence, that methodology says:

Buggy programs don't compile.

Obviously, I am far from the first person to suggest this methodology. Here is just a small sample of crates that use this methodology somewhere in their APIs:

ghost-cell, session_types, nalgebra, mundane, indexing, zerocopy, and bytemuck.

And here is a small sample of what has been written on the topic, both about Rust and about other languages:

References are like jumps, by withoutboats

Parse, don't validate, by Alexis King

Type Safety Back and Forth, by Matt Parsons

Ghosts of Departed Proofs, by Matt Noonan

The Typestate Pattern in Rust, by Cliff Biffle

Compiler-Driven Development in Rust, by No Boilerplate

Some notes on Rust, mutable aliasing and formal verification, by Graydon Hoare

So my goal for this talk is not to introduce a new idea.

Instead, my goals are:

First, I'm going to propose a concrete but general framework that attempts to unify all of the different ways this methodology shows up in practice, and explain them in terms of the same basic concepts.

Second, I'm going to walk through two examples — one from the standard library and one from Netstack3 — and show how we can explain them in terms of this framework.

Unfortunately 25 minutes isn't enough time to present more than two examples in the depth I'd like. I had to leave a lot on the cutting-room floor when I was writing this talk. But I promise that these two examples only scratch the surface of what's possible. The full list of references contains a surprising diversity of problems which this methodology has already been applied to.

What do we...