Attaque et sécurisation d'un schéma d'attestation à distance vérifié formellement — Benoît Morgan, Jonathan Certes
Date : 02 June 2022 à 10:00 — 30 min.
Dans le cadre de l'attestation à distance sur microprocesseurs ARM, nous émettons l'hypothèse qu'un adversaire, privilégié mais distant, ne peut reproduire la trace d'exécution de notre algorithme de confiance optimisé. Compte-tenu de cette hypothèse, du support matériel garantit la sécurité d'une architecture de vérification de l'intégrité d'environnement d'exécution.
Nous validons notre hypothèse en auditant notre système, au travers d'attaques de bas niveau, en tentant de reproduire les signaux d'accès sans exécuter notre algorithme de confiance. Sous réserve que notre algorithme de confiance respecte certaines contraintes liées à l'architecture matérielle du microprocesseur, nous montrons que nous pouvons accorder un fort degré de confiance en notre hypothèse.