{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T21:01:17Z","timestamp":1751662877634,"version":"3.41.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1521584"],"award-info":[{"award-number":["1521584"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>\n            One of the biggest implementation challenges in security-critical network protocols is nested state machines. In practice today, state machines are either implemented manually at a low level, risking bugs easily missed in audits; or are written using higher-level abstractions like threads, depending on runtime systems that may sacrifice performance or compatibility with the ABIs of important platforms (e.g., resource-constrained IoT systems). We present a compiler-based technique allowing the best of both worlds, coding protocols in a natural high-level form, using freer monads to represent nested\n            <jats:italic>coroutines<\/jats:italic>\n            , which are then compiled automatically to lower-level code with explicit state. In fact, our compiler is implemented as a tactic in the Coq proof assistant, structuring compilation as search for an equivalence proof for source and target programs. As such, it is straightforwardly (and soundly) extensible with new hints, for instance regarding new data structures that may be used for efficient lookup of coroutines. As a case study, we implemented a core of TLS sufficient for use with popular Web browsers, and our experiments show that the extracted Haskell code achieves reasonable performance.\n          <\/jats:p>","DOI":"10.1145\/3498685","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Certifying derivation of state machines from coroutines"],"prefix":"10.1145","volume":"6","author":[{"given":"Mirai","family":"Ikebuchi","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Japan"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9854-7500","authenticated-orcid":false,"given":"Andres","family":"Erbsen","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, USA"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Formal Certification of Code-Based Cryptographic Proofs. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009","author":"Barthe Gilles","year":"2009","unstructured":"Gilles Barthe , Benjamin Gr\u00e9goire , and Santiago Zanella-B\u00e9guelin . 2009 . Formal Certification of Code-Based Cryptographic Proofs. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009 . ACM, 90\u2013101. http:\/\/software.imdea.org\/~szanella\/Zanella.2009.POPL.pdf Gilles Barthe, Benjamin Gr\u00e9goire, and Santiago Zanella-B\u00e9guelin. 2009. Formal Certification of Code-Based Cryptographic Proofs. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009. ACM, 90\u2013101. http:\/\/software.imdea.org\/~szanella\/Zanella.2009.POPL.pdf"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319618"},{"key":"e_1_2_2_3_1","unstructured":"Eli Bendersky. 2009. Co-routines as an alternative to state machines. https:\/\/eli.thegreenplace.net\/2009\/08\/29\/co-routines-as-an-alternative-to-state-machines\/ Retrieved 2020-08-20.  Eli Bendersky. 2009. Co-routines as an alternative to state machines. https:\/\/eli.thegreenplace.net\/2009\/08\/29\/co-routines-as-an-alternative-to-state-machines\/ Retrieved 2020-08-20."},{"volume-title":"Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium. 207\u2013221","author":"Beringer Lennart","key":"e_1_2_2_4_1","unstructured":"Lennart Beringer , Adam Petcher , Katherine Q. Ye , and Andrew W. Appel . 2015 . Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium. 207\u2013221 . https:\/\/www.usenix.org\/system\/files\/conference\/usenixsecurity15\/sec15-paper-beringer.pdf Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. In 24th USENIX Security Symposium. 207\u2013221. https:\/\/www.usenix.org\/system\/files\/conference\/usenixsecurity15\/sec15-paper-beringer.pdf"},{"volume-title":"2015 IEEE Symposium on Security and Privacy. 535\u2013552","author":"Beurdouche B.","key":"e_1_2_2_5_1","unstructured":"B. Beurdouche , K. Bhargavan , A. Delignat-Lavaud , C. Fournet , M. Kohlweiss , A. Pironti , P. Strub , and J. K. Zinzindohoue . 2015. A Messy State of the Union: Taming the Composite State Machines of TLS . In 2015 IEEE Symposium on Security and Privacy. 535\u2013552 . https:\/\/smacktls.com\/smack.pdf B. Beurdouche, K. Bhargavan, A. Delignat-Lavaud, C. Fournet, M. Kohlweiss, A. Pironti, P. Strub, and J. K. Zinzindohoue. 2015. A Messy State of the Union: Taming the Composite State Machines of TLS. In 2015 IEEE Symposium on Security and Privacy. 535\u2013552. https:\/\/smacktls.com\/smack.pdf"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2006.1"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473599"},{"key":"e_1_2_2_8_1","volume-title":"Protocol State Fuzzing of TLS Implementations. In 24th USENIX Security Symposium (USENIX Security 15)","author":"de Ruiter Joeri","year":"2015","unstructured":"Joeri de Ruiter and Erik Poll . 2015 . Protocol State Fuzzing of TLS Implementations. In 24th USENIX Security Symposium (USENIX Security 15) . USENIX Association, Washington, D.C., 193\u2013206. isbn:978-1-939133-11-3 https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/de-ruiter Joeri de Ruiter and Erik Poll. 2015. Protocol State Fuzzing of TLS Implementations. In 24th USENIX Security Symposium (USENIX Security 15). USENIX Association, Washington, D.C., 193\u2013206. isbn:978-1-939133-11-3 https:\/\/www.usenix.org\/conference\/usenixsecurity15\/technical-sessions\/presentation\/de-ruiter"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341686"},{"key":"e_1_2_2_11_1","volume-title":"Proceedings of the Annual Conference on USENIX Annual Technical Conference","author":"Engelschall Ralf S.","year":"2000","unstructured":"Ralf S. Engelschall . 2000 . Portable Multithreading: The Signal Stack Trick for User-Space Thread Creation . In Proceedings of the Annual Conference on USENIX Annual Technical Conference ( San Diego, California) (ATC \u201900). USENIX Association, USA, 20. https:\/\/www.usenix.org\/legacy\/publications\/library\/proceedings\/usenix 2000\/general\/full_papers\/engelschall\/engelschall.pdf Ralf S. Engelschall. 2000. Portable Multithreading: The Signal Stack Trick for User-Space Thread Creation. In Proceedings of the Annual Conference on USENIX Annual Technical Conference (San Diego, California) (ATC \u201900). USENIX Association, USA, 20. https:\/\/www.usenix.org\/legacy\/publications\/library\/proceedings\/usenix2000\/general\/full_papers\/engelschall\/engelschall.pdf"},{"volume-title":"Without Compromises","author":"Erbsen Andres","key":"e_1_2_2_12_1","unstructured":"Andres Erbsen , Jade Philipoom , Jason Gross , Robert Sloan , and Adam Chlipala . 2019. Simple High-Level Code For Cryptographic Arithmetic \u2013 With Proofs , Without Compromises . In IEEE Security & Privacy (San Francisco, CA , USA) . http:\/\/adam.chlipala.net\/papers\/FiatCryptoSP19\/ Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. Simple High-Level Code For Cryptographic Arithmetic \u2013 With Proofs, Without Compromises. In IEEE Security & Privacy (San Francisco, CA, USA). http:\/\/adam.chlipala.net\/papers\/FiatCryptoSP19\/"},{"key":"e_1_2_2_13_1","volume-title":"First International Workshop on the Theory and Practice of Delimited Continuations (TPDC","author":"James Roshan P","year":"2011","unstructured":"Roshan P James and Amr Sabry . 2011 . Yield: Mainstream delimited continuations . In First International Workshop on the Theory and Practice of Delimited Continuations (TPDC 2011). 20 pages. https:\/\/legacy.cs.indiana.edu\/~sabry\/papers\/yield.pdf Roshan P James and Amr Sabry. 2011. Yield: Mainstream delimited continuations. In First International Workshop on the Theory and Practice of Delimited Continuations (TPDC 2011). 20 pages. https:\/\/legacy.cs.indiana.edu\/~sabry\/papers\/yield.pdf"},{"key":"e_1_2_2_14_1","volume-title":"Proceedings of the 24th USENIX Conference on Security Symposium (Washington, D.C.) (SEC\u201915)","author":"Kaloper-Mer\u0161injak David","year":"2015","unstructured":"David Kaloper-Mer\u0161injak , Hannes Mehnert , Anil Madhavapeddy , and Peter Sewell . 2015 . Not-Quite-so-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation . In Proceedings of the 24th USENIX Conference on Security Symposium (Washington, D.C.) (SEC\u201915) . USENIX Association, USA, 223\u2013238. isbn:978 1931971232 David Kaloper-Mer\u0161injak, Hannes Mehnert, Anil Madhavapeddy, and Peter Sewell. 2015. Not-Quite-so-Broken TLS: Lessons in Re-Engineering a Security Protocol Specification and Implementation. In Proceedings of the 24th USENIX Conference on Security Symposium (Washington, D.C.) (SEC\u201915). USENIX Association, USA, 223\u2013238. isbn:9781931971232"},{"volume-title":"Trends in Functional Programming","author":"Kawahara Satoru","key":"e_1_2_2_15_1","unstructured":"Satoru Kawahara and Yukiyoshi Kameyama . 2020. One-Shot Algebraic Effects as Coroutines . In Trends in Functional Programming , Aleksander Byrski and John Hughes (Eds.). Springer International Publishing , Cham , 159\u2013179. isbn:978-3-030-57761-2 https:\/\/link.springer.com\/content\/pdf\/10.1007 Satoru Kawahara and Yukiyoshi Kameyama. 2020. One-Shot Algebraic Effects as Coroutines. In Trends in Functional Programming, Aleksander Byrski and John Hughes (Eds.). Springer International Publishing, Cham, 159\u2013179. isbn:978-3-030-57761-2 https:\/\/link.springer.com\/content\/pdf\/10.1007"},{"key":"e_1_2_2_16_1","unstructured":"Masashi Kikuchi. 2014. How I discovered CCS Injection Vulnerability. http:\/\/ccsinjection.lepidum.co.jp\/blog\/2014-06-05\/CCS-Injection-en\/index.html  Masashi Kikuchi. 2014. How I discovered CCS Injection Vulnerability. http:\/\/ccsinjection.lepidum.co.jp\/blog\/2014-06-05\/CCS-Injection-en\/index.html"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2804302.2804319"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294106"},{"key":"e_1_2_2_19_1","unstructured":"Adam Langley. 2014. Early ChangeCipherSpec Attack. https:\/\/www.imperialviolet.org\/2014\/06\/05\/earlyccs.html  Adam Langley. 2014. Early ChangeCipherSpec Attack. https:\/\/www.imperialviolet.org\/2014\/06\/05\/earlyccs.html"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_2_2_21_1","unstructured":"Tyler Mandry. 2019. How Rust optimizes async\/await. https:\/\/tmandry.gitlab.io\/blog\/posts\/optimizing-await-1\/ Retrieved 2020-08-20.  Tyler Mandry. 2019. How Rust optimizes async\/await. https:\/\/tmandry.gitlab.io\/blog\/posts\/optimizing-await-1\/ Retrieved 2020-08-20."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462166.1462167"},{"key":"e_1_2_2_23_1","unstructured":"Gor Nishanov. 2018. N4760: Working Draft C++ Extensions for Coroutines.  Gor Nishanov. 2018. N4760: Working Draft C++ Extensions for Coroutines."},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46666-7_4"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158524"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_7"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2018.3"},{"key":"e_1_2_2_29_1","volume-title":"Cross-Platform Cryptographic Provider. In IEEE Symposium on Security and Privacy. IEEE. https:\/\/www.microsoft.com\/en-us\/research\/publication\/evercrypt-a-fast-veri","author":"Protzenko Jonathan","year":"2020","unstructured":"Jonathan Protzenko , Bryan Parno , Aymeric Fromherz , Chris Hawblitzel , Marina Polubelova , Karthikeyan Bhargavan , Benjamin Beurdouche , Joonwon Choi , Antoine Delignat-Lavaud , C\u00e9dric Fournet , Natalia Kulatova , Tahina Ramananandro , Aseem Rastogi , Nikhil Swamy , Christoph M. Wintersteiger , and Santiago Zanella-B\u00e9guelin . 2020 . EverCrypt: A Fast, Veri\ufb01ed , Cross-Platform Cryptographic Provider. In IEEE Symposium on Security and Privacy. IEEE. https:\/\/www.microsoft.com\/en-us\/research\/publication\/evercrypt-a-fast-veri Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, C\u00e9dric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, and Santiago Zanella-B\u00e9guelin. 2020. EverCrypt: A Fast, Veri\ufb01ed, Cross-Platform Cryptographic Provider. In IEEE Symposium on Security and Privacy. IEEE. https:\/\/www.microsoft.com\/en-us\/research\/publication\/evercrypt-a-fast-veri"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454032"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_32_1","volume-title":"Coroutines: Language and Implementation Impact","author":"Smith Richard","year":"2019","unstructured":"Richard Smith , Daveed Vandevoorde , Geoffrey Romer , Gor Nishanov , Nathan Sidwell , Iain Sandoe , and Lewis Baker . 2019 . Coroutines: Language and Implementation Impact . http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2019\/p1492r0.pdf P1492 R0. Richard Smith, Daveed Vandevoorde, Geoffrey Romer, Gor Nishanov, Nathan Sidwell, Iain Sandoe, and Lewis Baker. 2019. Coroutines: Language and Implementation Impact. http:\/\/www.open-std.org\/jtc1\/sc22\/wg21\/docs\/papers\/2019\/p1492r0.pdf P1492 R0."},{"key":"e_1_2_2_33_1","volume-title":"Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. In International Symposium on Implementation and Applicationof Functional Languages (IFL\u201919)","author":"Ullrich Sebastian","year":"2020","unstructured":"Sebastian Ullrich and Leonardo de Moura . 2020 . Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. In International Symposium on Implementation and Applicationof Functional Languages (IFL\u201919) . New York, NY, USA, 12 pages. https:\/\/arxiv.org\/abs\/ 1908.05647 Sebastian Ullrich and Leonardo de Moura. 2020. Counting Immutable Beans: Reference Counting Optimized for Purely Functional Programming. In International Symposium on Implementation and Applicationof Functional Languages (IFL\u201919). New York, NY, USA, 12 pages. https:\/\/arxiv.org\/abs\/1908.05647"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"},{"key":"e_1_2_2_35_1","volume-title":"Security in Computing and Communications, Sabu M","author":"Yadav Tarun","year":"1902","unstructured":"Tarun Yadav and Koustav Sadhukhan . 2019. Identification of Bugs and Vulnerabilities in TLS Implementation for Windows Operating System Using State Machine Learning . In Security in Computing and Communications, Sabu M . Thampi, Sanjay Madria, Guojun Wang, Danda B. Rawat, and Jose M. Alcaraz Calero (Eds.). Springer Singapore , Singapore , 348\u2013362. isbn:978-981-13-5826-5 https:\/\/arxiv.org\/pdf\/ 1902 .07471.pdf Tarun Yadav and Koustav Sadhukhan. 2019. Identification of Bugs and Vulnerabilities in TLS Implementation for Windows Operating System Using State Machine Learning. In Security in Computing and Communications, Sabu M. Thampi, Sanjay Madria, Guojun Wang, Danda B. Rawat, and Jose M. Alcaraz Calero (Eds.). Springer Singapore, Singapore, 348\u2013362. isbn:978-981-13-5826-5 https:\/\/arxiv.org\/pdf\/1902.07471.pdf"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3133974"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.32"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498685","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498685","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498685","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498685"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498685"],"URL":"https:\/\/doi.org\/10.1145\/3498685","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}