Reprogrammable High Assurance Internet Protocol Encryptor

Field Programmable Gate Arrays are widely recognized as an attractive technology for satisfying the needs of U.S. Government Crypto Modernization programs. However, FPGA technology creates some interesting challenges in terms of reliability and assurance of crypto implementations. In the late 1990s, the National Security Agency recognized the need to significantly improve the state-of-the-art for high assurance crypto implementations, and funded Galois Connections to research and propose compiler and formal method techniques in developing a solution. The result is the Cryptol specification language and tools intended for producing High Assurance cryptographic modules. The NSA subsequently funded Galois to develop a compiler to directly translate high-level Cryptol specifications into highly-efficient FGPA cores in an assured manner. Topic AF06-062 seeks to develop and demonstrate a programmable encryption device capable of meeting HAIPE requirements for use in future satellite communications applications. Galois proposes to address the demanding requirements of such an application by focusing on delivering the right tools for producing High Assurance cryptographic modules targeted to state of the art cryptographic hardware. For the hardware platform, Galois proposes to work in partnership with Rockwell Collins to target their next generation cryptographic platform, the Gigabit Encryptor, which is currently under development at Rockwell Collins.