Path-specific Information Flow Analysis for RSA Hardware Timing Channel Security Verification

The RSA algorithm is widely used for data encryption and digital signature, which may suffer from timing channel information leakage. Hardware information flow analysis are proposed to identify timing channel vulnerabilities, but the timing channel verification and detection are time-consuming and resource-intensive due to the huge scale and complexity for existing information flow models. In this work, we propose a path-specific information flow analysis method for RSA hardware timing channel security verification. It reduces the verification complexity of the information flow model by extracting the shortest physical path and generating the information flow model for the extracted specific path. We finally perform formal security verification and simulate the counterexample to identify timing channels. Experimental results demonstrate that the proposed method accelerates formal security verification and detects timing channel vulnerabilities in RSA effectively.