CompCert验证认证器的可信计算基础
The Trusted Computing Base of the CompCert Verified Compiler
摘要：
CompCert是第一个现实的正式验证编译器：它提供了一个机器检查的数学证明，证明它生成的代码与源代码匹配。然而，这种做法可能存在漏洞。我们全面分析了CompCert的错误可能导致生成错误代码的方面。可能的问题包括从源语言和目标语言的建模到用于从编译器内部调用外部算法的某些技术。
英文摘要：
CompCert is the first realistic formally verified compiler: it provides a machine-checked mathematical proof that the code it generates matches the source code. Yet, there could be loopholes in this approach. We comprehensively analyze aspects of CompCert where errors could lead to incorrect code being generated. Possible issues range from the modeling of the source and the target languages to some techniques used to call external algorithms from within the compiler.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
