PV4 ⊧ Scam-V: Side Channel Abstract Model Validatorrandomly generates observationally equivalent inputs and checks their equivalenceA framework for the automatic validation of abstract observational models.
- Information flow analysis
- Side channel attacks
- Security verification
InternalsIt 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