Masking is a countermeasure against Power Side Channel Attacks (PSCAs) in both software and hardware implementations of cryptographic algorithms. Compared to software masking, implementing masked hardware is time consuming and error prone. Recent approaches, therefore, rely on High Level Synthesis (HLS) tools to automatically generate masked Register Transfer Level (RTL) hardware from verified masked software, significantly reducing design effort. Since HLS was never developed for security, HLS optimizations may impact PSCA security of the generated RTL. As a result, verifying the PSCA security of HLS generated masked RTL is crucial. Existing hardware masking verification tools can verify masked hardware, but may produce false positives when applied to HLS generated designs with controller datapath architectures obtained due to resource-shared datapath obtained via HLS. This work proposes a hardware masking verification strategy for HLS generated masked hardware. Our toolflow MaskedHLSVerif, performs state-wise formal verification of controller datapath RTL obtained via HLS, thereby avoiding false positives caused by resource-shared datapaths. Our tool flow correctly verifies standard cryptographic benchmarks, consisting of cascaded masked gadgets and the PRESENT S-box masked with gadgets, where existing tools like REBECCA reports false positives. The proposed tool-flow is able to detect masking flaws induced by HLS-optimizations as well.

翻译：掩蔽是一种针对密码算法在软件和硬件实现中抵御功耗侧信道攻击（PSCA）的对抗措施。与软件掩蔽相比，实现掩蔽硬件耗时且易出错。因此，近期方法依赖高层综合（HLS）工具从经过验证的掩蔽软件自动生成掩蔽寄存器传输级（RTL）硬件，显著减少了设计工作量。由于HLS并非为安全性而开发，其优化可能影响生成RTL的PSCA安全性。因此，验证HLS生成的掩蔽RTL的PSCA安全性至关重要。现有硬件掩蔽验证工具可验证掩蔽硬件，但应用于经HLS生成、具有控制器数据路径架构（由HLS资源共享数据路径产生）的设计时，可能产生误报。本文提出一种针对HLS生成掩蔽硬件的掩蔽验证策略。我们的工具流程MaskedHLSVerif对经HLS获得的控制器数据路径RTL进行逐状态形式化验证，从而避免由资源共享数据路径引起的误报。该工具流程能正确验证标准密码基准测试（包括级联掩蔽门件及带掩蔽门件的PRESENT S盒），而REBECCA等现有工具会报告误报。所提出的工具流程还能够检测由HLS优化引入的掩蔽缺陷。