Levent Erkök
ABSTRACT
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 Isabelle/HOL specifications that can be interactively verified using the Isabelle theorem prover. 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.
- Clark Barrett and Cesare Tinelli. CVC3 web site. cs.nyu.edu/acsys/cvc3, 2008.Google Scholar
- Koen Claessen and John Hughes. QuickCheck: A lightweight tool for random testing of Haskell programs. In Proc. of International Conference on Functional Programming (ICFP). ACM SIGPLAN, 2000. Google ScholarDigital Library
- J. Duan, J. Hurd, G. Li, S. Owens, K. Slind, and J. Zhang. Functional correctness proofs of encryption algorithms. In G. Sutcliffe and A. Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2005), volume 3835 of Lecture Notes in Artificial Intelligence. Springer-Verlag, December 2005. Google ScholarDigital Library
- Bruno Duterte and Leonardo de Moura. The YICES SMT Solver. Available at: yices.csl.sri.com/tool-paper.pdf, 2006.Google Scholar
- Morris Dworkin. Recommendation for block cipher modes of operation: Methods and techniques, December 2001. URL http://csrc.nist.gov/publications/nistpubs/800-38a/sp800-38a.pdf. NIST Special Publication 800-38A.Google Scholar
- Niklas Eén and Niklas Sörensson. An extensible SAT-solver. In Enrico Giunchiglia and Armando Tacchella, editors, SAT, volume 2919 of Lecture Notes in Computer Science, pages 502--518. Springer, 2003. ISBN 3-540-20851-8.Google Scholar
- Xiushan Feng. Formal equivalence checking of software specifications vs. hardware implementations. PhD thesis, Vancouver, BC, Canada, Canada, 2007. Google ScholarDigital Library
- DPTAmit Goel, Jim Grundy, and Sava Krstić. DPT web site. http://sourceforge.net/projects/dpt, 2008.Google Scholar
- George Hagen and Cesare Tinelli. Scaling up the formal verification of Lustre programs with SMT-based techniques. In A. Cimatti and R. Jones, editors, Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD'08), Portland, Oregon, Lecture Notes in Computer Science. Springer, 2008. URL ftp://ftp.cs.uiowa.edu/pub/tinelli/papers/HagTin-FMCAD-08.pdf. Google ScholarDigital Library
- N. Halbwachs, P. Caspi, P. Raymond, and D. Pilaud. The synchronous dataflow programming language lustre. In Proceedings of the IEEE, pages 1305-1320, 1991.Google ScholarCross Ref
- J. Roger Hindley. Basic Simple Type Theory, volume 42. Cambridge University Press, Cambridge, UK, 1997. Google ScholarDigital Library
- Shi-Yu Huang and Kwant-Ting Cheng. Formal Equivalence Checking and Design Debugging. Kluwer Academic Publishers, Norwell, MA, USA, 1998. Google ScholarDigital Library
- Joe Hurd. Embedding Cryptol in higher order logic. Available from the author's website, March 2007. URL http://www.gilith.com/research/papers.Google Scholar
- Daniel Kroening and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2008. Google ScholarDigital Library
- J. R. Lewis and B. Martin. Cryptol: high assurance, retargetable crypto development and validation. In Military Communications Conference 2003, volume 2, pages 820--825. IEEE, October 2003. Google ScholarDigital Library
- Guodong Li and Konrad Slind. An embedding of Cryptol in HOL-4. Unpublished draft, 2005.Google Scholar
- Alan Mishchenko. ABC: System for sequential synthesis and verification. Release 70930, Available at: http://www.eecs.berkeley.edu/ alanmi/abc, 2007.Google Scholar
- T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic. LNCS 2283. Springer, 2002. Google ScholarDigital Library
- NIST. Announcing the AES, November 2001. URL http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf. FIPS Publication 197.Google Scholar
- Thomas Nordin. The jaig Equivalence Checker. Available from Objective Security Company, 2005.Google Scholar
- Lee Pike, Mark Shields, and John Matthews. A verifying core for a cryptographic language compiler. In ACL2 '06: Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, pages 1--10, New York, NY, USA, 2006. ACM. ISBN 0-9788493-0-2. http://doi.acm.org/10.1145/1217975.1217977. Google ScholarDigital Library
- John C. Reynolds. Definitional interpreters for higher-order programming languages. In ACM '72: Proceedings of the ACM annual conference, pages 717--740, New York, NY, USA, 1972. ACM. http://doi.acm.org/10.1145/800194.805852. Google ScholarDigital Library
- Konrad Slind, Scott Owens, Juliano Iyoda, and Mike Gordon. Proof producing synthesis of arithmetic and cryptographic hardware. Formal Aspects of Computing, 19 (3), August 2007. Google ScholarCross Ref
- A. Tarski, A. Mostowski, and R. M. Robinson. Undecidable Theories. North-Holland Publishing Company, 1953.Google Scholar
- Diana Toma and Dominique Borrione. Formal verification of a SHA-1 circuit core using ACL2. In Joe Hurd and Thomas F. Melham, editors, TPHOLs, volume 3603 of Lecture Notes in Computer Science, pages 326--341. Springer, 2005. ISBN 3-540-28372-2. Google ScholarDigital Library
- Tjark Weber and Hasan Amjad. Efficiently checking propositional refutations in HOL theorem provers. Journal of Applied Logic, July 2007. URL http://dx.doi.org/10.1016/j.jal.2007.07.003.Google Scholar
Index Terms
- Pragmatic equivalence and safety checking in Cryptol
Recommendations
Comparing HOL and MDG: a case study on the verification of an ATM switch fabric
Interactive formal proof and automated verification based on decision graphs are two contrasting formal hardware verification techniques. In this paper, we compare these two approaches. In particular, we consider HOL and MDG. The former is an ...
Verifying safety properties of a nonlinear control by interactive theorem proving with the Prototype Verification System
Interactive, or computer-assisted, theorem proving is the verification of statements in a formal system, where the proof is developed by a logician who chooses the appropriate inference steps, in turn executed by an automatic theorem prover. In this ...
Proving Invariants of I/O Automata with TAME
This paper describes a specialized interface to PVS called TAME (Timed Automata Modeling Environment) which provides automated support for proving properties of I/O automata. A major goal of TAME is to allow a software developer to use PVS to specify ...
Comments