- Homepage
- About the Joint Centre
- Research Areas & Projects
- Researchers
- News & Events
- Open Positions
Bât. I. 1st floor
Microsoft Research - Inria Joint Centre
Parc Orsay Université
Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations
Ricardo Corin, Universidad Nacional de Cordoba, Argentina
The analysis of code that uses cryptographic primitives is unfeasible with current state-of-the-art symbolic execution tools. We develop an extension that overcomes this limitation by treating certain concrete functions, like cryptographic primitives, as symbolic functions whose execution analysis is entirely avoided; their behaviour is in turn modelled formally via rewriting rules. Our code runs in a (simplified) LLVM virtual machine. We develop concrete and symbolic semantics for our LLVM, and we show our approach sound by proving operational correspondence between the two semantics. We present a prototype to illustrate our approach with several (sequential code) examples, and we discuss next milestones towards the symbolic analysis of fully concurrent cryptographic protocol implementations.