Andrew Herbert Career Celebration Workshop: Verifying Cryptographic Code in C

October 3, 2011
Andy Gordon

From the Andrew Herbert Career Celebration Workshop.

Speaker Details

Andy Gordon is a Principal Researcher at MSR Cambridge. His research interests are in the general areas of security and programming languages. His work at Microsoft has involved applying type theory and other formal techniques to problems of computer security, in projects including the following: an analysis (with Don Syme) of the type system underlying the bytecode verifier of the Microsoft .NET Common Language Runtime; Cryptyc (with Alan Jeffrey), a type-checker for cryptographic protocols; and the Samoa Project (with Karthik Bhargavan and Cédric Fournet) on formal tools for the security of XML Web Services. He is currently excited about the many possibilities of refinement types, and is actively developing them in the context of F7, an enhanced typechecker for the F# programming language. F7 is work in collaboration with Karthik Bhargavan, Cédric Fournet, and our colleagues.