PV4 Scam-V: Side Channel Abstract Model Validatorrandomly generates observationally equivalent inputs and checks their equivalence

A framework for the automatic validation of abstract observational models.

Application domain/field

Expected input





It has been implemented in the HOL4 theorem prover. It is embedded in HolBA. Scam-V attempts to construct pairs of initial states such that runs of the binary from these states are indistinguishable at the level of the hardware, but distinguishable on the real hardware. According to the repository, Scam-V:
Binary level


Related papers

Validation of Abstract Side-Channel Models for Computer Architectures

Last publication date

14 July 2020

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.