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 QMVerif. The extracting password will be released after the publication of the journal version of the paper.
mkdir build cd build cmake .. make
-pto describe the path of the program which needs to be verifid
- if you want to compute the QMS value, please add
-qmsparameter. Otherwise, the tool only conduct the perfect masking checking.
- if you need the simplification, please add
- 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
-hdcan verify the program based on the Hamming Distance model.
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