量子科技中心_量科网

对密码算法中功耗侧信道泄漏及其防护措施进行形式化验证极具挑战性，因为基于SAT的方法在包含大量XOR运算、时间展开且采用真实泄漏模型的密码电路上难以扩展。该团队构建了紧凑的合取范式（CNF）案例，用于建模两条迹线条件下的单比特泄漏，将密钥依赖性与状态演化联系起来。经典求解器很快达到复杂度极限，因此提出Q-LEAK方法，这是一种基于Grover算法的量子验证方法，将每个CNF编译成预言机，并应用振幅放大在O(sqrt(N))次预言机调用内进行搜索，其中预言机编码了两迹线泄漏谓词和CNF约束条件。与经典SAT的基准测试显示了潜在优势与实际资源限制。在5-7变量基准的无噪声测试中，Q-LEAK在1-4次尝试内一致地恢复了满足性赋值，标记的比特串明显高于背景分布，概率超过20%。在真实量子硬件上对Q-LEAK的评估显示，尽管存在噪声，但至少发现了一个经经典验证的SAT赋值。这些结果表明，存在一条通往量子辅助验证侧信道防护措施的潜在路径。