{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:21:51Z","timestamp":1743070911552,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030763831"},{"type":"electronic","value":"9783030763848"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-76384-8_19","type":"book-chapter","created":{"date-parts":[[2021,5,18]],"date-time":"2021-05-18T23:50:53Z","timestamp":1621381853000},"page":"304-321","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Efficient Verification of Optimized Code"],"prefix":"10.1007","author":[{"given":"Marc","family":"Schoolderman","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Moerman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sjaak","family":"Smetsers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marko","family":"van Eekelen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,5,19]]},"reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-28891-3_2","volume-title":"NASA Formal Methods","author":"AW Appel","year":"2012","unstructured":"Appel, A.W.: Verified software toolchain. In: Goodloe, A.E., Person, S. (eds.) NFM 2012. LNCS, vol. 7226, pp. 2\u20132. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_2"},{"key":"19_CR2","unstructured":"Atmel Corporation: AVR Instruction Set Manual, revision 0856L (2016)"},{"key":"19_CR3","unstructured":"AVR Libc Project: avr-libc User Manual. https:\/\/www.nongnu.org\/avr-libc\/user-manual\/FAQ.html"},{"key":"19_CR4","unstructured":"Barbosa, H., Blanchette, J.C., Fleury, M., Fontaine, P., Schurr, H.J.: Better SMT proofs for easier reconstruction. In: AITP 2019\u20134th Conference on Artificial Intelligence and Theorem Proving. Obergurgl, Austria, April 2019"},{"key":"19_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/11745853_14","volume-title":"Public Key Cryptography - PKC 2006","author":"DJ Bernstein","year":"2006","unstructured":"Bernstein, D.J.: Curve25519: new Diffie-Hellman speed records. In: Yung, M., Dodis, Y., Kiayias, A., Malkin, T. (eds.) PKC 2006. LNCS, vol. 3958, pp. 207\u2013228. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11745853_14"},{"key":"19_CR6","unstructured":"Bernstein, D., Lange, T.: Montgomery curves and the Montgomery ladder. Cryptology ePrint Archive, IACR (2017)"},{"key":"19_CR7","unstructured":"Bhargavan, K., et al.: Everest: towards a verified, drop-in replacement of HTTPS. In: Lerner, B.S., Bod\u00edk, R., Krishnamurthi, S. (eds.) 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), vol. 71, pp. 1:1\u20131:12. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2017)"},{"key":"19_CR8","unstructured":"Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: Proceedings of the 26th USENIX Conference on Security Symposium, pp. 917\u2013934 (2017)"},{"key":"19_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-27954-6_11","volume-title":"Topics in Cryptology \u2013 CT-RSA 2012","author":"BB Brumley","year":"2012","unstructured":"Brumley, B.B., Barbosa, M., Page, D., Vercauteren, F.: Practical realisation and elimination of an ECC-related software bug attack. In: Dunkelman, O. (ed.) CT-RSA 2012. LNCS, vol. 7178, pp. 171\u2013186. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27954-6_11"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Chen, Y.F., et al.: Verifying Curve25519 software. In: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp. 299\u2013309. CCS \u201914, Association for Computing Machinery, New York, NY, USA (2014)","DOI":"10.1145\/2660267.2660370"},{"key":"19_CR11","unstructured":"The Coq proof assistant reference manual (2015). https:\/\/coq.inria.fr\/documentation"},{"issue":"6","key":"19_CR12","doi-asserted-by":"publisher","first-page":"644","DOI":"10.1109\/TIT.1976.1055638","volume":"22","author":"W Diffie","year":"1976","unstructured":"Diffie, W., Hellman, M.: New directions in cryptography. IEEE Trans. Inf. Theor. 22(6), 644\u2013654 (1976)","journal-title":"IEEE Trans. Inf. Theor."},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1007\/978-3-319-48869-1_5","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"R Dockins","year":"2016","unstructured":"Dockins, R., Foltzer, A., Hendrix, J., Huffman, B., McNamee, D., Tomb, A.: Constructing semantic models of programs with the software analysis workbench. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 56\u201372. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_5"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"D\u00fcll, M., et al.: High-speed Curve25519 on 8-bit, 16-bit, and 32-bit microcontrollers. Des. Codes Crypt. 77(2\u20133), 493\u2013514 (2015)","DOI":"10.1007\/s10623-015-0087-1"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic - with proofs, without compromises. In: 2019 IEEE Symposium on Security and Privacy (SP), pp. 1202\u20131219 (2019)","DOI":"10.1109\/SP.2019.00005"},{"key":"19_CR16","doi-asserted-by":"publisher","unstructured":"Erk\u00f6k, L., Carlsson, M., Wick, A.: Hardware\/software co-verification of cryptographic algorithms using Cryptol. In: 2009 Formal Methods in Computer-Aided Design, pp. 188\u2013191 (2009). https:\/\/doi.org\/10.1109\/FMCAD.2009.5351121","DOI":"10.1109\/FMCAD.2009.5351121"},{"key":"19_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"19_CR18","doi-asserted-by":"crossref","unstructured":"Genkin, D., Valenta, L., Yarom, Y.: May the fourth be with you: a microarchitectural side channel attack on several real-world applications of Curve25519. In: Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pp. 845\u2013858. CCS \u201917, Association for Computing Machinery, New York, NY, USA (2017)","DOI":"10.1145\/3133956.3134029"},{"key":"19_CR19","unstructured":"GNU Project: avr-gcc ABI. https:\/\/gcc.gnu.org\/wiki\/avr-gcc"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-540-28632-5_9","volume-title":"Cryptographic Hardware and Embedded Systems - CHES 2004","author":"N Gura","year":"2004","unstructured":"Gura, N., Patel, A., Wander, A., Eberle, H., Shantz, S.C.: Comparing elliptic curve cryptography and RSA on 8-bit CPUs. In: Joye, M., Quisquater, J.-J. (eds.) CHES 2004. LNCS, vol. 3156, pp. 119\u2013132. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-28632-5_9"},{"key":"19_CR21","unstructured":"ISO: ISO\/IEC 15408\u20131:2009 Information technology\u2013Security techniques\u2013Evaluation criteria for IT security\u2013Part 1: Introduction and general model (2009)"},{"key":"19_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-319-48965-0_36","volume-title":"Cryptology and Network Security","author":"T Kaufmann","year":"2016","unstructured":"Kaufmann, T., Pelletier, H., Vaudenay, S., Villegas, K.: When constant-time source yields variable-time binary: exploiting Curve25519-donna built with MSVC 2015. In: Foresti, S., Persiano, G. (eds.) CANS 2016. LNCS, vol. 10052, pp. 573\u2013582. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48965-0_36"},{"key":"19_CR23","unstructured":"Kleppmann, M.: Implementing Curve25519\/X25519: A tutorial on elliptic curve cryptography. University of Cambridge, Department of Computer Science and Technology, Technical report (2020)"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Langley, A., Hamburg, M., Turner, S.: Elliptic Curves for Security. RFC 7748, January 2016. https:\/\/rfc-editor.org\/rfc\/rfc7748.txt","DOI":"10.17487\/RFC7748"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd ACM Symposium on Principles of Programming Languages, pp. 42\u201354. ACM Press (2006)","DOI":"10.1145\/1111320.1111042"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Liu, J., Shi, X., Tsai, M.H., Wang, B.Y., Yang, B.Y.: Verifying arithmetic in cryptographic c programs. In: 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 552\u2013564. IEEE (2019)","DOI":"10.1109\/ASE.2019.00058"},{"key":"19_CR27","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1090\/S0025-5718-1987-0866113-7","volume":"48","author":"PL Montgomery","year":"1987","unstructured":"Montgomery, P.L.: Speeding the Pollard and elliptic curve methods of factorization. Math. Comput. 48, 243\u2013264 (1987)","journal-title":"Math. Comput."},{"key":"19_CR28","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Proofs and refutations, and Z3. In: LPAR Workshops, vol. 418, pp. 123\u2013132. Doha, Qatar (2008)"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Protzenko, J., et al.: Evercrypt: a fast, verified, cross-platform cryptographic provider. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 983\u20131002. IEEE (2020)","DOI":"10.1109\/SP40000.2020.00114"},{"key":"19_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-319-72308-2_5","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"M Schoolderman","year":"2017","unstructured":"Schoolderman, M.: Verifying branch-free assembly code in Why3. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 66\u201383. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-72308-2_5"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Schoolderman, M., Smetsers, S., van Eekelen, M.: Is deductive program verification mature enough to be taught to software engineers? In: Proceedings of the 8th Computer Science Education Research Conference, pp. 50\u201357. CSERC \u201919, Association for Computing Machinery, New York, NY, USA (2019)","DOI":"10.1145\/3375258.3375265"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Schwabe, P., Viguer, B., Weerweg, T., Wiedijk, F.: A Coq proof of the correctness of x25519 in TweetNaCl. In: 2021 IEEE 31th Computer Security Foundations Symposium (CSF). (to appear) (2021)","DOI":"10.1109\/CSF51468.2021.00023"},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Velvindron, L., Baushke, M.D.: Increase the Secure Shell Minimum Recommended Diffie-Hellman Modulus Size to 2048 Bits. RFC 8270, December 2017. https:\/\/rfc-editor.org\/rfc\/rfc8270.txt","DOI":"10.17487\/RFC8270"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: ACM Conference on Computer and Communications Security (CCS). Dallas, United States, October 2017","DOI":"10.1145\/3133956.3134043"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Zinzindohou\u00e9, J.K., Bartzia, E., Bhargavan, K.: A verified extensible library of elliptic curves. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 296\u2013309 (2016)","DOI":"10.1109\/CSF.2016.28"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-76384-8_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,12,27]],"date-time":"2022-12-27T21:13:59Z","timestamp":1672175639000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-76384-8_19"}},"subtitle":["Correct High-Speed X25519"],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030763831","9783030763848"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-76384-8_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"19 May 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 May 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 May 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/shemesh.larc.nasa.gov\/nfm2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"66","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"21","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}