Professor Song Fu’s research group from the School of Information Science and Technology (SIST) has recently published an article entitled “A Hybrid Approach to Formal Verification of Higher-Order Masked Arithmetic Programs”. This article was published in ACM Transactions on Software Engineering Methodology (ACM TOSEM), one of the two most prestigious software engineering journals in the world (the other one is IEEE Transactions on Software Engineering with IF 6.116, the fourth highest ranking among all IEEE computer journals in 2019). In the past three years (2017-2019), ACM TOSEM published an average of only 20 articles each year, and of those, only 3 on average listed their first affiliation as Mainland China.
Side-channel attacks, which are capable of breaking secrecy via side-channel information, pose a growing threat to the implementation of cryptographic algorithms. Masking is an effective countermeasure against side-channel attacks by removing the statistical dependence between secrecy and power consumption via randomization. However, designing efficient and effective masked implementations turns out to be an error-prone task. Current techniques for verifying whether masked programs are secure are limited in their applicability and accuracy, especially when they are applied. To bridge this gap, this article proposes a sound type system, equipped with an efficient type inference algorithm, for verifying masked arithmetic programs against higher-order attacks. It then gives novel model-counting based and pattern-matching based methods which are able to precisely determine whether the potential leaky observable sets detected by the type system are genuine or simply spurious (Figure 1). The evaluation of various implementations of arithmetic programs confirms that the approach outperforms the state-of-the-art baselines in terms of applicability, accuracy, and efficiency.
Figure 1 Framework of HOME
Following the national cyberspace security strategy, Professor Song Fu’s research group has conducted an in-depth study on this topic. This article is based on their prior achievements, including a novel refinement-based verification methodology for verifying cryptographic programs (ACM Transactions on Software Engineering Methodology, 2019) and a novel compositional type inference system (IEEE Transactions on Software Engineering, 2020).
In the article, Ph.D. Candidate Gao Pengfei is the first author, Professor Song Fu is the corresponding author, and ShanghaiTech University is the first affiliation. This article was supported by grants from the Natural Science Foundation of China Key Program, the NSFC-DFG International Joint Program, and the ShanghaiTech University’s Startup Funding.
Article links:
2020 ACM TOSEM:
http://faculty.sist.shanghaitech.edu.cn/faculty/songfu/publications/TOSEM20.pdf
2020 IEEE TSE:
https://ieeexplore.ieee.org/document/9139284
2019 ACM TOSEM:
https://dl.acm.org/doi/10.1145/3330392