The Trusted Computing Base of the CompCert Verified Compiler
David Monniaux (VERIMAG - IMAG), Sylvain Boulm\'e (VERIMAG - IMAG)
TL;DR
This paper critically examines the security and correctness of the CompCert verified compiler by analyzing potential loopholes and vulnerabilities in its formal verification process.
Contribution
It provides a comprehensive analysis of possible errors and loopholes in the formal verification of CompCert, highlighting areas for improvement.
Findings
Identifies potential modeling errors in source and target languages
Highlights risks in external algorithm calls within the compiler
Suggests areas for strengthening the compiler's formal guarantees
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Advanced Malware Detection Techniques · Adversarial Robustness in Machine Learning