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

tacas-2019-papers
16:30 - 18:00: TACAS 2019 - SAT Solving and Theorem Proving at SUN I
Chair(s): Armin BiereJohannes Kepler University Linz
tacas-2019-papers16:30 - 17:00
Talk
Pengfei Gao, Hongyi Xie, Jun Zhang, Fu Song, Taolue ChenBirkbeck, University of London
Link to publication
tacas-2019-papers17:00 - 17:30
Talk
Wenxi WangThe University of Texas at Austin, Texas, USA, Kaiyuan WangGoogle, Inc., Milos GligoricUniversity of Texas at Austin, Sarfraz KhurshidUniversity of Texas at Austin
Link to publication
tacas-2019-papers17:30 - 18:00
Talk
Link to publication