FERMION - Formal Verification of Masked Hardware Implementations

develop techniques to formally prove that systems are immune against power side channel attacks and to automatically construct provably resistant systems. We will build on existing results to develop complete methods that are scalable to industrial size circuits and powerful attacks models. We will then develop tools that automatically construct side-channel resistant circuits given an unprotected circuit. These circuits will be provably correct and will significantly reduce the manual effort of the designer in constructing resistant systems, and the effort spent in external certification.