Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations

TitleEfficient Symbolic Execution for Analysing Cryptographic Protocol Implementations
Publication TypeConference Paper
Year of Publication2011
AuthorsCorin, R, Manzano, FA
EditorErlingsson, Ú, Wieringa, R, Zannone, N
Conference NameEngineering Secure Software and Systems - Third International Symposium, ESSoS 2011, Madrid, Spain, February 9-10, 2011. Proceedings
ISBN Number978-3-642-19124-4
AbstractThe 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.
DOI10.1007/978-3-642-19125-1_5
Powered by Drupal