Thomas Letan

PhD Student in Computer Science

Introducing SpecCert

Over time, hardware designs have constantly grown in complexity and modern platforms involve multiple interconnected hardware components. From a security point of view, this brings two issues. Firstly, during the last decade, several vulnerability disclosures have proven that trust in hardware can be misplaced. Secondly, software developers have to struggle with hundreds of pages of specifications divided into dozens of documents.

SpecCert is an attempt to tackle this two challenges. SpecCert is a framework to specify what we have called “Hardware-based Security Enforcement (HSE) mechansims”. As part of such a mechanism, a trusted software component configures the hardware platform so that untrusted software components cannot violate a security property. For instance, in order to enforce applications isolation, an operating system (which is the trusted software components in this scenario) partly relies on the memory paging mechanisms and user/supervisor execution contexts of modern CPUs.

By formally specifying a HSE mechanism, we gain two benefits. Firstly, we can verify our definition brings the desired security property according to our model. Secondly, we provide an unambiguous specification to any software developer interested in actually implemented the HSE mechanism.

SpecCert is still a work in progress. I have implemented and published a first proof of concept on Github. The project is written in Gallina using the Coq proof-assistant. If you are interested in the subject, feel free to have a look. You can also read our paper to have a more-in-depth description of the formalism..