Welcome to the Ironsides home page

$Description: C:\d\My Documents\My Webs\mcc_html\ironsides\index_files\image001.jpg$

The content of this page in no way reflects the opinions, standards, or policy of the United States Air Force Academy or the United States government.

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.

The GLOBECOM 2012 paper describing IRONSIDES, including a performance comparison with BIND is linked here. The 18th International Conference on Reliable Software Technologies - Ada-Europe 2013 paper is linked here.

Download

Download the April 15, 2015 AUTHORITATIVE snapshot

Download the June 4, 2014 AUTHORITATIVE snapshot

Download the June 4, 2014 RECURSIVE snapshot – NEW!

Download the June 4, 2014 Windows binaries (both authoritative and recursive) – NEW!

Older versions

Download the February 20, 2014 snapshot – AUTHORITATIVE ONLY

Download the March 15, 2013 snapshot – AUTHORITATIVE ONLY

Download the February 11, 2013 snapshot – AUTHORITATIVE ONLY

Download the August 13, 2012 snapshot – AUTHORITATIVE ONLY

As of 15 March 2013, IRONSIDES has added

SRV records
better Linux compilation instructions

As of 11 February 2013, IRONSIDES has added

Offline signed DNSSEC records (DNSKEY, RRSIG, NSEC)

As of 13 August 2012, IRONSIDES supports ONLY

Running as authoritative server (no recursive queries)
A, AAAA, CNAME, MX, NS, PTR, SOA records

Work is continuing to add DNSSEC and recursive queries

To compile and run IRONSIDES, you'll need an Ada compiler and the SPARK 2012 libraries. You can download GNAT GPL (a free Ada compiler) from Ada Core. SPARK 2012 is also available for download from Ada Core. We discourage using other distributions of GNAT (such as the one you can "apt-get" in Ubuntu), as we ran across a compiler bug that was still present in that version. Later versions of SPARK (after 2012) do not yet support tasking, and are a major language rewrite.

Using the downloaded source (AUTHORITATIVE)

The command we use to compile is:

gnatmake -gnat05 -O3 -gnatp -Ic:\spark\2012\lib\spark -Ic:\spark\2012\lib\spark\current spark_dns_main

To run the program, use:

spark_dns_main input_file

A sample input file is in dfcs.usafa.edu.zonefile. If running on Linux, use "dos2unix dfcs.usafa.edu.zonefile" to convert the end of line symbols. You may need administrative privileges to open a socket on a low numbered port. On linux, use "sudo ./spark_dns_main dfcs.usafa.edu.zonefile" or run from root. More thorough Linux instructions are in the README

If you wish to modify the program, the batch file "allbob.bat" shows how to run SPARK to generate all of the proofs (with a summary in "trunk.sum").

Using the downloaded source (RECURSIVE)

The command we use to compile is:

gnatmake -gnat05 -O3 -gnatp -Ic:\spark\2012\lib\spark -Ic:\spark\2012\lib\spark\current spark_dns_v1_1_main

To run the program, use:

spark_dns_v1_1_main –s IP_ADDRESS_OF_UPSTREAM_SERVER

For example (to use Google as your upstream server):

spark_dns_v1_1_main –s 8.8.8.8

If you wish to modify the program, the batch file "allbob.bat" shows how to run SPARK to generate all of the proofs (with a summary in "trunk.sum").

Ironsides is Free!

Ironsides is freely distributed as a service to the computer security community. Ironsides was originally developed by the US Air Force Academy, Department of Computer Science.

Authors:

Martin C. Carlisle
Barry Fagin

Feedback

Comments, suggestions, and bug reports are welcome. If you have a comment, suggestion or bug report, send an email to Martin Carlisle.

Acknowledgements

This work was supported by DARPA. The information here does not represent the official policies, either expressed or implied, of the Defense Advanced Research Projects Agency (DARPA) or the Department of Defense. DARPA does not guarantee the accuracy or reliability of the software or the information in the paper(s).

We also thank AdaCore Technologies and Altran Praxis for providing technical support on using their tools.