Séance de cours

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

Graph Chat

Chattez avec Graph Search

Posez n’importe quelle question sur les cours, conférences, exercices, recherches, actualités, etc. de l’EPFL ou essayez les exemples de questions ci-dessous.

AVERTISSEMENT : Le chatbot Graph n'est pas programmé pour fournir des réponses explicites ou catégoriques à vos questions. Il transforme plutôt vos questions en demandes API qui sont distribuées aux différents services informatiques officiellement administrés par l'EPFL. Son but est uniquement de collecter et de recommander des références pertinentes à des contenus que vous pouvez explorer pour vous aider à répondre à vos questions.

Description

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.

Source officielle

Concepts associés (22)

Chisel

Chisel est un langage informatique open-source de description matériel basé sur Scala. Chisel, pour en, permet de décrire des circuits électroniques numériques au niveau du transfert de registres (RTL). Chisel hérite des propriétés objet et fonctionnel de Scala pour décrire du matériel. L'utilisation de Scala comme base permet de se servir de Chisel comme un générateur de circuits électroniques. Il existe également TL-Chisel, l'équivalent en Chisel de TL-Verilog (Transaction-Level Verilog).

Vérification formelle

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. Formal verification can be helpful in proving the correctness of systems such as: cryptographic protocols, combinational circuits, digital circuits with internal memory, and software expressed as source code.

Processeur à jeu d'instructions réduit

Un processeur à jeu d'instructions réduit (en anglais RISC pour Reduced instruction set computer) est un type d'architecture de processeur qui se caractérise par un jeu d'instructions visant la rapidité d'exécution grâce à la facilité de décodage et d'exécution en pipeline des instructions machine. À la fin des années 1980 et au début des années 1990, cette stratégie permet aux microprocesseurs RISC d'obtenir de meilleures performances que les architectures anciennes, de type CISC (de l'anglais complex instruction-set computer).

Conception assistée par ordinateur pour l'électronique

La CAO électronique (pour Conception assistée par ordinateur électronique), nommée également en anglais EDA (pour Electronic design automation), est la catégorie des outils servant à la conception et la production des systèmes électroniques allant des circuits imprimés jusqu'aux circuits intégrés. Le terme CAO est aussi utilisé pour désigner la CAO mécanique, la conception assistée par ordinateur et la fabrication assistée par ordinateur en électronique et en électrotechnique.

Functional verification

Functional verification is the task of verifying that the logic design conforms to specification. Functional verification attempts to answer the question "Does this proposed design do what is intended?" This is complex and takes the majority of time and effort (up to 70% of design and development time) in most large electronic system design projects. Functional verification is a part of more encompassing design verification, which, besides functional verification, considers non-functional aspects like timing, layout and power.

Afficher plus

Séances de cours associées (7)

Chiffrement homomorphe

Introduit le cryptage homomorphe, permettant le calcul sur des données cryptées sans décryptage, couvrant la sécurité, les applications et les aspects pratiques.

Chiffrement homomorphe

Couvre le développement historique et les concepts clés du cryptage homomorphe, en se concentrant sur le cryptosystème Paillier et le cryptosystème BGV.

Vérification basée sur la simulation

Explore la vérification basée sur la simulation dans les systèmes VLSI à l'aide d'algorithmes basés sur le code compilé et les événements.

Vérification du matériel en utilisant des langages de conception de haut niveau

Explore les défis en matière de vérification matérielle, de spécifications claires, de dommages spéculatifs et de sémantique précise du cycle.

Introduction à la conception avancée VLSI

Couvre les concepts avancés de conception VLSI, y compris la conception personnalisée complète et l'ajout de préfixes parallèles.

Afficher plus

Concepts associés (22)

Chisel

Vérification formelle

Processeur à jeu d'instructions réduit

Conception assistée par ordinateur pour l'électronique

Functional verification

Afficher plus