QMVerif

!!! We have open-sourced this tool on Github.

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

• use -p to describe the path of the program which needs to be verifid
• if you want to compute the QMS value, please add -qms parameter. Otherwise, the tool only conduct the perfect masking checking.
• if you need the simplification, please add -sim parameter
• if you want to use brute-force based approach, please add -bf. Otherwise, the SMT-based approach will be invoked.
• if you want to provide some oracle, please add -oracle.
• Adding -hd can verify the program based on the Hamming Distance model.

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