John Launchbury, Cryptol in Future Cryptographic Evaluations (February 16, 2006)
From the CISR video library (http://www.cisr.us)
John Launchbury, Ph.D., President and CEO, Galois Connections Inc.
Cryptol in Future Cryptographic Evaluations
February 16, 2006
at the
Naval Postgraduate School
(http://www.nps.edu)
ABSTRACT
With growing demand, the next generation of cryptographic devices is required to be programmable and to attain throughput speeds of many gigabits per second. Devices that meet both of these requirements threaten to stress the evaluation process to breaking point. Working through Galois, the NSA is pursuing a fresh approach to the cryptographic evaluation problem by developing tools based around Cryptol, a formal cryptography specification language. The tools provide capabilities to generate FPGA implementations automatically from high level mathematical specifications, to generate test vectors and other aids for human developers, and to verify implementations formally against their specifications. This talk will explore the world of Cryptol, and provide insights into how formal techniques can be packaged to make them fully available to non-specialists.
Bio: John Launchbury founded Galois in 1999 to address challenges in Information Assurance through the application of Functional Programming and Formal Methods. The company has grown through successes on multiple contract awards for U.S. Government customers, and gained stature for its advanced technology development. John received First Class Honours in Mathematics from Oxford University in 1985. His Ph.D. in Computing Science won the British Computer Society's distinguished dissertation prize. John retains status as a full professor of Computer Science and Engineering, currently on extended entrepreneurial leave from the OGI School of Science and Engineering at OHSU. John's teaching style has earned him awards for outstanding teaching at OGI, and his work on Haskell and on the semantics of programming languages is internationally recognized.