线性码最优电路综合用于错误检测和纠正
Optimal Circuit Synthesis of Linear Codes for Error Detection and Correction
AI总结：
本文提出CiSC算法，通过SMT求解逐步减少输入和校验位大小，生成优于现有技术的线性码电路。
摘要：
故障注入攻击通过物理通道故意注入故障以干扰设备的正常执行。攻击者通过分析正常和故障输出推断秘密，对硬件实现的密码学原语构成严重威胁。为此，通过冗余（即并发错误检测方案）作为有效对策，二进制线性码已被用于防御故障注入攻击。然而，设计最优码电路往往耗时、易错且需要专业知识。本文基于输入和校验位大小的两个领域特定最小化目标，正式化了最优码电路综合问题（OptiCC）。我们提出了一种新颖的算法CiSC来解决OptiCC，优先最小化输入。我们的方法具有正确构造和安全构造特性。简而言之，CiSC通过SMT求解检查是否存在可行的布尔函数实现所需代码。我们进一步提出一种有效技术，懒惰地生成布尔函数的输入组合，同时快速识别等价的。我们实现了该方法的工具CiSC，并在实际基准上评估。实验结果表明，我们的方法能够生成显著优于最新最先进技术生成的码电路。
英文摘要：
Fault injection attacks deliberately inject faults into a device via physical channels to disturb its regular execution. Adversaries can effectively deduce secrets by analyzing both the normal and faulty outputs, posing serious threats to cryptographic primitives implemented in hardware. An effective countermeasure to such attacks is via redundancy, commonly referred to as concurrent error detection schemes, where Binary linear codes have been used to defend against fault injection attacks. However, designing an optimal code circuit is often time-consuming, error-prone, and requires substantial expertise. In this paper, we formalize the optimal code circuit synthesis problem (OptiCC) based on two domain-specific minimization objectives on individual inputs and parity size. We then propose a novel algorithm CiSC for solving OptiCC, prioritizing the minimization of individual inputs. Our approach features both correct-by-construction and secure-by-construction. In a nutshell, CiSC gradually reduces individual inputs and parity size by checking, via SMT solving, the existence of feasible Boolean functions for implementing a desired code. We further present an effective technique to lazily generate combinations of inputs to Boolean functions, while quickly identify equivalent ones. We implement our approach in a tool CiSC, and evaluate it on practical benchmarks. Experimental results show our approach can synthesize code circuits that significantly outperform those generated by the latest state-of-the-art techniques.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
