#SAT-based vulnerability analysis of security components — A case study

In this paper we describe a new approach to assess a circuit´s vulnerability to fault attacks. This is achieved through analysis of the circuit´s design specification, making use of modern SAT solving techniques. For each injectable fault, a corresponding SAT instance is generated. Every satisfying solution for such an instance is equivalent to a circuit state and an input assignment for which the fault affects the circuit´s outputs such that the error is not detected by the embedded fault detection. The number of solutions is precisely calculated by a #SAT solver and can be translated into an exact vulnerability measure. We demonstrate the applicability of this method for design space exploration by giving detailed results for various implementations of a deterministic random bit generator.