Compilation sécurisée de primitives cryptographiques – scrypt

Nous utilisons des méthodes formelles qui ont le plus haut niveau de
confiance et s'appuie sur les assistant à la preuve (Coq et
Easycrypt). Ils servent à prouver les résultats mathématiques
nécessaire mais aussi à prouver l'absence de bugs de la chaîne de
compilation. Les compilateurs, issus de cette approche, que nous
utilisons et développons sont CompCert et Jasmin.

Nous avons fait l’état de l’art des canaux cachés liés au temps
d’exécution, en particulier les « cache timing attacks », ainsi que
les mécanismes d’effacement sécurisé. Nous avons evalué le potentiel
d’exploitabilité de ces canaux cachés pour des primitives
cryptographiques. Nous avons ensuite proposé des méthodes d’évaluation.

Nous avons proposé des modèles formelles pour capturer sémantiquement
la notion de canaux cachés et proposé des techniques de preuves pour
prouver la préservation de ces propriétés par compilation. Nous nous
sommes concentrés sur les propriétés d’effacement sécurisé [CSF2019] et
de « cryptographic constant-time » [POPL2020]. Nous avons notamment
prouvé formellement que le compilateur CompCert préserve la propriété
de cryptographic constant-time.

Nous avons développé un cadriciel de vérification pour
Jasmin, le langage de bas-niveau dédié à la programmation de
primitives cryptographiques. Nous utilisons EasyCrypt, l’assistant de
preuve que nous développons et dont les logiques de programmes peuvent
être réutilisées pour Jasmin. Ainsi, outre le développement d'une
bibliothèque formelle d'arithmétique modulaire, nous avons apporté
plusieurs extensions à EasyCrypt qui ont amélioré l’ergonomie de
l’assistant pour les preuves d’implémentations bas-niveau de
différentes primitives cryptographiques (CHACHA20, POLY1035, SHA3)
[S&P2020]. En particulier, pour SHA3, notre implémentation est la
première à atteindre simultanément les quatre propriétés souhaitées
qui sont l’efficacité, la correction fonctionnel, la sécurité
prouvable et la protection contre les canaux auxiliaires [CCS2019].

Le travail est en cours pour prouver que le compilateur Jasmin preserve constant-time.
Comme il s’appuie sur un modèle sémantique différent; cela requiert de repenser les techniques de preuve. Nous
travaillons aussi à adapter CompCert afin de préserver des propriétés
d’effacement sécurisé. Dans cas, il est nécessaire de modifier le
compilateur et donc d’adapter les preuves de correction fonctionnel
avant de s’attaquer à la preuve de sécurité.


Nous continuons à étendre le langage Jasmin et son compilateur en
ajoutant des fonctionnalités nécessaires pour implémenter des
algorithmes plus complexes. Ces extensions ont des conséquences
notables sur le compilateur (notamment pour l’allocation de registres)
et donc sur sa preuve de correction. Un exemple de primitive qui
nécessite ces extensions est le schéma de cryptage post-quantique
Kyber.

[POPL2020] Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie and Alix Trieu. Formal verification of a constant-time preserving C compiler. PACMPL, 4(POPL). 2020.

[CCS2019] José Bacelar Almeida, Cecile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton and Pierre-Yves Strub. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS 2019. ACM. hal.inria.fr/hal-02404581v1

[S&P2020] José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub. The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. accepted S&P 2020. IEEE.

[CSF2019] Frédéric Besson, Alexandre Dang, Thomas P. Jensen: Information-Flow Preservation in Compiler Optimisations. CSF 2019. IEEE.

De robustes primitives cryptographiques sont essentielles pour assurer la
sécurité des communications. La sécurité est relative à un modèle d'attaquant
qui évolue avec le contexte technologique. La cryptographie à base de courbes
elliptiques (ECC) est une alternative à la cryptographie symétrique, p. ex. RSA,
qui a des avantages pour des appareils contraints en ressources comme les
téléphones mobiles ou les cartes à puce. Dans ce cas, la résistance mathématique
des algorithmes cryptographiques n'est pas suffisante car l'attaquant, qui a un
accès physique à l'appareil, peut espionner l'exécution de la primitive
cryptographique et en déduire la clé secrète par le biais de canaux cachés.

L'objectif du projet est de développer une chaîne de compilation sécurisée qui
assure, à l'aide de méthodes formelles, la sécurité des primitives
cryptographiques depuis le code source jusqu'au binaire. Notre but est de
prouver l'absence d'erreurs de programmation mais aussi d'assurer que des
contre-mesures de sécurité sont bien présentes dans le binaire et réduisent
sûrement et efficacement le potentiel des attaques par canaux cachés qui sont
d'habitude ignorés par un modèle idéalisé. Le défi est de générer des codes
cryptographiques qui soient à la fois sûre par construction mais aussi conformes
à de strictes exigences d'efficacité.

Pour l'efficacité, notre approche consiste à concevoir un language de bas-niveau
dédié aux cryptographes qui ont besoin d'avoir un contrôle fin sur l'exécution
du programme. Pour la sécurité, notre approche est basée sur la preuve mécanisée
dont la base de confiance se réduit au noyau logique d'un assistant de preuve.
Notre chaîne de compilation va utiliser la technologie de la compilation
certifiée où le compilateur est à la fois programmé et prouvé à l'intérieur de
l'assistant de preuve Coq. Notre infrastructure de preuve contiendra des outils
de vérification déductive pour prouver la correction fonctionnelle de primitives
cryptographiques optimisées et des transformations de programme pour insérer des
contre-mesures aux canaux cachés. Un trait distinctif de notre compilateur est
qu'il garantit que le binaire hérite du source sa même robustesse vis à vis des
canaux cachés.

Le projet est focalisé sur la conception et la mise en œuvre de notre chaîne de
compilation qui un résultat majeur du projet. L'évaluation pratique est aussi un
objectif. Pour les primitives cryptographiques, nous visons la cryptographie à
base de courbes elliptiques (EEC) dont la mise en œuvre correcte et efficace est
difficile tant du fait des mathématiques mises en jeu que des détails
d'implantation. Un résultat attendu du projet est une bibliothèque ECC vérifiée
qui soit compétitive avec bibliothèque non-vérifiée de l'état de l'art. Du
point de vue canaux cachés, nous mettrons l'accent sur les attaques temporelles
et à base de consommation d'énergie en améliorant des contre-mesures bien
établies que sont le masquage et la discipline de programmation en temps constant.

Les bonnes pratiques recommandent soit de programmer les primitives
cryptographiques directement en assembleur, soit d'inspecter manuellement le
code produit. C'est à la fois chronophage et sujet à erreurs. De plus, il n'est
pas possible d'assurer à un tiers que le code est sûr. Notre chaîne de
compilation assure automatiquement que le code des primitives cryptographiques
est sûr. De plus, cette sécurité (par construction) est vérifiable. Ceci est
particulièrement important pour des bibliothèques cryptographiques Open Source.