Mediaspace scheduled maintenance: Aug 25, 2026 07:00 - 12:00 AM. During this time, videos will be temporarily unavailable. Check status updates.

Lecture

SecChisel: Security Verification of Secure Processor Architectures

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.

This video is available exclusively on Mediaspace for a restricted audience. Please log in to MediaSpace to access it if you have the necessary permissions.

Watch on Mediaspace

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.

ARM architecture family

ARM (stylised in lowercase as arm, formerly an acronym for Advanced RISC Machines and originally Acorn RISC Machine) is a family of reduced instruction set computer (RISC) instruction set architectures for computer processors, configured for various environments. Arm Ltd. develops the architectures and licenses them to other companies, who design their own products that implement one or more of those architectures, including system on a chip (SoC) and system on module (SOM) designs, that incorporate different components such as memory, interfaces, and radios.

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).

Related lectures (7)

Homomorphic Encryption Log in to Mediaspace to watch this video

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

Hardware Verification using High-Level Design Languages Log in to Mediaspace to watch this video

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

Homomorphic Encryption Log in to Mediaspace to watch this video

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

X86 and ARM: Processors Evolution and Microarchitectures Log in to Mediaspace to watch this video

Explores the evolution and microarchitectures of x86 and ARM processors, from early designs to modern advancements.

Simulation-Based Verification Log in to Mediaspace to watch this video