Formal verification of pipelined cryptographic circuits: A functional approach

Abir Bitat, Salah Merniz

Abstract


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 Description
Languages (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).


Full Text:

PDF

References


[Toma, D. ”Vrification Formelle des systmes numriques par dmonstration de thormes: appli-cation aux composants cryptographiques” (Doc-toral dissertation) (2006).

Singh, Kirat Pal, and Shivani Parmar. ”Design of high performanceMIPS cryptography proces-sor based on T-DES algorithm.” arXiv preprint arXiv:1503.03166 (2015).

Ali, Imran, Gulistan Raja, and Ahmad Khalil Khan. ”A 16-Bit Architecture of Advanced En-cryption Standard for Embedded Applications.” 2014 12th International Conference on Frontiers

of Information Technology. IEEE, (2014).

Lam, Chiu Hong. ”Verification of pipelined ciphers”. MS thesis. University of Waterloo, (2009).

Clarke, E., Kroening, D. ”Hardware verification using ANSI-C programs as a reference”. In Pro-ceedings of the ASP-DAC Asia and South Pa-cific Design Automation Conference. pp. 308-311. IEEE. (2003).

Homma, Naofumi, Kazuya Saito, and Takafumi

Aoki. ”A Formal Approach to Designing Cryp-tographic Processors Based on GF (2^m) Arith-metic Circuits.” IEEE Transactions on Informa-tion Forensics and Security vol. 7, no 1, p. 3-13. (2011).

Homma, Naofumi, Kazuya Saito, and Takafumi Aoki. ”Toward formal design of practical cryp-tographic hardware based on Galois field arith-metic.” IEEE Transactions on Computers. vol. 63, no 10, p. 2604-2613 (2013).

Bond, Barry, et al. ”Vale: Verifying high-performance cryptographic assembly code.” 26th USENIX Security Symposium (USENIX

Security 17). p. 917-934. (2017).

Lewis, Jeff. ”Cryptol: specification, implemen-tation and verification of high-grade crypto-graphic applications.” Proceedings of the 2007

ACM workshop on Formal methods in security engineering. p. 41-41.(2007).

Lam, Chiu Hong, and Mark D. Aagaard. ”For-mal Verification of a Pipelined Cryptographic Circuit Using Equivalence Checking and Com-pletion Functions.” 2007 Canadian Conference

on Electrical and Computer Engineering. IEEE, p. 1401-1404. (2007).

Kim, Ho Won, and Sunggu Lee. ”Design and im-plementation of a private and public key crypto processor and its application to a security sys-tem.” IEEE Transactions on Consumer Electron-ics.vol. 50, no 1, p. 214-224. (2004).

Wolfs, Davy, et al. ”Design automation for cryp-tographic hardware using functional languages.” Proceedings of the 32nd WIC Symposiumon In-formation Theory in the Benelux. Werkgemeen-schap voor Informatie-en Communicatietheo-rie.; Netherlands, p. 194-201. (2011).

Chen, Gang. ”A short historical survey of func-tional hardware languages.” ISRN Electronics vol 2012 (2012).

Bjesse, Per, et al. ”Lava: hardware design in Haskell.” ACM SIGPLAN Notices vol. 34, no 1, p. 174-184. (1998).

Guo, Xiaolong, et al. ”Pre-silicon security ver-ification and validation: A formal perspective.” Proceedings of the 52nd Annual Design Au-tomation Conference. p. 1-6. (2015).

Claessen, Koen, and Mary Sheeran. ”A slightly revised tutorial on lava: A hardware description and verification system.” (2007).

Daemen, Joan, and Vincent Rijmen. The de-sign of Rijndael: AES-the advanced encryption standard. Springer Science and Business Media,

(2013).

Abir, Bitat., and merniz. Salah. ”Towards formal verification of cryptographic circuits: A func-tional approach.” 2018 3rd International Confer-ence on Pattern Analysis and Intelligent Systems(PAIS). IEEE,p. 1-6. (2018).




DOI: https://doi.org/10.31449/inf.v45i4.3176

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 License.