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 DNS server 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 recursive queries. It does, however, support a sufficient number of DNS records to be useful as an authoritative 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 the February 20, 2014 snapshot

Download the March 15, 2013 snapshot

Download the February 11, 2013 snapshot

Download the August 13, 2012 snapshot

As of 15 March 2013, IRONSIDES has added

As of 11 February 2013, IRONSIDES has added

As of 13 August 2012, IRONSIDES supports ONLY

Work is continuing to add DNSSEC and recursive queries

To compile and run IRONSIDES, you'll need an Ada compiler and the SPARK libraries. You can download GNAT GPL (a free Ada compiler) from Ada Core. SPARK 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. We have received a report that you need to use the 2012 version of SPARK on Ubuntu.

Using the downloaded source

The command we use to compile is:

gnatmake -gnat05 -O3 -gnatp -Ic:\spark\2011\lib\spark -Ic:\spark\2011\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").

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.



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


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.