Repository navigation
Add support for indirect branch tracking (IBT) #556
Description
On newer Intel x86/64 CPUs and on OpenBSD, CompCert produced binaries will crash due to lack of IBT support. As a quick solution we can append “-z nobtcfi” to clinker_options in configure to disable IBT safeguards. However a preferable solution would be to add support for IBT on this platform. This can be partially solved by outputting “endbr64” after “.cfi_startproc” in backend/Printasmaux.ml. And then all that should be left is solving for jump tables. Thank you.
Activity
xavierleroy commentedon Jul 28, 2025
See #557 for a tentative implementation of IBT.
didickman commentedon Jul 28, 2025
Works nicely for me in my basic testing with an intel CPU that supports IBT. Responding to the note about x86/32 -- indeed OpenBSD does not implement IBT for legacy 32-bit x86 either. Only 64-bit systems have IBT/BTI. Would be great to merge this pull request when ready. Thanks!
xavierleroy commentedon Aug 29, 2025
I'm late on the next release of CompCert and #557 is not as ready to be merged as I would like. As a temporary measure, I added
-z nobtcfito the linker options on x86 BSD, commit d5dcac4 . I'll restart #557 later.monniaux commentedon Sep 9, 2025
@didickman Would what is done in Chamois suit your needs?
https://gricad-gitlab.univ-grenoble-alpes.fr/certicompil/Chamois-CompCert
didickman commentedon Sep 9, 2025
Extremely interesting project! Thanks for sharing! I will definitely take a look into this. In case of interest I am using CompCert on the industrial use side not for research.
monniaux commentedon Sep 9, 2025
@didickman We support branch target protection and other countermeasures on AArch64 and x86(-64). Feel free to contact me (email) if interested.