Formally verifying a low-trust architecture

Problem

Low-trust architectures let software work on always-encrypted data, and they shrink the trusted hardware to a small, software-free enclave. The security claim must hold for every program and every implementation, which testing cannot show.

Idea

We define the security requirements at the ISA of the Sequestered Encryption (SE) architecture. Looking up, the ISA shows that no program built from these instructions can leak data, through direct disclosure or digital side channels. Looking down, the same ISA gives the proof obligations that any RTL implementation must discharge, and commercial formal tools discharge them.

Result

My role

Co-first author (equal contribution).

Paper: CCS 2023