Provably Secure DNS: A Case Study in Reliable Software

http://ironsides.martincarlisle.com ^ | Unknown | Barry Fagin and Martin Carlisle

[OneWingedShark]

Abstract.
We describe the use of formal methods in the development of IRONSIDES, an implementation of DNS with superior performance to both BIND and Windows, the two most common DNS servers on the Internet. More importantly, unlike BIND and Windows, IRONSIDES is impervious to all single-packet denial of service attacks and all forms of remote code execution.

Introduction
DNS is a protocol essential to the proper functioning of the Internet. The two most common implementations of DNS are the free software version BIND and the implementations that come bundled with various versions of Windows. Unfortunately, despite their ubiquity and importance, these implementations suffer from security vulnerabilities and require frequent patching. As of this writing, according to the Internet Systems Consortium’s web site, there are 51 known vulnerabilities in various versions of BIND [1]. Over the past five years, Microsoft has released at least 8 security bulletins relating to vulnerabilities in Windows DNS. Since neither of these products have ever been, to our knowledge, formally validated, it is likely that further flaws remain for hackers to discover and exploit.

The existence of security flaws in such a vital component of the Internet software suite is troubling, to say the least. These vulnerabilities permit not only bad-packet denial of service attacks to crash a DNS server, but in the worst case can actually lead to remote code execution exploits, giving the adversary control over the host machine. To address this problem, the authors have used formal methods and the SPARK tool set from Praxis Systems to develop a high-performance version of DNS that is provably exception-free.

[OneWingedShark]

Here's an interesting paper [PDF] if you're interested in computer correctness or security.

[OneWingedShark]

Tech ping.

[Errant]

The system’s distributed nature means that there is no central DNS server.

mE likely!!

[ShadowAce]

[ro_dreaming]

ping for later

[OneWingedShark]

Well, that's the DNS-system… though with Ada's Annex E (Distributed systems) you could make it so your DNS-program was distributed, too.

[Errant]

Okay then, just don’t screw with distribution. In fact, look at improving it (more efficient, less hierarchy). Not something TPTB are going to allow today, IMO.

[rarestia]

If MS DNS is implemented properly, it’s as secure as BIND. Most admins deploy MS DNS with secure updates turned off and zone transfers enabled from all sources, which is just a nightmare for administration and security overall.

[OneWingedShark]

If MS DNS is implemented properly, it’s as secure as BIND. Most admins deploy MS DNS with secure updates turned off and zone transfers enabled from all sources, which is just a nightmare for administration and security overall.

But the point here is that BIND isn't secure either. Ironsides, on the other hand, is provably free of exceptions (the paper here) and both single-packet denial of service and remote code executions (this paper). That's a huge distinction.

[rarestia]

I’m absolutely not taking away from that point, sir. I just wanted to jump to the defense of MSDNS since the paper seemed to jump on it as flawed. Every system is flawed with the right backdoors or vulnerabilities to exploit.

We’re already discussing IRONSIDES here internally.

[OneWingedShark]

I’m absolutely not taking away from that point, sir. I just wanted to jump to the defense of MSDNS since the paper seemed to jump on it as flawed. Every system is flawed with the right backdoors or vulnerabilities to exploit.

Ah, I see. You are certainly right that MS DNS can be as secure as BIND, I would actually be surprised if BIND didn't actually have statistically more than MS DNS because [IIUC] MS has, over the past few years, been integrating some prover technology into their build-cycle/code-review. -- Of course since they're likely using languages that are highly resistant to analysis (the C-family as a whole) I'd take that with a grain of salt.

[rarestia]

Don’t mistake my defense here. I believe BIND to be far superior to MSDNS. BIND allows split-horizon and ACL recursion, but MSDNS is much faster than BIND over all, as evidenced in the paper.

Also, given the prevalence of MS products in many corporate environments, MS DNS is the predominant product deployed for DNS over BIND as a whole.

[Noumenon]

If MS DNS is implemented properly, it’s as secure as BIND. Most admins deploy MS DNS with secure updates turned off and zone transfers enabled from all sources, which is just a nightmare for administration and security overall.

This. Lazy admins take the shotgun approach. Not smart.

[rarestia]

When it comes to high-level domain infrastructure, implementation should be surgical.

MS infrastructure is my expertise. My last few jobs I’ve been hired to “clean up” implementations, esp. post-Novell migrations, and I’ve yet to come across a company that does it correctly.

Engineers don’t like to document and scope everything, so the installation usually goes full-default and it’s just a mess. DNS is no exception.

[Noumenon]

When it comes to high-level domain infrastructure, implementation should be surgical. But most of the time it resembles sausage-making, doesn't it? The lack of documentation is the bane of my existence. Even simple Visio diagrams would be helpful, but I've almost always gotten blank looks when I ask for them.

And yeah, Netware migrations tend to be messy. It's almost better to start from scratch using best practices for a clean implementation.

[rarestia]

My academic background is in English comp and professional writing, but I’ve been in IT for 20 years. They love me in my shop, because I’m the documentation guy and I don’t mind it.

My personal quote: “You can lead an engineer to documentation, but you can’t make him read it.”

[OneWingedShark]

My academic background is in English comp and professional writing, but I’ve been in IT for 20 years. They love me in my shop, because I’m the documentation guy and I don’t mind it.
My personal quote: “You can lead an engineer to documentation, but you can’t make him read it.”

That's pretty cool.