Ironsides, formally proven DNS now handles Recursive DNS

IRONSIDES is an authoritative/recursive DNS server pair that is provably invulnerable to many of the problems that plague other servers. It achieves this property through the use of formal methods in its design, in particular the language Ada and the SPARK formal methods tool set. Code validated in this way is provably exception-free, contains no data flow errors, and terminates only in the ways that its programmers explicitly say that it can. These are very desirable properties from a computer security perspective.

IRONSIDES is not a complete implementation of DNS. In particular, it does not support zone transfers or all query types. It does, however, support a sufficient number of DNS records to be useful as a DNS server for an enterprise.

DNS In A Nutshell
DNS connects browsers to servers by translating URLs into the IP (Internet Protocol) numbers that are used by routers and servers to direct HTTP requests and data to the right places.

There are two fundamental types of DNS servers that allow this to work: the servers that respond to browser’s queries and the servers that hold the canonical information about which IP maps to which URL.

Recursive DNS Servers
When your browser sends out a DNS query — assuming the browser doesn’t already have the mapping stored in its cache — it is sent to a recursive DNS server. Recursive servers are the part of the DNS that provides the required information to web clients. They are usually managed by ISPs or the organizations that own the domain from which the connection is being made — a company, for example, although there are some popular public recursive DNS servers run by big corporations like Google and other organizations.

Authoritative DNS Servers
Authoritative DNS servers “know” the mapping of URL to IP for a domain. They are the source of the information that the recursive DNS servers send to web clients like browsers. Authoritative DNS servers for a website are usually provided by web hosting companies or specialist DNS hosting companies.

Thus, as DNS is so fundamental to the internet's structure, it is very good that there's now a formally verified implementation.

Ada ... a very good programming language with less career potential than Cobol or Fortran.

Perhaps; but if formal verification becomes widely adopted (and things like the [fairly] recent heartbleed bug make it seem that it is the direction we need to go) Ada has some very nice qualities for verification (in addition to its reputation for safety-critical systems).

So, mayhaps the career-potential will increase.

Having implemented MSDNS, BIND, and Ironsides, I can tell you that Ironsides blows away the competition for security. DNS poisoning is impossible if configured by a competent admin.

That being said, Ironsides lacks a lot of the features available in MSDNS and a lot of the flexibility of BIND.

Disclaimer: Opinions posted on Free Republic are those of the individual posters and do not necessarily represent the opinion of Free Republic or its management. All materials posted herein are protected by copyright law and the exemption for fair use of copyrighted works.