Étude de la crypto-agilité de OpenSSL et du test automatisé de systèmes non déterministes

Ce mémoire propose une approche destinée à relever les défis liés au test des systèmes non déterministes, dont les comportements imprévisibles peuvent résulter du temps d’exécution, de la concurrence ou de l’utilisation d’entrées aléatoires. Il s’intéresse également à l’analyse approfondie de la structure logicielle d’OpenSSL, principale bibliothèque cryptographique libre, ainsi qu’à celle de son fournisseur d’algorithmes post-quantiques: Open Quantum Safe (OQS). Une première phase est consacrée aux fondements théoriques : la cryptographie classique et post-quantique, la crypto-agilité et les méthodes de génération de tests. Sur cette base, la première contribution repose sur l’utilisation des tests basés sur les modèles, associés à des méthodes formelles, afin d’assurer une couverture de test systématique. L’outil ProB, vérificateur de modèles pour la méthode B, est employé pour analyser un modèle formel du système ciblé et générer automatiquement des scénarios de test. Cette méthodologie est appliquée au protocole TLS 1.3, norme cryptographique complexe et largement utilisée, en ciblant une implémentation via l’API Java BouncyCastle pour OpenSSL. Bien que TLS repose sur des mécanismes majoritairement déterministes, il intègre des éléments non déterministes---tels que la négociation dynamique d’algorithmes ou la génération de valeurs aléatoires---qui en font un environnement expérimental pertinent pour évaluer l’efficacité du test à base de modèle. La seconde contribution s’inscrit dans le contexte de la transition vers la cryptographie post-quantique, engagée par l'Institut national des normes et de la technologie depuis 2016 pour remplacer les primitives vulnérables aux attaques quantiques. L’intégration de ces nouveaux algorithmes dans TLS soulève des enjeux techniques significatifs, touchant autant l’architecture logicielle que l’implémentation. L’étude met en évidence, par rétro-ingénierie, les contraintes imposées par les structures héritées en C d’OpenSSL, qui freinent la crypto-agilité et compliquent la maintenance, en comparaison avec l’architecture modulaire d’OQS fondée sur le concept de fournisseurs. En combinant les méthodes formelles, l’analyse des comportements non déterministes et l’exploration d’architectures logicielles modernes pour la cryptographie post-quantique, ce travail souligne la nécessité de cadres de test et de développement plus flexibles, fiables et adaptés aux exigences croissantes de la cybersécurité.

Name thesis:degree_name

M. Sc.

Level thesis:degree_level

Maîtrise

Discipline thesis:degree_discipline

Génie informatique

Grantor dc:publisher

Université de Sherbrooke

Year dc:date.issued

2025

Author dc:creator

• Onofrei, Alexander

Advisor dc:contributor.advisor

• Frappier, Marc

• Cryptographie post-quantique
• Cryptoagilité
• TLS
• OpenSSL
• ProB
• Langage B
• Tests à base de modèles
• Systèmes non déterministes

Licence dc:rights.uri

• http://creativecommons.org/licenses/by/4.0/

Language dc:language.iso

fr, en

DOI

https://doi.org/10.71892/11143/1238

OAI identifier oai:identifier

oai:usherbrooke.scholaris.ca:11143/23648