{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T08:43:06Z","timestamp":1726130586846},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030816841"},{"type":"electronic","value":"9783030816858"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,15]],"date-time":"2021-07-15T00:00:00Z","timestamp":1626307200000},"content-version":"vor","delay-in-days":195,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"Abstract<\/jats:title>\nWe have completed machine-assisted proofs of two highly-optimized cryptographic primitives, AES-256-GCM and SHA-384. We have verified that the implementations of these primitives, written in a mix of C and x86 assembly, are memory safe and functionally correct, by which we mean input-output equivalent to their algorithmic specifications. Our proofs were completed using SAW, a bounded cryptographic verification tool which we have extended to handle embedded x86. The code we have verified comes from AWS LibCrypto. This code is identical to BoringSSL and very similar to OpenSSL, from which it ultimately derives. We believe we are the first to formally verify these implementations, which protect the security of nearly everybody on the internet.<\/jats:p>","DOI":"10.1007\/978-3-030-81685-8_31","type":"book-chapter","created":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:02:35Z","timestamp":1626480155000},"page":"645-668","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verified Cryptographic Code for Everybody"],"prefix":"10.1007","author":[{"given":"Brett","family":"Boston","sequence":"first","affiliation":[]},{"given":"Samuel","family":"Breese","sequence":"additional","affiliation":[]},{"given":"Joey","family":"Dodds","sequence":"additional","affiliation":[]},{"given":"Mike","family":"Dodds","sequence":"additional","affiliation":[]},{"given":"Brian","family":"Huffman","sequence":"additional","affiliation":[]},{"given":"Adam","family":"Petcher","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Stefanescu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,15]]},"reference":[{"key":"31_CR1","doi-asserted-by":"publisher","unstructured":"Almeida, J.B., et al.: The last mile: high-assurance and high-speed cryptographic implementations. In: 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, 18\u201321 May 2020, pp. 965\u2013982. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00028","DOI":"10.1109\/SP40000.2020.00028"},{"key":"31_CR2","unstructured":"Amazon Web Services: AWS libcrypto (AWS-LC) public preview. https:\/\/github.com\/awslabs\/aws-lc"},{"key":"31_CR3","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, p. 2. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28891-3_2"},{"key":"31_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"31_CR5","unstructured":"Bond, B., et al.: Vale: verifying high-performance cryptographic assembly code. In: 26th USENIX Security Symposium, USENIX Security 2017, Vancouver, BC, pp. 917\u2013934. USENIX Association (August 2017)"},{"key":"31_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-319-96142-2_26","volume-title":"Computer Aided Verification","author":"A Chudnov","year":"2018","unstructured":"Chudnov, A., et al.: Continuous formal verification of Amazon s2n. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10982, pp. 430\u2013446. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96142-2_26"},{"key":"31_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Clarke","year":"2004","unstructured":"Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168\u2013176. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24730-2_15"},{"key":"31_CR9","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: Proceedings of the 40th IEEE Symposium on Security and Privacy, S&P 2019 (May 2019)","DOI":"10.1109\/SP.2019.00005"},{"issue":"POPL","key":"31_CR10","doi-asserted-by":"publisher","first-page":"63:1","DOI":"10.1145\/3290376","volume":"3","author":"A Fromherz","year":"2019","unstructured":"Fromherz, A., Giannarakis, N., Hawblitzel, C., Parno, B., Rastogi, A., Swamy, N.: A verified, efficient embedding of a verifiable assembly language. Proc. ACM Program. Lang. 3(POPL), 63:1-63:30 (2019). https:\/\/doi.org\/10.1145\/3290376","journal-title":"Proc. ACM Program. Lang."},{"key":"31_CR11","unstructured":"Galois Inc.: Cryptol: the language of cryptography. https:\/\/cryptol.net\/files\/ProgrammingCryptol.pdf"},{"key":"31_CR12","unstructured":"Galois Inc.: Macaw binary analysis framework. https:\/\/github.com\/GaloisInc\/macaw"},{"key":"31_CR13","unstructured":"Galois Inc.: SAW tutorial. https:\/\/saw.galois.com\/tutorial.html"},{"key":"31_CR14","unstructured":"Galois Inc.: Software analysis workbench (SAW). https:\/\/saw.galois.com\/"},{"key":"31_CR15","unstructured":"Galois Inc.: What4 symbolic formula representation and solver interaction library. https:\/\/github.com\/GaloisInc\/what4"},{"key":"31_CR16","unstructured":"Google: boringssl. https:\/\/boringssl.googlesource.com\/boringssl"},{"key":"31_CR17","doi-asserted-by":"publisher","unstructured":"Lim, J.P., Nagarakatte, S.: Automatic equivalence checking for assembly implementations of cryptography libraries. In: Kandemir, M.T., Jimborean, A., Moseley, T. (eds.) IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2019, Washington, DC, USA, 16\u201320 February 2019, pp. 37\u201349. IEEE (2019). https:\/\/doi.org\/10.1109\/CGO.2019.8661180","DOI":"10.1109\/CGO.2019.8661180"},{"key":"31_CR18","unstructured":"National Security Agency: Commercial national security algorithm suite. https:\/\/apps.nsa.gov\/iad\/programs\/iad-initiatives\/cnsa-suite.cfm"},{"key":"31_CR19","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P.W.: Continuous reasoning: scaling the impact of formal methods. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, 9\u201312 July 2018, pp. 13\u201325. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209109","DOI":"10.1145\/3209108.3209109"},{"key":"31_CR20","unstructured":"OpenSSL cryptography and SSL\/TLS toolkit. https:\/\/www.openssl.org"},{"key":"31_CR21","doi-asserted-by":"publisher","unstructured":"Protzenko, J., et al.: Evercrypt: a fast, verified, cross-platform cryptographic provider. In: 2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, 18\u201321 May 2020, pp. 983\u20131002. IEEE (2020). https:\/\/doi.org\/10.1109\/SP40000.2020.00114","DOI":"10.1109\/SP40000.2020.00114"},{"key":"31_CR22","doi-asserted-by":"publisher","unstructured":"Ye, K.Q., Green, M., Sanguansin, N., Beringer, L., Petcher, A., Appel, A.W.: Verified correctness and security of mbedtls HMAC-DRBG. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, 30 October\u201303 November 2017, pp. 2007\u20132020. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3133974","DOI":"10.1145\/3133956.3133974"},{"key":"31_CR23","doi-asserted-by":"publisher","unstructured":"Zinzindohou\u00e9, J.K., Bhargavan, K., Protzenko, J., Beurdouche, B.: HACL*: a verified modern cryptographic library. In: Thuraisingham, B.M., Evans, D., Malkin, T., Xu, D. (eds.) Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, 30 October\u201303 November 2017, pp. 1789\u20131806. ACM (2017). https:\/\/doi.org\/10.1145\/3133956.3134043","DOI":"10.1145\/3133956.3134043"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81685-8_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,17]],"date-time":"2021-07-17T00:09:49Z","timestamp":1626480589000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81685-8_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030816841","9783030816858"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81685-8_31","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":"15 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","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":"20 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"33","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-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":"290","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":"63","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":"0","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":"22% - 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":"12","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)"}},{"value":"16 tool papers and 5 invited papers are also included.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}