ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Mon 8 Apr 2019 16:30 - 17:00 at SUN I - SAT Solving and Theorem Proving Chair(s): Armin Biere

Power side-channel attacks, which can deduce secret data via statistical analysis, have become a serious threat. Masking is an effective countermeasure for reducing the statistical dependence between secret data and side-channel information. However, designing masking algorithms is an error-prone process. In this paper, we propose a hybrid approach combing type inference and model-counting to verify masked arithmetic programs against side-channel attacks. The type inference allows an efficient, lightweight procedure to determine most observable variables whereas model-counting accounts for completeness. In case that the program is not perfectly masked, we also provide a method to quantify the security level of the program. We implement our methods in a tool QMVerif and evaluate it on cryptographic benchmarks. The experimental results show the effectiveness and efficiency of our approach.oach.

Mon 8 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:30 - 18:00
SAT Solving and Theorem ProvingTACAS at SUN I
Chair(s): Armin Biere Johannes Kepler University Linz
16:30
30m
Talk
Quantitative Verification of Masked Arithmetic Programs against Side-Channel Attacks
TACAS
Pengfei Gao , Hongyi Xie , Jun Zhang , Fu Song , Taolue Chen Birkbeck, University of London
Link to publication
17:00
30m
Talk
Incremental Analysis of Evolving Alloy Models
TACAS
Wenxi Wang The University of Texas at Austin, Texas, USA, Kaiyuan Wang Google, Inc., Milos Gligoric University of Texas at Austin, Sarfraz Khurshid University of Texas at Austin
Link to publication
17:30
30m
Talk
Extending a Brainiac Prover to Lambda-Free Higher-Order Logic
TACAS
Link to publication