Formal verification of pipelined cryptographic circuits: A functional approach
Abir Bitat, Salah Merniz · Informatica · 2021
Cryptographic circuits are essential in systems where security is the main criteria. Therefore, it is crucial to ensure the correctness of not only the cryptographic algorithms, but also their hardware implementations. Formal methods, unlike the other validation techniques, guarantee the absence of errors.The problem is that designers still use conventional Hardware DescriptionLanguages (HDLs), which are poorly suited for formal verification.This paper presents a verificationmethodology for the pipelined cryptographic circuits using for-mal methods in an automatic manner. It consists on using the functional HDL Lava to describe and verify the equivalence between the behavioral specification and structural implementation of a circuit. To the best of our knowledge, we are the first to use this functional HDL for that computpurpose.To show the features of the proposed approach, it was applied to verify the pipelined implemen-tation of the cryptographic circuit AES (Advanced Encryption Standard).