Lecture

SecChisel: Security Verification of Secure Processor Architectures

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

Description

This lecture introduces the SecChisel framework, which verifies security properties of secure processor architectures at design-time. It covers Chisel as a hardware construction language, information flow tracking, security lattices, security tags, FIRRTL, SMT-LIB, and evaluation using AES within a RISC-V Rocket Chip. The framework aims to detect information leaks and hardware bugs efficiently, without adding runtime components.

Official source

Related concepts (22)

Chisel (programming language)

The Constructing Hardware in a Scala Embedded Language (Chisel) is an open-source hardware description language (HDL) used to describe digital electronics and circuits at the register-transfer level. Chisel is based on Scala as an embedded domain-specific language (DSL). Chisel inherits the object-oriented and functional programming aspects of Scala for describing digital hardware. Using Scala as a basis allows describing circuit generators. High quality, free access documentation exists in several languages.

Formal verification

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.

Reduced instruction set computer

In computer engineering, a reduced instruction set computer (RISC) is a computer architecture designed to simplify the individual instructions given to the computer to accomplish tasks. Compared to the instructions given to a complex instruction set computer (CISC), a RISC computer might require more instructions (more code) in order to accomplish a task because the individual instructions are written in simpler code.

Electronic design automation

Electronic design automation (EDA), also referred to as electronic computer-aided design (ECAD), is a category of software tools for designing electronic systems such as integrated circuits and printed circuit boards. The tools work together in a design flow that chip designers use to design and analyze entire semiconductor chips. Since a modern semiconductor chip can have billions of components, EDA tools are essential for their design; this article in particular describes EDA specifically with respect to integrated circuits (ICs).

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.

Related lectures (7)

Homomorphic Encryption

Introduces homomorphic encryption, enabling computation on encrypted data without decryption, covering security, applications, and practical aspects.

Homomorphic Encryption

Covers the historical development and key concepts of homomorphic encryption, focusing on the Paillier cryptosystem and the BGV cryptosystem.

Simulation-Based Verification

Explores simulation-based verification in VLSI systems using compiled-code and event-driven algorithms.

Hardware Verification using High-Level Design Languages

Explores challenges in hardware verification, clear specifications, speculation harm, and cycle-precise semantics.

Introduction to Advanced VLSI Design