Un langage de conception matériel pour la sécurité des flux d'information sensibles au timing

La sécurité de l'information peut être compromise par des fuites via des caractéristiques matérielles de bas niveau. Un exemple récemment prominent est les attaques de probing de cache, qui s'appuient sur des canaux temporels créés par les caches. Nous introduisons un langage de conception matériel, SecVerilog, qui permet d'analyser statiquement le flux d'information au niveau matériel. Avec SecVerilog, des systèmes peuvent être construits avec un contrôle vérifiable des canaux temporels et d'autres canaux d'information. SecVerilog est Verilog, étendu avec des annotations de type expressives qui permettent un raisonnement précis sur le flux d'information. Il est également accompagné d'une assurance formelle rigoureuse : nous prouvons que SecVerilog impose une non-interférence sensible au timing et assure ainsi un flux d'information sécurisé. En construisant un processeur MIPS sécurisé et ses caches, nous démontrons que SecVerilog rend possible la construction de conceptions matérielles complexes avec une sécurité vérifiée, tout en ayant un faible surcoût en temps, en espace et en effort pour le concepteur matériel.