Personal tools
You are here: Home Events Lab Lunch: Prof Andrew D. Gordon

Lab Lunch: Prof Andrew D. Gordon

Title: Experience with Verifying Cryptographic Software in C

What
When Jul 12, 2011
from 01:00 PM to 02:00 PM
Where IF, MF2
Add event to calendar vCal
iCal

Experience with Verifying Cryptographic Software in C

Andrew D. Gordon (MSR and University of Edinburgh)

Based on joint work with Mihhail Aizatulin (OU), Francois Dupressoir (OU), Jan Juerjens (Dortmund), and David A. Naumann (Stevens)

 

The security of much critical infrastructure depends in part on cryptographic software coded in C, and yet vulnerabilities continue to be discovered in such software. I describe recent progress on checking the security of C code. In particular, I describe projects that combine verification-condition generation and symbolic execution techniques for C, with methods for stating and verifying security properties of abstract models of cryptographic protocols. I illustrate these techniques on C code for a simple two-message protocol. I conclude with some suggestions for future work.

http://dl.dropbox.com/u/10577207/Publications/extracting.pdf

http://dl.dropbox.com/u/10577207/Publications/guiding-csf.pdf

Document Actions