Vérification de la sécurité de code C

Description

La plupart des logiciels que l'on utilise tous les jours sont écrits en langage bas-niveau C/C++, certaines applications comportent même des parties écrites directement en assembleur. Ces langages permettent de créer des programmes très efficaces et performants mais ils sont très vulnérables à des attaques de type injection de code, corruption de code, fuite d'information, \(\ldots\) En effet, ces attaques exploitent typiquement des bugs de programmation le plus souvent dûs à la (mauvaise) gestion de la mémoires [13]. Une autre menace apparaît lorsque les applications s'éxecutent sur de petits systèmes embarqués : ceux-ci peuvent être soumis à des attaques physiques [1,11,9] qui permettent de récupérer des informations, d'accéder à des services sans y être autorisé, prendre le contrôle du système sans même exploiter de vulnérabilités logicielles. Les objets connectés (\emph{internet of things}) qui font de plus en plus partie de notre vie quotidienne deviennent des objets critiques [3] comme le montre les dernières attaques de dénis de service (DDoS) [14].

L'ajout de protections logicielles permet de se prémunir contre ces attaques ou les rendre trop difficiles à réaliser. Toutefois, il faut pouvoir cibler les parties de code à sécuriser et garantir que l'application renforcée est robuste. Le déploiement de protections vise à protéger une fonctionnalité, les données sensibles manipulées, \(\ldots\) et dépend de l'application. La vérification de la robustesse d'une application, utile autant pour cibler le déploiement de protections que pour vérifier l'efficacité des protections déployées, nécessite de connaître la propriété de sécurité que l'on souhaite garantir. Dans le cadre de ce stage, on va s'intéresser à exprimer des propriétés de sécurité pour permettre l'évaluation de robustesse d'une application intégrant ou non des mécanismes de protection.

Les méthodes formelles offrent la possibilité de vérifier (complètement) le code (pour des systèmes de tailles moyennes). Ces méthodes sont généralement utilisées pour vérifier le fonctionnement des systèmes. Plus récemment, des approches émergent pour se concentrer sur les propriétés de sécurité des systèmes [4].

L'équipe ALSOC du LIP6 étudie depuis plusieurs années les effets d'attaques physiques sur des codes assembleur et s'appuie sur des méthodes formelles pour vérifier des contre-mesures, évaluer la robustesse de code contre ces attaques physiques. L'équipe developpe une plateforme de vérification au niveau assembleur RobustA [7].

Le stage a pour objectif d'explorer comment exprimer des propriétés de sécurité au niveau C/C++ et quel est le lien, du point de vu de la sécurité, entre le code C et sa version compilé. On souhaite déterminer comment se traduisent les propriétés de sécurité au niveau assembleur pour profiter de la plateforme RobustA. Cette étude se fera à travers trois études de cas: le code pin, comme exemple simple ; une fonctionnalité de FreeRTOS (http://www.freertos.org/) et une partie d'un "boot loader" seront étudiées .

Déroulement du stage envisagé

Étude bibliographique sur les propriétés de sécurités pour des codes bas niveaux.
Étude du code PIN et expression de propriétés au niveau C.
Étude du code assembleur et expression de propriétés.
Étudier le lien entre l'expression de la propriété au niveau C et au niveau assembleur.
Application sur une fonctionnalité de FreeRTOS et d'une partie d'un boot loader.

Pre-requis

Connaissance de la programmation C/C++/assembleur,
Notion de compilation
Connaissance en sécurité et des notions d'attaque bienvenues.

Encadrement

Cécile Braunstein et Karine Heydemann

Lieu

Laboratoire Informatique de Paris 6

Contact

cecile.braunstein@lip6.fr / karine.heydemann@lip6.fr

Rémunération

Indemnités de stage fixées par décret (environ 600 euros/mois)

References

[1]	H. Bar-El, H. Choukri, D. Naccache, M. Tunstall, and C. Whelan. The sorcerer's apprentice guide to fault attacks. Proc. of the IEEE, 94(2):370--382, feb 2006.
[2]	Cécile Braunstein, Anne E. Haxthausen, Wen-ling Huang, Felix Hübner, Jan Peleska, Uwe Schulze, and Linh Vu Hong. Complete model-based equivalence class testing for the ETCS ceiling speed monitor. In Stephan Merz and Jun Pang, editors, Formal Methods and Software Engineering, volume 8829, pages 380--395. Springer International Publishing, 2014. [ http ]
[3]	Bruce Schneier. The Internet of Things Will Turn Large-Scale Hacks into Real World Disasters, July 2016. [ http ]
[4]	Onur Demir, Wenjie Xiong, Faisal Zaghloul, and Jakub Szefer. Survey of approaches for security verification of hardware/software systems. IACR Cryptology ePrint Archive, 2016:846, 2016. [ .pdf ]
[5]	Peiyuan Dong, Yue Han, Xiaobo Guo, and Feng Xie. A Systematic Review of Studies on Cyber Physical System Security. International Journal of Security and Its Applications, 9(1):155--164, January 2015. [ DOI \| .pdf ]
[6]	Michael Felderer, Philipp Zech, Ruth Breu, Matthias Büchler, and Alexander Pretschner. Model-based security testing: a taxonomy and systematic classification: MODEL-BASED SECURITY TESTING. Software Testing, Verification and Reliability, 26(2):119--148, 2016. [ DOI \| http ]
[7]	Lucien Goubet, Karine Heydemann, Emmanuelle Encrenaz, and Ronald De Keulenaer. Efficient design and evaluation of countermeasures against fault attacks using formal verification. In Naofumi Homma and Marcel Medwed, editors, Smart Card Research and Advanced Applications, volume 9514, pages 177--192. Springer International Publishing, 2015. [ http ]
[8]	Wen-ling Huang and Jan Peleska. Complete model-based equivalence class testing. International Journal on Software Tools for Technology Transfer, 18(3):265--283, 2016. [ DOI \| http ]
[9]	Daniele Miorandi, Sabrina Sicari, Francesco De Pellegrini, and Imrich Chlamtac. Internet of things: Vision, applications and research challenges. Ad Hoc Networks, 10(7):1497--1516, September 2012. [ DOI \| http ]
[10]	Nicolas Moro. Sécurisation de programmes assembleur face aux attaques visant les processeurs embarqués, 2014. [ http ]
[11]	Nachiketh Potlapally. Hardware security in practice: Challenges and opportunities. In Hardware-Oriented Security and Trust (HOST), 2011 IEEE International Symposium on, pages 93--98. IEEE, 2011. [ http ]
[12]	Srivaths Ravi, Anand Raghunathan, Paul Kocher, and Sunil Hattangady. Security in embedded systems: Design challenges. ACM Transactions on Embedded Computing Systems (TECS), 3(3):461--491, 2004. [ http ]
[13]	Laszlo Szekeres, Mathias Payer, Lenx Tao Wei, and R. Sekar. Eternal war in memory. IEEE Security & Privacy, 12(3):45--53, 2014. [ DOI \| http ]
[14]	Nicky Woolf. DDoS attack that disrupted internet was largest of its kind in history, experts say. The Guardian, October 2016. [ http ]