Skip to main content
Top
Published in:

2018 | OriginalPaper | Chapter

hacspec: Towards Verifiable Crypto Standards

Authors : Karthikeyan Bhargavan, Franziskus Kiefer, Pierre-Yves Strub

Published in: Security Standardisation Research

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present hacspec, a collaborative effort to design a formal specification language for cryptographic primitives. Specifications (specs) written in hacspec are succinct, easy to read and implement, and lend themselves to formal verification using a variety of existing tools. The syntax of hacspec is similar to the pseudocode used in cryptographic standards but is equipped with a static type system and syntax checking tools that can find errors. Specs written in hacspec are executable and can hence be tested against test vectors taken from standards and specified in a common format. Finally, hacspec is designed to be compilable to other formal specification languages like F\({}^{\star }\), EasyCrypt, Coq, and cryptol, so that it can be used as the basis for formal proofs of functional correctness and cryptographic security using various verification frameworks. This paper presents the syntax, design, and tool architecture of hacspec. We demonstrate the use of the language to specify popular cryptographic algorithms, and describe preliminary compilers from hacspec to F\({}^{\star }\) and to EasyCrypt. Our goal is to invite authors of cryptographic standards to write their pseudocode in hacspec and to help the formal verification community develop the language and tools that are needed to promote high-assurance cryptographic software backed by mathematical proofs.

To get access to this content you need the following product:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference ChaCha20 and Poly1305 for IETF Protocols. IETF RFC 7539 (2015) ChaCha20 and Poly1305 for IETF Protocols. IETF RFC 7539 (2015)
2.
go back to reference Elliptic Curves for Security. IETF RFC 7748 (2016) Elliptic Curves for Security. IETF RFC 7748 (2016)
6.
go back to reference Bernstein, D.J.: Cache-timing attacks on AES. Technical report (2005) Bernstein, D.J.: Cache-timing attacks on AES. Technical report (2005)
7.
go back to reference Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secure Comput. 5, 193–207 (2007)CrossRef Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secure Comput. 5, 193–207 (2007)CrossRef
9.
go back to reference Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: Proceedings of the USENIX Security Symposium, August 2017 Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: Proceedings of the USENIX Security Symposium, August 2017
10.
go back to reference US Department of Commerce, National Institute of Standards and Technology (NIST): Federal Information Processing Standards Publication 180-4: Secure Hash Standard (SHS) (2012) US Department of Commerce, National Institute of Standards and Technology (NIST): Federal Information Processing Standards Publication 180-4: Secure Hash Standard (SHS) (2012)
11.
go back to reference Courtois, N.T., Emirdag, P., Valsorda, F.: Private key recovery combination attacks: on extreme fragility of popular bitcoin key management, wallet and cold storage solutions in presence of poor RNG events. Cryptology ePrint Archive, Report 2014/848 (2014). https://eprint.iacr.org/2014/848 Courtois, N.T., Emirdag, P., Valsorda, F.: Private key recovery combination attacks: on extreme fragility of popular bitcoin key management, wallet and cold storage solutions in presence of poor RNG events. Cryptology ePrint Archive, Report 2014/848 (2014). https://​eprint.​iacr.​org/​2014/​848
12.
go back to reference Dworkin, M.: Recommendation for Block Cipher Modes of Operation: Galois/Counter Mode (GCM) and GMAC. NIST Special Publication 800-38D (2007) Dworkin, M.: Recommendation for Block Cipher Modes of Operation: Galois/Counter Mode (GCM) and GMAC. NIST Special Publication 800-38D (2007)
13.
go back to reference Dworkin, M.J., Barker, E.B., Nechvatal, J.R., Foti, J., Bassham, L.E., Roback, E., Dray Jr., J.F.: Advanced Encryption Standard (AES). NIST FIPS-197 (2001) Dworkin, M.J., Barker, E.B., Nechvatal, J.R., Foti, J., Bassham, L.E., Roback, E., Dray Jr., J.F.: Advanced Encryption Standard (AES). NIST FIPS-197 (2001)
15.
go back to reference Institute, A.N.S.: Public Key Cryptography for the Financial Services Industry: The Elliptic Curve Digital Signature Algorithm. ANSI X9.62-1998 (199) Institute, A.N.S.: Public Key Cryptography for the Financial Services Industry: The Elliptic Curve Digital Signature Algorithm. ANSI X9.62-1998 (199)
21.
go back to reference Swamy, N., et al.: Dependent types and multi-monadic effects in F*. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20–22 January 2016, pp. 256–270 (2016). https://doi.org/10.1145/2837614.2837655 Swamy, N., et al.: Dependent types and multi-monadic effects in F*. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20–22 January 2016, pp. 256–270 (2016). https://​doi.​org/​10.​1145/​2837614.​2837655
22.
go back to reference Tomb, A.: Automated verification of real-world cryptographic implementations. IEEE Secur. Priv. 14(6), 26–33 (2016)CrossRef Tomb, A.: Automated verification of real-world cryptographic implementations. IEEE Secur. Priv. 14(6), 26–33 (2016)CrossRef
23.
go back to reference Zinzindohoué, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, 30 October–03 November 2017, pp. 1789–1806 (2017) Zinzindohoué, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, 30 October–03 November 2017, pp. 1789–1806 (2017)
Metadata
Title
hacspec: Towards Verifiable Crypto Standards
Authors
Karthikeyan Bhargavan
Franziskus Kiefer
Pierre-Yves Strub
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-04762-7_1

Premium Partner