Verification of Implementations of Cryptographic Hash Functions
Cryptographic hash functions have become the basis of modern network computing for identity authorization and secure computing; protocol consistency of cryptographic hash functions is one of the most important properties that affect the security and correctness of cryptographic implementations, and...
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2017-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/7924403/ |
| _version_ | 1818876753968365568 |
|---|---|
| author | Dexi Wang Yu Jiang Houbing Song Fei He Ming Gu Jiaguang Sun |
| author_facet | Dexi Wang Yu Jiang Houbing Song Fei He Ming Gu Jiaguang Sun |
| author_sort | Dexi Wang |
| collection | DOAJ |
| description | Cryptographic hash functions have become the basis of modern network computing for identity authorization and secure computing; protocol consistency of cryptographic hash functions is one of the most important properties that affect the security and correctness of cryptographic implementations, and protocol consistency should be well proven before being applied in practice. Software verification has seen substantial application in safety-critical areas and has shown the ability to deliver better quality assurance for modern software; thus, applying software verification to a protocol consistency proof for cryptographic hash functions is a reasonable approach to prove their correctness. Verification of protocol consistency of cryptographic hash functions includes modeling of the cryptographic protocol and program analysis of the cryptographic implementation; these require a dedicated cryptographic implementation model that preserves the semantics of the code, efficient analysis of cryptographic operations on arrays and bits, and the ability to verify large-scale implementations. In this paper, we propose a fully automatic software verification framework, VeriHash, that brings software verification to protocol consistency proofs for cryptographic hash function implementations. It solves the above challenges by introducing a novel cryptographic model design for modeling the semantics of cryptographic hash function implementations, extended array theories for analysis of operations, and compositional verification for scalability. We evaluated our verification framework on two SHA-3 cryptographic hash function implementations: the winner of the NIST SHA-3 competition, Keccack; and an open-source hash program, RHash. We successfully verified the core parts of the two implementations and reproduced a bug in the published edition of RHash. |
| first_indexed | 2024-12-19T13:47:24Z |
| format | Article |
| id | doaj.art-627d66f08ebe47209cdddbfd6843f776 |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-19T13:47:24Z |
| publishDate | 2017-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-627d66f08ebe47209cdddbfd6843f7762022-12-21T20:18:49ZengIEEEIEEE Access2169-35362017-01-0157816782510.1109/ACCESS.2017.26979187924403Verification of Implementations of Cryptographic Hash FunctionsDexi Wang0https://orcid.org/0000-0002-6285-9123Yu Jiang1Houbing Song2https://orcid.org/0000-0003-2631-9223Fei He3Ming Gu4Jiaguang Sun5School of Software, Tsinghua University, Beijing, ChinaSchool of Software, Tsinghua University, Beijing, ChinaDepartment of Electrical and Computer Engineering, West Virginia University Institute of Technology, Montgomery, WV, USASchool of Software, Tsinghua University, Beijing, ChinaSchool of Software, Tsinghua University, Beijing, ChinaSchool of Software, Tsinghua University, Beijing, ChinaCryptographic hash functions have become the basis of modern network computing for identity authorization and secure computing; protocol consistency of cryptographic hash functions is one of the most important properties that affect the security and correctness of cryptographic implementations, and protocol consistency should be well proven before being applied in practice. Software verification has seen substantial application in safety-critical areas and has shown the ability to deliver better quality assurance for modern software; thus, applying software verification to a protocol consistency proof for cryptographic hash functions is a reasonable approach to prove their correctness. Verification of protocol consistency of cryptographic hash functions includes modeling of the cryptographic protocol and program analysis of the cryptographic implementation; these require a dedicated cryptographic implementation model that preserves the semantics of the code, efficient analysis of cryptographic operations on arrays and bits, and the ability to verify large-scale implementations. In this paper, we propose a fully automatic software verification framework, VeriHash, that brings software verification to protocol consistency proofs for cryptographic hash function implementations. It solves the above challenges by introducing a novel cryptographic model design for modeling the semantics of cryptographic hash function implementations, extended array theories for analysis of operations, and compositional verification for scalability. We evaluated our verification framework on two SHA-3 cryptographic hash function implementations: the winner of the NIST SHA-3 competition, Keccack; and an open-source hash program, RHash. We successfully verified the core parts of the two implementations and reproduced a bug in the published edition of RHash.https://ieeexplore.ieee.org/document/7924403/Model-predictive controlsmootheninggradient-based optimizationemission controlurban traffic control |
| spellingShingle | Dexi Wang Yu Jiang Houbing Song Fei He Ming Gu Jiaguang Sun Verification of Implementations of Cryptographic Hash Functions IEEE Access Model-predictive control smoothening gradient-based optimization emission control urban traffic control |
| title | Verification of Implementations of Cryptographic Hash Functions |
| title_full | Verification of Implementations of Cryptographic Hash Functions |
| title_fullStr | Verification of Implementations of Cryptographic Hash Functions |
| title_full_unstemmed | Verification of Implementations of Cryptographic Hash Functions |
| title_short | Verification of Implementations of Cryptographic Hash Functions |
| title_sort | verification of implementations of cryptographic hash functions |
| topic | Model-predictive control smoothening gradient-based optimization emission control urban traffic control |
| url | https://ieeexplore.ieee.org/document/7924403/ |
| work_keys_str_mv | AT dexiwang verificationofimplementationsofcryptographichashfunctions AT yujiang verificationofimplementationsofcryptographichashfunctions AT houbingsong verificationofimplementationsofcryptographichashfunctions AT feihe verificationofimplementationsofcryptographichashfunctions AT minggu verificationofimplementationsofcryptographichashfunctions AT jiaguangsun verificationofimplementationsofcryptographichashfunctions |