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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
See, for example, this bug in a popular Curve25519 implementation https://www.imperialviolet.org/2014/09/07/provers.html.
- 2.
- 3.
- 4.
- 5.
- 6.
- 7.
- 8.
- 9.
- 10.
References
ChaCha20 and Poly1305 for IETF Protocols. IETF RFC 7539 (2015)
Elliptic Curves for Security. IETF RFC 7748 (2016)
Almeida, J., et al.: Jasmin: high-assurance and high-speed cryptography. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS. pp. 1807–1823. (2017, to appear). https://acmccs.github.io/papers/p1807-almeidaA.pdf
Appel, A.W.: Verified software toolchain. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 2–2. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28891-3_2
Barthe, G., Dupressoir, F., Grégoire, B., Kunz, C., Schmidt, B., Strub, P.-Y.: EasyCrypt: a tutorial. In: Aldini, A., Lopez, J., Martinelli, F. (eds.) FOSAD 2012-2013. LNCS, vol. 8604, pp. 146–166. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10082-1_6
Bernstein, D.J.: Cache-timing attacks on AES. Technical report (2005)
Blanchet, B.: A computationally sound mechanized prover for security protocols. IEEE Trans. Dependable Secure Comput. 5, 193–207 (2007)
Böck, H., Zauner, A., Devlin, S., Somorovsky, J., Jovanovic, P.: Nonce-disrespecting adversaries: practical forgery attacks on GCM in TLS. In: 10th USENIX Workshop on Offensive Technologies (WOOT 2016). USENIX Association, Austin (2016). https://www.usenix.org/conference/woot16/workshop-program/presentation/bock
Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: Proceedings of the USENIX Security Symposium, August 2017
US Department of Commerce, National Institute of Standards and Technology (NIST): Federal Information Processing Standards Publication 180-4: Secure Hash Standard (SHS) (2012)
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
Dworkin, M.: Recommendation for Block Cipher Modes of Operation: Galois/Counter Mode (GCM) and GMAC. NIST Special Publication 800-38D (2007)
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)
Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: Proceedings of the IEEE Symposium on Security and Privacy 2019, S&P 2019, May 2019. http://adam.chlipala.net/papers/FiatCryptoSP19/
Institute, A.N.S.: Public Key Cryptography for the Financial Services Industry: The Elliptic Curve Digital Signature Algorithm. ANSI X9.62-1998 (199)
Josefsson, S., Liusvaara, I.: Edwards-Curve Digital Signature Algorithm (EdDSA). RFC 8032 (Informational), January 2017. 10.17487/RFC8032. https://doi.org/10.17487/RFC8032. https://www.rfc-editor.org/rfc/rfc8032.txt
Käsper, E., Schwabe, P.: Faster and timing-attack resistant AES-GCM. In: Clavier, C., Gaj, K. (eds.) CHES 2009. LNCS, vol. 5747, pp. 1–17. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04138-9_1
Langley, A., Hamburg, M., Turner, S.: Elliptic Curves for Security. RFC 7748 (Informational), January 2016. https://doi.org/10.17487/RFC7748. https://www.rfc-editor.org/rfc/rfc7748.txt
Mouha, N., Raunak, M.S., Kuhn, D.R., Kacker, R.: Finding bugs in cryptographic hash function implementations. Cryptology ePrint Archive, Report 2017/891 (2017). https://eprint.iacr.org/2017/891
Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 53–72. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46666-7_4
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
Tomb, A.: Automated verification of real-world cryptographic implementations. IEEE Secur. Priv. 14(6), 26–33 (2016)
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)
Acknowledgments
We would like to thank all participants of the HACS workshop that made this work possible. hacspec is an ongoing project with a number contributors in addition to the the authors.
Online Materials
hacspec source code: https://github.com/hacs-workshop/hacspec/
hacspec builtin library documentation: https://hacs-workshop.github.io/hacspec/docs/
hacspec mailing list: https://moderncrypto.org/mailman/listinfo/hacspec.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Bhargavan, K., Kiefer, F., Strub, PY. (2018). hacspec: Towards Verifiable Crypto Standards. In: Cremers, C., Lehmann, A. (eds) Security Standardisation Research. SSR 2018. Lecture Notes in Computer Science(), vol 11322. Springer, Cham. https://doi.org/10.1007/978-3-030-04762-7_1
Download citation
DOI: https://doi.org/10.1007/978-3-030-04762-7_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-04761-0
Online ISBN: 978-3-030-04762-7
eBook Packages: Computer ScienceComputer Science (R0)