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

Program?

Format:

HOL?

Internals

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

Links

Last commit date

2 August 2021 (the scamv subdirectory in the repository has last been updated on 4 February 2021)

Related papers

https://doi.org/10.1007/978-3-030-53288-8_12

Last publication date

14 July 2020

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.