Formal Verification of the Heatseeker Technique for Detection of Code-Reuse Attacks. Companion Artifact

This artifact aims to support and reproduce the verification results of the paper "Formal Verification of the Heatseeker Technique for Detection of Code-Reuse Attacks" by Téo Biton, Nikolai Kosmatov, Olivier Gilles, Daniel Gracia Pérez and Sébastien Pillement, submitted to ISoLA 2026, and should be cited as: Téo Biton, Nikolai Kosmatov, Olivier Gilles, Daniel Gracia Pérez and Sébastien Pillement. "Formal Verification of the Heatseeker Technique for Detection of Code-Reuse Attacks. Companion Artifact for the Paper Submitted to ISoLA 2026". Zenodo. https://doi.org/10.5281/zenodo.19794964 The artifact itself is available in the attached VM HeatseekerProof.ova.See the documentation in README.md in the folder /home/user/proof/ inside the VM. In the provided VM, all tools have already been installed.The VM is running Ubuntu 22.04 LTS.The VM was tested with VirtualBox 7.0.16.For information, the password of user "user" in the VM is "user". For convenience of the readers and a faster access to files, the contents of the VM are also available in the attached ZIP.The ZIP is provided for information. The artifact should be preferably used with the attached VM HeatseekerProof.ova. See the included REQUIREMENTS.md file for more detail. See the included LICENSE file for the terms of use and distribution rights, and LICENSE_cbmc.md for the CBMC license.