PV1 ⊧ SCInferdetermines whether nodes of a cryptographic program are perfectly masked

A tool to verify masking countermeasures.

Application domain/field

• Side channel attacks
• Security verification
• Power side-channel leaks
• Cryptographic algorithms

Expected input

• Program $P$
• Sets of public $p$
• Secret $k$
• Random $r$ variables
• Empty map $\pi$

Expected output

The map indicates per node (in the data dependency graph (DDG) of the program) whether it is perfectly masked (SID), not perfectly masked (NPM) or unknown (UKD).

Internals

Uses Z3.