Formal verification of pipelined cryptographic circuits: A functional approach
DOI:
https://doi.org/10.31449/inf.v45i4.3176Abstract
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).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).
Downloads
Published
How to Cite
Issue
Section
License
I assign to Informatica, An International Journal of Computing and Informatics ("Journal") the copyright in the manuscript identified above and any additional material (figures, tables, illustrations, software or other information intended for publication) submitted as part of or as a supplement to the manuscript ("Paper") in all forms and media throughout the world, in all languages, for the full term of copyright, effective when and if the article is accepted for publication. This transfer includes the right to reproduce and/or to distribute the Paper to other journals or digital libraries in electronic and online forms and systems.
I understand that I retain the rights to use the pre-prints, off-prints, accepted manuscript and published journal Paper for personal use, scholarly purposes and internal institutional use.
In certain cases, I can ask for retaining the publishing rights of the Paper. The Journal can permit or deny the request for publishing rights, to which I fully agree.
I declare that the submitted Paper is original, has been written by the stated authors and has not been published elsewhere nor is currently being considered for publication by any other journal and will not be submitted for such review while under review by this Journal. The Paper contains no material that violates proprietary rights of any other person or entity. I have obtained written permission from copyright owners for any excerpts from copyrighted works that are included and have credited the sources in my article. I have informed the co-author(s) of the terms of this publishing agreement.
Copyright © Slovenian Society Informatika
