LeaSyn allows to automatically synthesize verified leakage contracts by combining a synthesis workflow that yields a precise yet possibly unsound contract with an iterative verification process.

Extending the SimBricks simulator framework to support the Gazebo physics simulator. This simulation is then used to spoof sensors and actuators of CPS allowing to simulate unmodified firmware.

A semi-automatic methodology for synthesizing hardware-software leakage contracts for open-source microarchitectures.

Introducing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts.

An approach to automatically infer hardware-software contracts for open-source processors.