Efficient symbolic execution for analysing cryptographic protocol implementations

Abstract. The analysis of code that uses cryptographic primitives is unfeasible with current state-of-the-art symbolic execution tools. We de-velop 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.