| Title | Efficient Symbolic Execution for Analysing Cryptographic Protocol Implementations |
| Publication Type | Conference Paper |
| Year of Publication | 2011 |
| Authors | Corin, R, Manzano, FA |
| Editor | Erlingsson, Ú, Wieringa, R, Zannone, N |
| Conference Name | Engineering Secure Software and Systems - Third International Symposium, ESSoS 2011, Madrid, Spain, February 9-10, 2011. Proceedings |
| ISBN Number | 978-3-642-19124-4 |
| Abstract | 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. |
| DOI | 10.1007/978-3-642-19125-1_5 |
