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. We define concrete and symbolic semantics within a (subset) of the low-level virtual machine LLVM. We then show our approach sound by proving operational correspondence between the two semantics. We present a prototype to illustrate our approach and discuss next milestones towards the symbolic analysis of fully concurrent cryptographic protocol implementations.

Bio: Felipe Andres Manzano obtained his degree in Computer Science from FCEIA, Universidad Nacional de Rosario, Argentina. He is currently a PhD candidate at FaMAF, Universidad Nacional de Cordoba, Argentina, working under the supervision of Ricardo Corin. His research focuses on testing and formal verification of cryptographic protocols and their implementations.