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-
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.
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:
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").
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.