Research Operations

Talks


[05 Minute]
[30 Minute]

Thesis

Specification mining can discover properties that can be used to verify
  • the secure behavior of closed source CISC CPU designs,
  • properties that can be used to verify the temporal correctness of CPU designs, and
  • hyperproperties that can be used to verify that modules, SoCs, and CPUs have secure information flow.

Plain English

Just as there are bugs in code that makes software, modern hardware is also written in code and therefore may contain bugs.

I find bugs in hardware.

Repos


[Aphrodite]
[Isadora][SoC]
[Astarte]
[Undine]
[Coppelia]

Papers