高阶掩码算术程序形式化验证的混合方法
密码学与安全
2020-06-17 v1 软件工程
摘要
能够通过侧信道信息破坏机密性的侧信道攻击，对密码算法实现构成日益增长的威胁。掩码通过随机化消除机密性与功耗之间的统计依赖，是针对侧信道攻击的一种有效对策。然而，设计高效且有效的掩码实现是一项易出错的任务。当前用于验证掩码程序是否安全的技术在适用性与准确性上有限，尤其在应用时。为弥补此差距，本文中我们首先提出一个可靠的类型系统，配备高效的类型推断算法，用于针对高阶攻击验证掩码算术程序。随后我们给出基于模型计数与基于模式匹配的新方法，能够精确判定类型系统检测到的潜在泄露可观测集是真实的还是虚假的。我们在各类算术密码程序实现上评估了我们的方法。实验证实，我们的方法在适用性、准确性与效率方面优于最先进的基线。
引用
@article{arxiv.2006.09171,
title = {A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs},
author = {Pengfei Gao and Hongyi Xie and Fu Song and Taolue Chen},
journal= {arXiv preprint arXiv:2006.09171},
year = {2020}
}