2026-08-19T12:38:22Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24629 2025-09-22T06:50:21Z ddc:004 open_access

On Verifying Secret Control Flow Elimination Knothe, David Bringmann, Oliver CompCert small-step linearization side-channels constant-time verification security taint analysis Many countermeasures against timing side-channel attacks have been developed in recent years, including tools to verify that code or a binary is constant-time, compilers or languages that compile into constant-time code, and a formal verification of a compiler that retains the constant-time property. We take a first step toward formally verifying a C compiler that eliminates control-flow-induced timing side channels. Specifically, we extend CompCert with Partial Control-Flow Linearization (PCFL) [Simon Moll and Sebastian Hack, 2018], a global if-conversion algorithm that was repurposed by Soares et al. [Luigi Soares et al., 2023] for removing timing side channels. Our transformation is split into multiple steps, separating linearization from instruction predication. One of the intermediate states contains the current program points before and after linearization simultaneously and we exploit a postdominance relation between those to show semantic preservation. We give a new proof that PCFL leaves uniform program points untouched and use it to show that our transformation correctly eliminates all secret control flow. Although our transformation currently only supports a subset of C, making it unsuitable for use in production, it gives an insight into how a global graph-based linearization technique like PCFL can be verified in CompCert and thereby shows the challenges and obstacles of this undertaking. Schloss Dagstuhl – Leibniz-Zentrum für Informatik David Knothe and Oliver Bringmann 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.31 urn:nbn:de:0030-drops-246299 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.31 eng https://creativecommons.org/licenses/by/4.0/legalcode