Our goal is to create guaranteed correct implementations of cryptographic algorithms in both hardware and software. This is part of a more general investigation to explore the use of automated deduction for compiling mathematical specifications into implementations.
Our approach is to specify crytographic algorithms and the mathematics needed for their verification in higher order logic (specifically in the HOL Logic), and then to implement them by formal deductive compilation to ARM software and custom hardware (both also modelled in higher order logic). The aim is to generate 'golden' implementations that can be used to evaluate other implementations generated by a more conventional process.
We plan to explore how to meet the verification requirements of FIPS 140-2 Level 4 and the Common Criteria Evaluation Assurance Level 7 (EAL7), which are the highest assurance levels currently used for procurement. EAL7 only requires "a semiformal presentation of the low-level design, and formal and semiformal demonstration of correspondence between them". We hope to create machine checked fully formal specifications and verifications of low-level designs, so our research will go beyond existing assurance levels.