High assurance programming in Cryptol

摘要

In this extended abstract, we have provided a very brief overview of the verification framework of Cryptol, a key ingredient of Cryp-tol's high-assurance development environment. The system has already proved itself useful in practice, especially in establishing the equivalence of reference and pipelined implementations of crypto-algorithms, essential in generating efficient FPGA representations. Since such transformations are done both manually by programmers and automatically by the compiler, it is absolutely essential to ensure that correctness is preserved through many structural transformations applied to obtain a time/space efficient realization.