Pragmatic Equivalence and Safety Checking in Cryptol

摘要

Cryptol is programming a language designed for specifying and programming cryptographic algorithms. In order to meet high-assurance requirements, Cryptol comes with a suite of formal-methods based tools allowing users to perform various program verification tasks. In the fully automated mode, Cryptol uses modern off-the-shelf SAT and SMT solvers to perform verification in a push-button manner. In the manual mode, Cryptol produces Is-abelle/HOL specifications that can be interactively verified using the Isabelle theorem proven In this paper, we provide an overview of Cryptol's verification toolset, describing our experiences with building a practical programming environment with dedicated support for formal verification.