Vérification de la sécurité à travers le matériel et les logiciels

Cette séance de cours couvre la vérification de la sécurité à travers le matériel et les logiciels, y compris les algorithmes vérifiés comme SSL, TLS et SHA utilisés dans les principaux systèmes, ainsi que les techniques pour éliminer automatiquement les fuites spéculatives et vérifier les programmes distribués. Il traite également de l'application de l'iode pour vérifier le temps constant pour le matériel, attraper des attaques de chronométrage via coloriage, et l'utilisation de Blade pour corriger les bogues spéculatifs dans le logiciel. L'instructeur présente des points de repère, des hypothèses et des défis dans la vérification du temps constant pour le matériel, soulignant l'importance de faire des hypothèses sur le matériel explicite pour éviter les bogues dans les logiciels vérifiés.