- Homepage
- About the Joint Centre
- Research Areas & Projects
- Researchers
- News & Events
- Open Positions
Wednesday 8 October 2008, 11h, batiment I, 1er étage
Refinement Typechecking for Security Verification
Karthik Bhargavan
Microsoft Research, Cambridge
We report on recent experimental results using the F7: an enhanced typechecker for the F# programming language. F7 supports static checking of properties expressed with refinement types. We use it to verify confidentiality and authenticity properties of ML code implementing cryptographic protocols.
The talk will cover two ongoing case studies:
(1) verifying auto-generated custom protocol implementations of multi-party sessions, and
(2) verifying an implementation of a web services-based identity management protocol.
We will outline verification tasks and challenges, and describe enhancements to the typechecker.