Vérification Formelle de La Primitive

**Type de contrat **:CDD

**Niveau de diplôme exigé **:Bac + 5 ou équivalent

**Fonction **:Ingénieur scientifique contractuel

**Contexte et atouts du poste**:
La sécurité de la cryptographie usuelle repose sur des problèmes mathématiques réputés difficiles à résoudre: trouver
un logarithme discret (DLOG), ou décomposer de grands nombres en facteurs premiers (FACT). Toutefois, cette cryptographie
est menacée par une percée technologique: l'ordinateur quantique. En effet, les opérations élémentaires des ordinateurs
classique et quantique étant de natures différentes, elles rendent ce dernier capable de résoudre efficacement les
problèmes DLOG et FACT. Cette menace a fait s'intéresser les chercheurs à des alternatives pouvant lui résister, donnant
lieu à plusieurs nouveaux algorithmes actuellement en voie de standardisation.

Néanmoins, bien que les algorithmes cryptographiques aient été étudiés extensivement d'un point de vue théorique,
obtenir des implémentations correctes et efficaces a été historiquement difficile : par exemple, la librairie OpenSSL,
une des librairies cryptographiques les plus utilisées actuellement, reporte régulièrement des vulnérabilités liées
à des erreurs d'implementation. Dans certains cas, ces vulnérabilités peuvent mener à différentes attaques par déni de
service, ou à la fuite d'informations confidentielles, avec des conséquences désastreuses pour la protection de la
vie privée.

En raison de leur aspect critique et de leur complexité, les implémentations cryptographiques bénéficient tout
particulièrement des garanties apportées par la vérification formelle. Contrairement à des techniques de test
traditionnelles, la vérification formelle analyse tous les chemins d'exécution possibles d'un programme, et
permet donc de garantir statiquement l'absence de certaines classes d'attaques et d'erreurs. Différents projets
récents, tels que HACL*, Fiat-Crypto, ou Jasmin, ont démontré son utilité pour obtenir des garanties de sûreté
mémoire, de correction fonctionnelle, et de résistance face à certaines formes d'attaques par canaux cachés
pour des implémentations efficaces de primitives cryptographiques.

**Mission confiée**:
Nous proposons d'étendre ces travaux à la cryptographie post-quantique, en ciblant particulièrement la
signature cryptographique Falcon. La mission principale de ce travail sera l'implémentation et la
vérification en Rust d'une version optimisée de Falcon, en utilisant la toolchain Circus co-dévelopée
par l'équipe Prosecco pour traduire le code Rust vers différents assistants de preuve, tels que F*
ou Lean afin d'établir des preuves formelles de la sûreté et de la correction de l'implémentation.
Dans le cadre de ce projet, l'ingénieur sera également amené à interagir avec les développeurs
actuels de la toolchain Circus, et de ses sous-composants hacspec et Aeneas, ainsi qu'à proposer
et implémenter des améliorations et extensions des outils utilisés.

**Principales activités**:

- Développement d'une implémentation de Falcon en Rust
- Ecriture et test d'une spécification formelle de la primitive Falcon en hacspec
- Vérification formelle à l'aide d'un assistant de preuves (F*/Lean) de la sûreté et correction de l'implémentation Rust
- Interaction avec les développeurs de CIRCUS, et extension de la toolchain si nécessaire lors de l'implémentation de Falcon

**Compétences**:
Compétences techniques et niveau requis:

- Familiarité avec les outils de preuve formelle, et particulièrement avec F* et/ou Lean
- Programmation Rust
- Connaissances théoriques en cryptographie post-quantique

Langues : français et anglais

**Avantages**:

- Restauration subventionnée
- Transports publics remboursés partiellement
- Congés: 7 semaines de congés annuels + 10 jours de RTT (base temps plein) + possibilité d'autorisations d'absence exceptionnelle (ex : enfants malades, déménagement)
- Possibilité de télétravail
- Aménagement du temps de travail (après 6 mois d'ancienneté)
- Équipements professionnels à disposition (visioconférence, prêts de matériels informatiques, etc.)
- Prestations sociales, culturelles et sportives (Association de gestion des œuvres sociales d'Inria)
- Accès à la formation professionnelle
- Sécurité sociale