QMVerif

Our new tool which is based on compositional verification is coming soon...

QMVerif is a tool focusing on the verification of masked arithmetic programs against power side-channel attack. Please see our paper Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks for more details.

Download

Download QMVerif. The extracting password will be released after the publication of the journal version of the paper.

Build

mkdir build
cd build
cmake ..
make

Usage

Examples

Command of perfect masking verification of CHES10 multiplication order1 in default setting (no simpification, using Z3 if needs model counting)

QMVerif -p ../examples/CHES10_multiplication_order1.ec

Command of perfect masking verification and QMS computation of cube_order1.ec (no simpification, using brute-force if needs model counting)

QMVerif -p ../examples/cube_order1.ec -bf -qms