{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,12]],"date-time":"2025-12-12T13:45:48Z","timestamp":1765547148270,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":22,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819983100"},{"type":"electronic","value":"9789819983117"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,11,21]],"date-time":"2023-11-21T00:00:00Z","timestamp":1700524800000},"content-version":"vor","delay-in-days":324,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Most of the existing work on verified compilation leaves unverified the translation of assembly programs into binary code in object file formats (e.g., the Executable and Linkable Format or ELF). The challenges of developing verified assemblers come from the intrinsic complexities in low-level assembling processes caused by the need to support different computer architectures and their details, such as encoding a large number of instructions and verifying its correctness. We present a framework that overcomes the above challenges. It works as a template which may be instantiated to generate verified assemblers for different architectures targeting ELF object files. For this, it is parameterized over the implementation and verification of architecture-dependent assembling processes through well-defined interfaces. By plugging the architecture-dependent parts into the template, we get complete verified assemblers. To manage the complexity in developing and verifying encoding of instructions, we integrate into our framework the CSLED framework for automatically generating verified instruction encoders and decoders from declarative instruction specifications. To show the effectiveness of our framework, we have applied it to generate verified assemblers for the complete X86 and RISC-V assembly languages in CompCert.<\/jats:p>","DOI":"10.1007\/978-981-99-8311-7_10","type":"book-chapter","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T07:02:17Z","timestamp":1700636537000},"page":"205-224","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards a\u00a0Framework for\u00a0Developing Verified Assemblers for\u00a0the\u00a0ELF Format"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5812-053X","authenticated-orcid":false,"given":"Jinhua","family":"Wu","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3990-2418","authenticated-orcid":false,"given":"Yuting","family":"Wang","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0007-8876-3406","authenticated-orcid":false,"given":"Meng","family":"Sun","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6619-781X","authenticated-orcid":false,"given":"Xiangzhe","family":"Xu","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0003-2445-8403","authenticated-orcid":false,"given":"Yichen","family":"Song","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"doi-asserted-by":"publisher","unstructured":"Appel, A.W.: Foundational proof-carrying code. In: Proceedings of 31st IEEE Symposium on Logic in Computer Science (LICS\u201916), pp. 247\u2013256. IEEE Computer Society, Boston (2001). https:\/\/doi.org\/10.1109\/LICS.2001.932501","key":"10_CR1","DOI":"10.1109\/LICS.2001.932501"},{"doi-asserted-by":"publisher","unstructured":"Armstrong, A., et al.: Isa semantics for armv8-a, risc-v, and cheri-mips. Proc. ACM Program. Lang. 3(POPL), 71:1\u201371:31 (2019). https:\/\/doi.org\/10.1145\/3290384","key":"10_CR2","DOI":"10.1145\/3290384"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-319-66107-0_6","volume-title":"Interactive Theorem Proving","author":"F Besson","year":"2017","unstructured":"Besson, F., Blazy, S., Wilke, P.: CompCertS: a memory-aware verified C compiler using pointer as integer semantics. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 81\u201397. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_6"},{"doi-asserted-by":"publisher","unstructured":"Kang, J., Hur, C.K., Mansky, W., Garbuzov, D., Zdancewic, S., Vafeiadis, V.: A formal c memory model supporting integer-pointer casts. In: Proceedings of 2015 ACM Conference on Programming Language Design and Implementation (PLDI 2015), pp. 326\u2013335. ACM, New York (2015). https:\/\/doi.org\/10.1145\/2737924.2738005","key":"10_CR4","DOI":"10.1145\/2737924.2738005"},{"unstructured":"K\u00e4stner, D., et al.: Compcert: practical experience on integrating and qualifying a formally verified optimizing compiler. In: Proceedings of 9th European Congress Embedded Real-Time Software and Systems, pp. 1\u20139. SEE (2018)","key":"10_CR5"},{"doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: Cakeml: a verified implementation of ml. In: Proceedings of 41st ACM Symposium on Principles of Programming Languages (POPL 2014), pp. 179\u2013191. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","key":"10_CR6","DOI":"10.1145\/2535838.2535841"},{"unstructured":"Leroy, X.: The CompCert Verified Compiler (2005-2023). http:\/\/compcert.inria.fr\/","key":"10_CR7"},{"issue":"4","key":"10_CR8","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9155-4","journal-title":"J. Autom. Reason."},{"unstructured":"Leroy, X., Appel, A.W., Blazy, S., Stewart, G.: The CompCert Memory Model, Version 2. Research Report RR-7987, INRIA (2012). https:\/\/hal.inria.fr\/hal-00703441","key":"10_CR9"},{"issue":"1","key":"10_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"X Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformation. J. Autom. Reason. 41(1), 1\u201331 (2008). https:\/\/doi.org\/10.1007\/s10817-008-9099-0","journal-title":"J. Autom. Reason."},{"unstructured":"Morrisett, G., et al.: TALx86: a realistic typed assembly language. In: 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pp. 25\u201335. Atlanta, GA, USA (1999)","key":"10_CR11"},{"issue":"3","key":"10_CR12","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1145\/319301.319345","volume":"21","author":"JG Morrisett","year":"1999","unstructured":"Morrisett, J.G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM Trans. Program. Lang. Syst. 21(3), 527\u2013568 (1999). https:\/\/doi.org\/10.1145\/319301.319345","journal-title":"ACM Trans. Program. Lang. Syst."},{"doi-asserted-by":"publisher","unstructured":"Mullen, E., Zuniga, D., Tatlock, Z., Grossman, D.: Verified peephole optimizations for compcert. In: Proceedings of 2016 ACM Conference on Programming Language Design and Implementation (PLDI 2016). pp. 448\u2013461. ACM, New York (2016). https:\/\/doi.org\/10.1145\/2980983.2908109","key":"10_CR13","DOI":"10.1145\/2980983.2908109"},{"doi-asserted-by":"publisher","unstructured":"Necula, G.: Proof-carrying code. In: Proceedings of 24th ACM Symposium on Principles of Programming Languages (POPL 1997), pp. 106\u2013119. ACM, New York (1997). https:\/\/doi.org\/10.1145\/263699.263712","key":"10_CR14","DOI":"10.1145\/263699.263712"},{"issue":"3","key":"10_CR15","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1145\/256167.256225","volume":"19","author":"N Ramsey","year":"1997","unstructured":"Ramsey, N., Fern\u00e1ndez, M.F.: Specifying representations of machine instructions. ACM Trans. Program. Lang. Syst. 19(3), 492\u2013524 (1997). https:\/\/doi.org\/10.1145\/256167.256225","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR16","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000229","volume":"29","author":"YK Tan","year":"2019","unstructured":"Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A.C.J., Owens, S., Norrish, M.: The verified cakeml compiler backend. J. Funct. Program. 29, e2 (2019). https:\/\/doi.org\/10.1017\/S0956796818000229","journal-title":"J. Funct. Program."},{"unstructured":"The Coq development team: The Coq proof assistant (1999 - 2023). http:\/\/coq.inria.fr","key":"10_CR17"},{"unstructured":"The GNU development team: GNU Binutils (2000 - 2023). https:\/\/sourceware.org\/binutils\/","key":"10_CR18"},{"doi-asserted-by":"publisher","unstructured":"Wang, Y., Wilke, P., Shao, Z.: An abstract stack based approach to verified compositional compilation to machine code. Proc. ACM Program. Lang. 3(POPL), 62:1\u201362:30 (2019). https:\/\/doi.org\/10.1145\/3290375","key":"10_CR19","DOI":"10.1145\/3290375"},{"doi-asserted-by":"publisher","unstructured":"Wang, Y., Xu, X., Wilke, P., Shao, Z.: Compcertelf: verified separate compilation of c programs into elf object files. Proc. ACM Program. Lang. 4(OOPSLA) 197, 1\u2013197:28 (2020). https:\/\/doi.org\/10.1145\/3428265","key":"10_CR20","DOI":"10.1145\/3428265"},{"doi-asserted-by":"publisher","unstructured":"Wang, Y., Zhang, L., Shao, Z., Koenig, J.: Verified compilation of C programs with a nominal memory model. Proc. ACM Program. Lang. 6(POPL), 1\u201331 (2022). https:\/\/doi.org\/10.1145\/3498686","key":"10_CR21","DOI":"10.1145\/3498686"},{"key":"10_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"728","DOI":"10.1007\/978-3-030-81688-9_34","volume-title":"Computer Aided Verification","author":"X Xu","year":"2021","unstructured":"Xu, X., Wu, J., Wang, Y., Yin, Z., Li, P.: Automatic generation and validation of instruction encoders and decoders. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 728\u2013751. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_34"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-99-8311-7_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T07:02:32Z","timestamp":1700636552000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-99-8311-7_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9789819983100","9789819983117"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-981-99-8311-7_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2023","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":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","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":"15","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":"47% - 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":"4","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)"}}]}}