{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T15:34:39Z","timestamp":1743003279363,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031711763"},{"type":"electronic","value":"9783031711770"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Rust has gained popularity as a safer alternative to C\/C++ for low-level programming due to its memory-safety features and minimal runtime overhead. However, the use of the \u201cunsafe\u201d keyword allows developers to bypass safety guarantees, posing memory-safety risks. Bounded Model Checking (BMC) is commonly used to detect memory-safety problems, but it has limitations for large-scale programs, as it can only detect bugs within a bounded number of executions.<\/jats:p><jats:p>In this paper, we introduce <jats:italic>UnsafeCop<\/jats:italic> that utilizes and enhances BMC for analyzing memory safety in real-world unsafe Rust code. Our methodology incorporates harness design, loop bound inference, and both loop and function stubbing for comprehensive analysis. We optimize verification efficiency through a strategic function verification order, leveraging both types of stubbing. We conducted a case study on TECC (Trusted-Environment-based Cryptographic Computing), a proprietary framework consisting of 30,174 lines of Rust code, including 3,019 lines of unsafe Rust code, developed by Ant Group. Experimental results demonstrate that <jats:italic>UnsafeCop<\/jats:italic> effectively detects and verifies dozens of memory safety issues, reducing verification time by 73.71% compared to the traditional non-stubbing approach, highlighting its practical effectiveness.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_19","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"307-324","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["UnsafeCop: Towards Memory Safety for\u00a0Real-World Unsafe Rust Code with\u00a0Practical Bounded Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2270-2076","authenticated-orcid":false,"given":"Minghua","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0380-3506","authenticated-orcid":false,"given":"Jingling","family":"Xue","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-5659-1471","authenticated-orcid":false,"given":"Lin","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yuan","family":"Zi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tao","family":"Wei","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"19_CR1","doi-asserted-by":"publisher","first-page":"100635","DOI":"10.1016\/j.softx.2020.100635","volume":"12","author":"L Ardito","year":"2020","unstructured":"Ardito, L., et al.: Rust-code-analysis: a rust library to analyze and extract maintainability information from source codes. SoftwareX 12, 100635 (2020). https:\/\/doi.org\/10.1016\/j.softx.2020.100635","journal-title":"SoftwareX"},{"key":"19_CR2","doi-asserted-by":"publisher","unstructured":"Astrauskas, V., et al.: The prusti project: formal verification for rust. In: NASA Formal Methods Symposium, pp. 88\u2013108. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_5","DOI":"10.1007\/978-3-031-06773-0_5"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Astrauskas, V., Matheja, C., Poli, F., M\u00fcller, P., Summers, A.J.: How do programmers use unsafe rust? Proceedings of the ACM on programming languages 4, 1 \u2013 27 (2020). https:\/\/api.semanticscholar.org\/CorpusID:220859132","DOI":"10.1145\/3428204"},{"key":"19_CR4","unstructured":"Biere, A., Fleury, M., Heisinger, M.: CaDiCaL, Kissat, Paracooba entering the SAT Competition 2021. In: Balyo, T., Froleyks, N., Heule, M., Iser, M., J\u00e4rvisalo, M., Suda, M. (eds.) Proc.\u00a0of SAT Competition 2021 \u2013 Solver and Benchmark Descriptions. Department of Computer Science Report Series B, vol. B-2021-1, pp. 10\u201313. University of Helsinki (2021)"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proceedings of the 2nd International Symposium on Programming, Paris, France, pp. 106\u2013130. Dunod (1976)","DOI":"10.1145\/390018.808314"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"19_CR7","doi-asserted-by":"publisher","unstructured":"Cui, M., Chen, C., Xu, H., Zhou, Y.: Safedrop: detecting memory deallocation bugs of rust programs via static data-flow analysis. ACM Trans. Softw. Eng. Methodol. 32(4) (2023). https:\/\/doi.org\/10.1145\/3542948","DOI":"10.1145\/3542948"},{"key":"19_CR8","doi-asserted-by":"publisher","unstructured":"Denis, X., Jourdan, J.H., March\u00e9, C.: Creusot: a foundry for the deductive verification of rust programs. In: International Conference on Formal Engineering Methods, pp. 90\u2013105. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17244-1_6","DOI":"10.1007\/978-3-031-17244-1_6"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Ebert, C., Cain, J., Antoniol, G., Counsell, S., Laplante, P.: Cyclomatic complexity. IEEE Softw. 33(6), 27\u201329 (2016)","DOI":"10.1109\/MS.2016.147"},{"key":"19_CR10","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: International Conference on Computer Aided Verification, pp. 343\u2013361. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_20","DOI":"10.1007\/978-3-319-21690-4_20"},{"key":"19_CR11","unstructured":"Halstead, M.H.: Elements of Software Science (Operating and programming systems series), Elsevier Science Inc. (1977)"},{"key":"19_CR12","unstructured":"Harmonic mean. https:\/\/en.wikipedia.org\/wiki\/Harmonic_mean"},{"key":"19_CR13","unstructured":"H\u00f6ltervennhoff, S., Klostermeyer, P., W\u00f6hler, N., Acar, Y., Fahl, S.: $$\\{$$\u201cI$$\\}$$ wouldn\u2019t want my unsafe code to run my $$\\{$$pacemaker\u201d$$\\}$$: an interview study on the use, comprehension, and perceived risks of unsafe rust. In: 32nd USENIX Security Symposium (USENIX Security 23), pp. 2509\u20132525 (2023)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: Rustbelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2(POPL), 1\u201334 (2017)","DOI":"10.1145\/3158154"},{"key":"19_CR15","unstructured":"Kani rust verifier. https:\/\/github.com\/model-checking\/kani"},{"key":"19_CR16","doi-asserted-by":"publisher","unstructured":"Kroening, D., Tautschnig, M.: CBMC\u2013C bounded model checker: (competition contribution). In: Tools and Algorithms for the Construction and Analysis of Systems: 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings 20, pp. 389\u2013391. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_26","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Li, Z., Wang, J., Sun, M., Lui, J.C.: Mirchecker: detecting bugs in rust programs via static analysis. In: Proceedings of the 2021 ACM SIGSAC conference on computer and communications security, pp. 2183\u20132196 (2021)","DOI":"10.1145\/3460120.3484541"},{"key":"19_CR18","doi-asserted-by":"publisher","unstructured":"Li, Z., Wang, J., Sun, M., Lui, J.C.: Detecting cross-language memory management issues in rust. In: European Symposium on Research in Computer Security. pp. 680\u2013700. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-17143-7_33","DOI":"10.1007\/978-3-031-17143-7_33"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Lindner, M., Aparicius, J., Lindgren, P.: No panic! verification of rust programs by symbolic execution. In: 2018 IEEE 16th International Conference on Industrial Informatics (INDIN, pp. 108\u2013114. IEEE (2018)","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Matsushita, Y., Denis, X., Jourdan, J.H., Dreyer, D.: Rusthornbelt: a semantic foundation for functional verification of rust programs with unsafe code. In: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pp. 841\u2013856 (2022)","DOI":"10.1145\/3519939.3523704"},{"issue":"4","key":"19_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3462205","volume":"43","author":"Y Matsushita","year":"2021","unstructured":"Matsushita, Y., Tsukada, T., Kobayashi, N.: Rusthorn: CHC-based verification for rust programs. ACM Trans. Program. Lang. Syst. (TOPLAS) 43(4), 1\u201354 (2021)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"19_CR22","unstructured":"Mirai: Rust mid-level IR abstract interpreter. https:\/\/github.com\/facebookexperimental\/MIRA"},{"key":"19_CR23","unstructured":"Miri: an interpreter for rust\u2019s mid-level intermediate representation. https:\/\/github.com\/rust-lang\/miri"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Qin, B., Chen, Y., Yu, Z., Song, L., Zhang, Y.: Understanding memory and thread safety practices and issues in real-world rust programs. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 763\u2013779 (2020)","DOI":"10.1145\/3385412.3386036"},{"key":"19_CR25","doi-asserted-by":"publisher","unstructured":"Rakamari\u0107, Z., Emmi, M.: Smack: decoupling source language details from verifier implementations. In: Computer Aided Verification: 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings 26, pp. 106\u2013113. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_7","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"19_CR26","unstructured":"Rust verification tools. https:\/\/project-oak.github.io\/rust-verification-tools\/about.html"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Shen, Y., et al.: Occlum: Secure and efficient multitasking inside a single enclave of intel sgx. In: Proceedings of the Twenty-Fifth International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 955\u2013970 (2020)","DOI":"10.1145\/3373376.3378469"},{"key":"19_CR28","unstructured":"Tomb, A.: Crux: Introducing our new open-source tool for software verification (2020)"},{"key":"19_CR29","unstructured":"Trustinsoft analyzer. https:\/\/trust-in-soft.com"},{"key":"19_CR30","unstructured":"Ullrich, S.: Simple verification of rust programs via functional purification, Master\u2019s Thesis, Karlsruher Institut fr Technologie (KIT) (2016)"},{"key":"19_CR31","unstructured":"Unsafe superpowers. https:\/\/doc.rust-lang.org\/book\/ch19-01-unsafe-rust.html"},{"key":"19_CR32","doi-asserted-by":"crossref","unstructured":"Wang, H., et al.: Towards memory safe enclave programming with rust-sgx. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp. 2333\u20132350 (2019)","DOI":"10.1145\/3319535.3354241"},{"key":"19_CR33","unstructured":"Xu, H., Chen, Z., Sun, M., Zhou, Y., Lyu, M.: Memory-safety challenge considered solved. Empirical Study Rust CVEs. CoRR, abs\/2003.03296 (2020)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:13:48Z","timestamp":1726121628000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}