COSIC seminar – Sanctum: Towards an Open-Source, Formally-Verified Secure Processor

COSIC seminar – Sanctum: Towards an Open-Source, Formally-Verified Secure Processor – Srini Devadas (Massachusetts Institute of Technology)

Architectural isolation can be used to secure computation on a remote secure processor with a private key where the privileged software is potentially malicious as recently deployed by Intel’s Software Guard Extensions (SGX). This talk will describe the Sanctum secure processor architecture, which offers the same promise as SGX, namely strong provable isolation of software modules running concurrently and sharing resources, but protects against an important class of additional software attacks that infer private information by exploiting resource sharing. We will also briefly describe a verification methodology based on a trusted abstract platform (TAP) that formally models idealized enclaves and a parameterized adversary.

Joint work with Victor Costan, Ilia Lebedev, and the Seshia Group at U. C. Berkeley.