{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T00:14:54Z","timestamp":1777421694383,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":54,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,11,12]],"date-time":"2021-11-12T00:00:00Z","timestamp":1636675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001839","name":"University Grants Committee","doi-asserted-by":"publisher","award":["RGC R4032-18"],"award-info":[{"award-number":["RGC R4032-18"]}],"id":[{"id":"10.13039\/501100001839","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,11,12]]},"DOI":"10.1145\/3460120.3484541","type":"proceedings-article","created":{"date-parts":[[2021,11,13]],"date-time":"2021-11-13T12:05:34Z","timestamp":1636805134000},"page":"2183-2196","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":65,"title":["MirChecker: Detecting Bugs in Rust Programs via Static Analysis"],"prefix":"10.1145","author":[{"given":"Zhuohua","family":"Li","sequence":"first","affiliation":[{"name":"The Chinese University of Hong Kong, Shatin, N.T., Hong Kong"}]},{"given":"Jincheng","family":"Wang","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong, Shatin, N.T., Hong Kong"}]},{"given":"Mingshen","family":"Sun","sequence":"additional","affiliation":[{"name":"Baidu Security, Beijing, China"}]},{"given":"John C.S.","family":"Lui","sequence":"additional","affiliation":[{"name":"The Chinese University of Hong Kong, Shatin, N.T., Hong Kong"}]}],"member":"320","published-online":{"date-parts":[[2021,11,13]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2889160.2889229"},{"key":"e_1_3_2_2_2_1","volume-title":"Leveraging Rust Types for Modular Specification and Verification. Proceedings of the ACM on Programming Languages","volume":"3","author":"Astrauskas Vytautas","year":"2019","unstructured":"Vytautas Astrauskas, Peter M\u00fcller, Federico Poli, and Alexander J. Summers. 2019. Leveraging Rust Types for Modular Specification and Verification. Proceedings of the ACM on Programming Languages, Vol. 3, OOPSLA (2019), 1--30."},{"key":"e_1_3_2_2_3_1","unstructured":"Rust Fuzzing Authority. 2021. Trophy Case. https:\/\/github.com\/rust-fuzz\/trophy-case"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_32"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"crossref","unstructured":"Francc ois Bourdoncle. 1993. Efficient Chaotic Iteration Strategies with Widenings. In Formal Methods in Programming and their Applications. 128--141.","DOI":"10.1007\/BFb0039704"},{"key":"e_1_3_2_2_7_1","volume-title":"IKOS: A Framework for Static Analysis Based on Abstract Interpretation. In International Conference on Software Engineering and Formal Methods (SEFM '14)","author":"Brat Guillaume","year":"2014","unstructured":"Guillaume Brat, Jorge A Navas, Nija Shi, and Arnaud Venet. 2014. IKOS: A Framework for Static Analysis Based on Abstract Interpretation. In International Conference on Software Engineering and Formal Methods (SEFM '14). 271--277."},{"key":"e_1_3_2_2_8_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI '08)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI '08). 209--224."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_2_10_1","unstructured":"CVE Contributors. 2017. CVE-2017--1000430. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2017--1000430"},{"key":"e_1_3_2_2_11_1","unstructured":"CVE Contributors. 2019 a. CVE-2019--15552. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2019--15552"},{"key":"e_1_3_2_2_12_1","unstructured":"CVE Contributors. 2019 b. CVE-2019--15553. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2019--15553"},{"key":"e_1_3_2_2_13_1","unstructured":"CVE Contributors. 2019 c. CVE-2019--16140. https:\/\/cve.mitre.org\/cgi-bin\/cvename.cgi?name=CVE-2019--16140"},{"key":"e_1_3_2_2_14_1","unstructured":"Crab Contributors. 2021 a. CoRnucopia of ABstractions: a language-agnostic library for abstract interpretation. https:\/\/github.com\/seahorn\/crab"},{"key":"e_1_3_2_2_15_1","unstructured":"MIRAI Contributors. 2021 b. MIRAI: Rust mid-level IR Abstract Interpreter. https:\/\/github.com\/facebookexperimental\/MIRAI"},{"key":"e_1_3_2_2_16_1","unstructured":"Miri Contributors. 2021 c. Miri: An interpreter for Rust's mid-level intermediate representation. https:\/\/github.com\/rust-lang\/miri"},{"key":"e_1_3_2_2_17_1","unstructured":"RedoxOS Contributors. 2021 d. Redox OS. https:\/\/www.redox-os.org\/"},{"key":"e_1_3_2_2_18_1","volume-title":"Proceedings of the 2nd International Symposium on Programming (ISOP '76)","author":"Cousot Patrick","year":"1976","unstructured":"Patrick Cousot and Radhia Cousot. 1976. Static Determination of Dynamic Properties of Programs. In Proceedings of the 2nd International Symposium on Programming (ISOP '76). 106--130."},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/567752.567778"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512770"},{"key":"e_1_3_2_2_22_1","unstructured":"Mohan Cui Chengjun Chen Hui Xu and Yangfan Zhou. 2021. SafeDrop: Detecting Memory Deallocation Bugs of Rust Programs via Static Data-Flow Analysis. arxiv: 2103.15420 [cs.PL]"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_24_1","unstructured":"Rob DeLine and Rustan Leino. 2005. BoogiePL: A Typed Procedural Language for Checking Object-Oriented Programs. Technical Report MSR-TR-2005--70. 13 pages."},{"key":"e_1_3_2_2_25_1","unstructured":"Rust For Linux Developers. 2021. Rust for Linux. https:\/\/github.com\/Rust-for-Linux"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.65"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250784"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/502059.502041"},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380413"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-39322-9_5"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511629150.002"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1080\/00207168908803778"},{"key":"e_1_3_2_2_33_1","unstructured":"Florian Hahn. 2016. Rust2Viper: Building a Static Verifier for Rust. Master's thesis. ETH Z\u00fcrich."},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1052883.1052895"},{"key":"e_1_3_2_2_35_1","volume-title":"Apron: A Library of Numerical Abstract Domains for Static Analysis. In International Conference on Computer Aided Verification (CAV '09)","author":"Jeannet Bertrand","year":"2009","unstructured":"Bertrand Jeannet and Antoine Min\u00e9. 2009. Apron: A Library of Numerical Abstract Domains for Static Analysis. In International Conference on Computer Aided Verification (CAV '09). 661--667."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/512927.512945"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132786"},{"key":"e_1_3_2_2_40_1","volume-title":"Proceedings of the 14th International Conference on Availability, Reliability and Security (ARES '19)","author":"Li Zhuohua","unstructured":"Zhuohua Li, Jincheng Wang, Mingshen Sun, and John C.S. Lui. 2019. Securing the Device Drivers of Your Embedded Systems: Framework and Prototype. In Proceedings of the 14th International Conference on Availability, Reliability and Security (ARES '19). 1--10."},{"key":"e_1_3_2_2_41_1","volume-title":"2018 IEEE 16th International Conference on Industrial Informatics (INDIN '18)","author":"Lindner M.","unstructured":"M. Lindner, J. Aparicius, and P. Lindgren. 2018. No Panic! Verification of Rust Programs by Symbolic Execution. In 2018 IEEE 16th International Conference on Industrial Informatics (INDIN '18). 108--114."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380325"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8609-1"},{"key":"e_1_3_2_2_44_1","volume-title":"Schwartzbach","author":"M\u00f8ller Anders","year":"2018","unstructured":"Anders M\u00f8ller and Michael I. Schwartzbach. 2018. Static Program Analysis ."},{"key":"e_1_3_2_2_45_1","volume-title":"Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation -","volume":"9583","author":"M\u00fcller Peter","unstructured":"Peter M\u00fcller, Malte Schwerhoff, and Alexander J. Summers. 2016. Viper: A Verification Infrastructure for Permission-Based Reasoning. In Proceedings of the 17th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 9583 (VMCAI '16). 41--62."},{"key":"e_1_3_2_2_46_1","volume-title":"Principles of Program Analysis","author":"Nielson Flemming","unstructured":"Flemming Nielson, Hanne R. Nielson, and Chris Hankin. 2010. Principles of Program Analysis .Springer Publishing Company, Incorporated."},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386036"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1953-0053041-6"},{"key":"e_1_3_2_2_50_1","volume-title":"Crust: A Bounded Verifier for Rust. In 2015 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE '15)","author":"Toman J.","unstructured":"J. Toman, S. Pernsteiner, and E. Torlak. 2015. Crust: A Bounded Verifier for Rust. In 2015 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE '15). 75--80."},{"key":"e_1_3_2_2_51_1","unstructured":"Jeff Vander Stoep and Stephen Hines. 2021. Rust in the Android platform. https:\/\/security.googleblog.com\/2021\/04\/rust-in-android-platform.html"},{"key":"e_1_3_2_2_52_1","unstructured":"Philip Wadler. 1990. Linear Types Can Change the World!. In Programming Concepts and Methods ."},{"key":"e_1_3_2_2_53_1","volume-title":"Memory-Safety Challenge Considered Solved? An In-Depth Study with All Rust CVEs. arxiv","author":"Xu Hui","year":"2003","unstructured":"Hui Xu, Zhuangbin Chen, Mingshen Sun, Yangfan Zhou, and Michael Lyu. 2021. Memory-Safety Challenge Considered Solved? An In-Depth Study with All Rust CVEs. arxiv: 2003.03296 [cs.PL]"},{"key":"e_1_3_2_2_54_1","volume-title":"arxiv","author":"Yu Zeming","year":"1902","unstructured":"Zeming Yu, Linhai Song, and Yiying Zhang. 2019. Fearless Concurrency? Understanding Concurrent Programming Safety in Real-World Rust Software. arxiv: 1902.01906 [cs.PL]"}],"event":{"name":"CCS '21: 2021 ACM SIGSAC Conference on Computer and Communications Security","location":"Virtual Event Republic of Korea","acronym":"CCS '21","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"]},"container-title":["Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484541","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3460120.3484541","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T20:52:04Z","timestamp":1763499124000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3460120.3484541"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,12]]},"references-count":54,"alternative-id":["10.1145\/3460120.3484541","10.1145\/3460120"],"URL":"https:\/\/doi.org\/10.1145\/3460120.3484541","relation":{},"subject":[],"published":{"date-parts":[[2021,11,12]]},"assertion":[{"value":"2021-11-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}