SecChisel Framework for Security Verification of Secure Processor Architectures

By Shuwen Deng, Doguhan Gümüsoglu, Wenjie Xiong, Sercan Sari, Y. S. Gener, Corine Lu, O. Demir, Jakub Szefer. 2019

16 citations recorded by the source corpus.

This work presents a design-time security verification framework for secure processor architectures. Our new SecChisel framework is built upon the Chisel hardware construction language and tools, and uses information flow analysis to verify the security properties of an architecture at design-time. To enforce information flow security, the framework supports adding security tags to wires, registers, modules, and other parts of the design description, as well as allows for defining a custom security lattice and custom information flow policies. The framework performs automatic security tag propagation analysis in a new SecChisel parser and information flow checking using the Z3 SMT solver. The same SecChisel codebase is used to design hardware modules as well as to verify the security properties, ensuring that the verified design directly corresponds to the actual design. This framework is evaluated on RISC-V Rocket Chip expanded with AES and SHA modules. The framework was able to capture information leaks in the hardware bugs or Trojans that it was tested with.

Subfields: Artificial Intelligence, Hardware and Architecture, Privacy & Security, Signal Processing

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

  1. Brendan Dolan-Gavitt
  2. Benjamin Tan
  3. Ramesh Karri
  4. Baleegh Ahmad
  5. Hammond A. Pearce
  6. Aleksander Madry

In Hardware and Architecture

  1. Brendan Dolan-Gavitt
  2. Ramesh Karri

In Privacy & Security

  1. Ramesh Karri

In Signal Processing

  1. Brendan Dolan-Gavitt
  2. Ramesh Karri
  3. Aleksander Madry

Citations in the corpus