Security protocol specifications; formal manalysis; C reverse engineering
Résumé :
[en] Often, analysts have to face a challenging situation when formally verifying the implementation of a security protocol: they need to build a model of the protocol from only poorly or not documented code, and with little or no help from the developers to better understand it. Security protocols implementations frequently use services provided by libraries coded in the C programming language; automatic tools for codelevel reverse engineering offer good support to comprehend the behavior of code in object-oriented languages but are ineffective to deal with libraries in C. Here we propose a systematic, yet human-dependent approach, which combines the capabilities of state-of-the-art tools in order to help the analyst to retrieve, step by step, the security protocol specifications from a library in C. Those specifications can then be used to create the formal model needed to carry out the analysis.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
VAZQUEZ SANDOVAL, Itzel ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
LENZINI, Gabriele ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT)
Co-auteurs externes :
no
Langue du document :
Anglais
Titre :
Experience report: How to extract security protocols’ specifications from C libraries
Date de publication/diffusion :
juin 2018
Nom de la manifestation :
COMPSAC 2018: 42nd IEEE International Conference on Computers, Software and Applications
H. Garavel and S. Graf, "Formal methods for safe and secure computers systems, " Federal Office for Inf. Security, Tech. Rep., 2013.
B. Blanchet, "A computationally sound automatic prover for cryptographic protocols, " in Workshop on the link between formal and computational models, Paris, France, Jun. 2005.
K. Beck, J. Grenning, R. Martin, M. Beedle, J. Highsmith, S. Mellor, A. Van Bennekum, A. Hunt, Schwaber, Cockburn, Jeffries, Sutherland, Cunningham, Kern, Thomas, Fowler, and Marick, "Manifesto for agile software development, " 2001, accessed: 2018-01-11.
C. Dougherty, K. Sayre, R. Seacord, D. Svoboda, and K. Togashi, "Secure design patterns, " SFW Engineering Inst., Carnegie Mellon University, Pittsburgh, PA, Tech. Rep. CMU/SEI-2009-TR-010, 2009.
Wikipedia, "Comparison of cryptography libraries, " https://en. wikipedia. org/wiki/Comparison of cryptography libraries.
E. Eilam, Reversing: Secrets of Reverse Engineering. New York, NY, USA: John Wiley & Sons, Inc., 2005.
E. J. Chikofsky and J. H. Cross, "Reverse engineering and design recovery: a taxonomy, " IEEE Software, vol. 7, no. 1, pp. 13-17, 1990.
B. P. Douglass, "Uml for the c programming language, " IBM, Tech. Rep., June 2009.
M. Fowler, Refactoring: Improving the Design of Existing Code. Boston, MA, USA: Addison-Wesley, 1999.
P. Tonella and R. Potrich, "Reverse engineering of the interaction diagrams from c++ code, " in In International Conference on Software Maintenance, 2003, pp. 159-168.
N. Tiwari and L. Prasad, "Reverse engineering tools for simplifying programming environment through flowcharting, " Int. Journal of Eng. Trends and Technology (IJETT), vol. 26, pp. 65-71, 8 2015.
J. Narayan, S. Shukla, and T. Charles Clancy, "A survey of automatic protocol reverse engineering tools, " ACM Computing Surveys, vol. 48, pp. 1-26, 12 2015.
M. Avalle, A. Pironti, and R. Sisto, "Formal verification of security protocol implementations: a survey, " Formal Aspects of Computing, pp. 1-25, 2012.
M. Aizatulin, A. D. Gordon, and J. Jürjens, "Extracting and verifying cryptographic models from C protocol code by symbolic execution, " in Proceedings of the 18th ACM Conf. on Computer and Communications Security, ser. CCS '11. NY, USA: ACM, 2011, pp. 331-340.
