Page 212 - 《软件学报》2025年第8期

张卓若 等: 面向 Rust 语言的形式化验证方法研究综述 3635

Verification. Koblenz: ACM, 2023. 1–8. [doi: 10.1145/3625275.3625398]
[64] LeBlanc H, Taylor N, Bornholt J, Chidambaram V. SquirrelFS: Using the Rust compiler to check file-system crash consistency. In: Proc.
of the 18th USENIX Symp. on Operating Systems Design and Implementation. Santa Clara: USENIX Association, 2024. 387–404.
[65] Jia YK, Liu S, Wang WH, Chen Y, Zhai ZD, Yan SM, He ZY. HyperEnclave: An open and cross-platform trusted execution
environment. In: Proc. of the 2022 USENIX Annual Technical Conf. Carlsbad: USENIX Association, 2022. 437–454.
[66] Dai ZY, Liu S, Sjoberg V, Li XP, Chen Y, Wang WH, Jia YK, Anderson SN, Elbeheiry L, Sondhi S, Zhang Y, Ni ZZ, Yan SM, Gu RH,
He ZY. Verifying Rust implementation of page tables in a software enclave hypervisor. In: Proc. of the 29th ACM Int’l Conf. on
Architectural Support for Programming Languages and Operating Systems. La Jolla: ACM, 2024. 1218–1232. [doi: 10.1145/3620665.
3640398]
[67] AMD. AMD secure encrypted virtualization (SEV). 2024. https://www.amd.com/zh-tw/developer/sev.html
[68] Zhou ZQ, Anjali, Chen WT, Gong SS, Hawblitzel C, Cui WD. VERISMO: A verified security module for confidential VMs. In: Proc. of
the 18th USENIX Symp. on Operating Systems Design and Implementation. Santa Clara: USENIX Association, 2024. 32.
[69] Kiefer F. evercrypt-rust. 2024. https://github.com/franziskuskiefer/evercrypt-rust
[70] Merigoux D, Kiefer F, Bhargavan K. Hacspec: Succinct, executable, verifiable specifications for high-assurance cryptography embedded
in Rust. Inria: HAL, 2021.
[71] Hax. 2023. https://github.com/hacspec/hax
[72] Chen HB, Chen HH, Sun MS, Li K, Chen ZF, Wang XF. A verified confidential computing as a service framework for privacy
preservation. In: Proc. of the 32nd USENIX Conf. on Security Symp. Anaheim: USENIX Association, 2023. 265.
[73] Njor EJ, Gústafsson H. Static taint analysis in Rust [MS. Thesis]. Aalborg: Aalborg University, 2021.
[74] Asterinas. 2024. https://github.com/asterinas/asterinas
[75] Sun XD, Ma WJ, Gu JT, Ma ZC, Chajed T, Howell J, Lattuada A, Padon O, Suresh L, Szekeres A, Xu TY. Anvil: Verifying liveness of
cluster management controllers. In: Proc. of the 18th USENIX Conf. on Operating Systems Design and Implementation. Santa Clara:
USENIX Association, 2024. 35.
[76] Ferrocene. 2024. https://ferrocene.dev/en/
[77] A-mir-formality. 2022. https://github.com/rust-lang/a-mir-formality
[78] Minirust. 2022. https://github.com/minirust/minirust
[79] Li HY, Guo LW, Yang YX, Wang SG, Xu MW. An empirical study of Rust-for-Linux: The success, dissatisfaction, and compromise. In:
Proc. of the 2024 Conf. on Usenix Annual Technical Conf. Santa Clara: USENIX Association, 2024. 27.
[80] Wang YT. Compiler validation methods for Rust core language mechanisms. 2024 (in Chinese). https://jhc.sjtu.edu.cn/~yutingwang/files/
posters/rust-hyl.pdf
[81] Zheng XY, Wan ZY, Zhang Y, Chang R, Lo D. A closer look at the security risks in the Rust ecosystem. ACM Trans. on Software
Engineering and Methodology, 2024, 33(2): 34. [doi: 10.1145/3624738]
[82] Zhao JZ, Nagarakatte S, Martin MMK, Zdancewic S. Formalizing the LLVM intermediate representation for verified program
transformations. In: Proc. of the 39th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. Philadelphia:
ACM, 2012. 427–440. [doi: 10.1145/2103656.2103709]
[83] Blazy S, Leroy X. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 2009, 43(3):
263–288. [doi: 10.1007/s10817-009-9148-3]
[84] Song PY, Yang KY, Anandkumar A. Towards large language models as copilots for theorem proving in lean. arXiv:2404.12534, 2024.
[85] Wu YH, Jiang AQ, Li WD, Rabe MN, Staats C, Jamnik M, Szegedy C. Autoformalization with large language models. In: Proc. of the
36th Int’l Conf. on Neural Information Processing Systems. New Orleans, 2022. 32353–32368.
[86] Jiang AQ, Welleck S, Zhou JP, Li WD, Liu JC, Jamnik M, Lacroix T, Wu YH, Lample G. Draft, sketch, and prove: Guiding formal
theorem provers with informal proofs. arXiv:2210.12283, 2022.
[87] Sunday E. Using Kani to write and validate Rust code with ChatGPT. 2023. https://blog.logrocket.com/using-kani-write-validate-rust-
code-chatgpt
[88] Sun CY, Sheng Y, Padon O, Barrett C. Clover: Closed-loop verifiable code generation. In: Proc. of the 1st Int’l Symp. on AI Verification.
Montreal: Springer, 2024. 134–155.

附中文参考文献:
[11] 胡霜, 华保健, 欧阳婉容, 樊淇梁. Rust 语言安全研究综述. 信息安全学报, 2023, 8(6): 64–83. [doi: 10.19363/J.cnki.cn10-1380/tn.