SecChisel: Vérification de sécurité des architectures de processeurs sécurisés

Cette séance de cours présente le cadre SecChisel, qui vérifie les propriétés de sécurité des architectures de processeurs sécurisées au moment de la conception. Il couvre Chisel comme un langage de construction matérielle, le suivi de flux d'information, les réseaux de sécurité, les étiquettes de sécurité, FIRRTL, SMT-LIB, et l'évaluation en utilisant AES au sein d'une puce de Rocket RISC-V. Le cadre vise à détecter efficacement les fuites d'informations et les bogues matériels, sans ajouter de composants d'exécution.