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

• Information flow analysis
• Side channel attacks
• Security verification

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:

• Works for small programs
• Cannot handle certain cases such as memory dependent observations