How Cloudflare Uses Racket and Rosette to Verify DNS Changes

Keynote
James Larisch and Suleman Ahmad
How Cloudflare Uses Racket and Rosette to Verify DNS Changes
Since 2022, Cloudflare has used Racket and Rosette to prevent DNS-related bugs. Cloudflare engineers express desired DNS behavior as small programs called policies, written in a custom DSL called topaz-lang. Topaz-lang policies are executed in real-time on Cloudflare’s global edge network in response to live DNS queries. But before deployment, all policies are checked for bugs using a verifier we wrote in Rosette, a solver-aided Racket #lang.
In this talk, we describe our experience writing and using Racket in production at Cloudflare. We describe why managing DNS behavior at Cloudflare scale is so challenging, and how these challenges motivated topaz-lang and its parent system Topaz. We discuss why we chose Racket (and Rosette) and the types of bugs our Rosette verifier detects. Finally, we reflect on why making changes to our verifier remains daunting for many software engineers.

Bio: Suleman is a Research Engineer at Cloudflare, working at the intersection of systems engineering and Internet security. He holds a Master’s degree from the University of Wisconsin–Madison, where he focused on analyzing security and privacy challenges in large-scale Internet architectures and engineering scalable measurement platforms. It was during his master’s studies that he developed an appreciation for functional programming and its practical application to verifiable distributed systems.
James is a systems/security researcher and programming language fanboy. He developed his appreciation for the functional style (and Racket) during his undergraduate degree at Northeastern University. He received his PhD in Computer Science from Harvard University, where one of his projects involved bringing Prolog to the Web Public Key Infrastructure. He is currently a Research Engineer at Cloudflare, where he works on the Web PKI, distributed systems, and a bit of formal methods.