A verifying core for a cryptographic language compiler

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A verifying core for a cryptographic language compiler

Full text

Pdf (300 KB)

Source

ACM International Conference Proceeding Series; Vol. 205 archive
Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications table of contents

Seattle, Washington

SESSION: Session 1 table of contents

Pages: 1 - 10

Year of Publication: 2006

ISBN:0-9788493-0-2

Authors

Lee Pike	Galois Connections, Beaverton, Oregon
Mark Shields	Galois Connections, Beaverton, Oregon
John Matthews	Galois Connections, Beaverton, Oregon

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 46, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Review this Article Save this Article to a Binder Display Formats: BibTex EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1217975.1217977 What is a DOI?

ABSTRACT

A verifying compiler is one that emits both object code and a proof of correspondence between object and source code.¹ We report the use of ACL2 in building a verifying compiler for μCryptol, a stream-based language for encryption algorithm specification that targets Rockwell Collins' AAMP7 microprocessor (and is designed to compile efficiently to hardware, too). This paper reports on our success in verifying the "core" transformations of the compiler -- those transformations over the sub-language of μCryptol that begin after "higher-order" aspects of the language are compiled away, and finish just before hardware or software specific transformations are exercised. The core transformations are responsible for aggressive optimizations. We have written an ACL2 macro that automatically generates both the correspondence theorems and their proofs. The compiler also supplies measure functions that ACL2 uses to automatically prove termination of μCryptol programs, including programs with mutually-recursive cliques of streams. Our verifying compiler has proved the correctness of its core transformations for multiple algorithms, including TEA, RC6, and AES. Finally, we describe an ACL2 book of primitive operations for the general specification and verification of encryption algorithms.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	H. P. Barendregt. The Lambda Calculus. Number 103 in Studies in Logic and the Foundations of Mathematics. North-Holland, revised edition, 1991.
	2	S. Blazy, Z. Dargaye, and X. Leroy. Formal verification of a c compiler front-end. In Proceedings of Formal Methods, 2006. Accepted. Available at http://pauillac.inria.fr/~xleroy/.
	3	Common Criteria for Information Technology Security Evaluation (CCITSE), Mar. 1999. Available at http://www.radium.ncsc.mil/tpep/library/ccitse/ccitse.html.
	4	Maulik A. Dave, Compiler verification: a bibliography, ACM SIGSOFT Software Engineering Notes, v.28 n.6, November 2003 [doi>10.1145/966221.966235]
	5	Federal Information Processing Standards Publication. Specification for the advanced encryption standard (AES). Technical Report 197, National Institute of Standards and Technology, Nov. 2001. Available at http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf.
	6	R. T. C. for Aeronautics (RTCA). DO-178b: Software considerations in airborne systems and equipment certification, Dec. 1992.
	7	A. C. J. Fox. Formal specification and verification of ARM6. In Theorem Proving in Higher-Order Logics (TPHOLs), pages 25--40, 2003.
	8	D. Greve, R. Richards, and M. Wilding. A summary of intrinsic partitioning verification. In In Proceedings of the Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2), Austin, TX, Nov. 2004.
	9	David S. Hardin , Eric W. Smith , William D. Young, A robust machine code proof framework for highly secure applications, Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, August 15-16, 2006, Seattle, Washington [doi>10.1145/1217975.1217978]
	10	Tony Hoare, The verifying compiler: A grand challenge for computing research, Journal of the ACM (JACM), v.50 n.1, p.63-69, January 2003 [doi>10.1145/602382.602403]
	11	Steven D. Johnson, Synthesis of Digital Design from Recursive Equations, MIT Press, Cambridge, MA, 1984
	12	Matt Kaufmann , J. Strother Moore , Panagiotis Manolios, Computer-Aided Reasoning: An Approach, Kluwer Academic Publishers, Norwell, MA, 2000
	13	M. Kaufmann, P. Manolios, and J. S. Moore, editors. Computer Aided Reasoning: ACL2 Case Studies, chapter Chapter 8: High-Speed, Analyzable Simulators. Self-Published, Aug. 2002.
	14	Xavier Leroy, Formal certification of a compiler back-end or: programming a compiler with a proof assistant, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-54, January 11-13, 2006, Charleston, South Carolina, USA
	15	X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system: Documentation and user's manual. Available at http://caml.inria.fr/pub/docs/manual-ocaml/index.html, 2005.
	16	J. R. Lewis and W. B. Martin. Cryptol: High assurance, retargetable crypto development and validation. In Proceedings of the IEEE/AFCEA Conference on Military Communications (MILCOM), Boston, MA, Oct. 2003. Available at http://www.galois.com/files/milcom.pdf.
	17	J. Matthews, J. S. Moore, S. Ray, and D. Vroon. Verification condition generation via theorem proving. Submitted, Mar. 2006.
	18	J. Strother Moore, A mechanically verified language implementation, Journal of Automated Reasoning, v.5 n.4, p.461-492, Dec. 1989
	19	J. S. Moore. A grand challenge proposal for formal methods: A verified stack. In 10th Anniversary Colloquium of UNU/IIST, pages 161--172, 2002.
	20	Isabelle/HOL: a proof assistant for higher-order logic, Springer-Verlag, London, 2002
	21	S. L. Peyton Jones. Implementing lazy functional languages on stock hardware: The Spineless Tagless G-machine. Journal of Functional Programming, 2(2):127--202, Apr. 1992.
	22	S. L. Peyton-Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, 2003. Available at http://www.haskell.org/definition/haskell98-report.ps.gz.
	23	R. L. Rivest1, M. J. B. Robshaw, R. Sidney, and Y. L. Yin. The security of the rc6 block cipher. Technical report, RSA Security, 1998.
	24	Mary Sheeran, Designing regular array architectures using higher order functions, Proc. of a conference on Functional programming languages and computer architecture, p.220-237, January 1985, Nancy, France
	25	M. Shields. A language for symmetric-key cryptographic algorithms and its implementation. Available at http://www.cartesianclosed.com/pub/mcryptol/, Jan. 2006.
	26	M. B. Shields. μCryptol Reference Manual, Nov. 2005. Available at http://www.galois.com/files/mCryptol_refman-0.9.pdf.
	27	K. Slind, G. Li, and S. Owens. A proof-producing software compiler for a subset of higher order logic. Available at http://www.cs.utah.edu/~slind/sw-compiler/, 2006.
	28	K. Slind, S. Owens, J. Iyoda, and M. Gordon. Proof producing synthesis of arithmetic and cryptographic hardware. In Seventh International Workshop on Designing Correct Circuits DCC: Participants' Proceedings, 2006. Satellite Event of ETAPS.
	29	D. J. Wheeler and R. M. Needham. TEA, a tiny encryption algorithm. In B. Preneel, editor, Proceedings of the 1994 Workshop on Fast Software Encryption (FSE), Belgium, volume 1008 of LNCS, pages 363--366. Springer, 1995.