Andrew Herbert Career Celebration Workshop: Verifying Cryptographic Code in C

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.

Date:
Speakers:
Andy Gordon
    • Portrait of Andy Gordon

      Andy Gordon

      Partner Research Manager

    • Portrait of Jeff Running

      Jeff Running