Optimal Circuit Synthesis of Linear Codes for Error Detection and Correction

TL;DR

This paper introduces an optimal circuit synthesis method for linear codes used in error detection and correction, improving efficiency and security against fault injection attacks.

Contribution

It formalizes the OptiCC problem and proposes the CiSC algorithm, enabling secure and correct code circuit synthesis with better performance than existing methods.

Findings

CiSC outperforms state-of-the-art techniques in benchmark tests.

The approach reduces individual inputs and parity size effectively.

Experimental results demonstrate improved synthesis efficiency.

Abstract

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.