We develop an extension of standard symbolic execution to tackle the analysis of code that uses black box functions like cryptographic primitives. Our extension treats such primitives as symbolic terms that can be rewritten and simplified within an equational theory.
Our code runs in a (simplified) LLVM virtual machine. We develop concrete and symbolic semantics for our LLVM, and show our approach sound by proving operational correspondence between the two semantics.
We develop a prototype and illustrate the usefulness of our approach with several (sequential code) examples, and discuss next milestones towards symbolically analysing fully concurrent cryptographic protocol implementations.