United States Air Force Academy
Ironsides Secure DNS Server
Dr. Martin C. Carlisle (former director of the Academy Center for Cyberspace Research at the USAF Academy, and now at Carnegie Mellon University) and Dr. Barry Fagin (US Air Force Academy) have developed a secure DNS server using Ada and the SPARK formal methods tool set. 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.
More information can be found at the project link below. Many related papers on SPARK and security are here. This conference paper received a Best Presentation award.