Search Results

Documents authored by Bringmann, Oliver

Document
DOI: 10.4230/LIPIcs.ITP.2025.31
On Verifying Secret Control Flow Elimination

Authors: David Knothe and Oliver Bringmann

Published in: LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025)

Abstract
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.
Cite as

David Knothe and Oliver Bringmann. On Verifying Secret Control Flow Elimination. In 16th International Conference on Interactive Theorem Proving (ITP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 352, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{knothe_et_al:LIPIcs.ITP.2025.31,
  author =	{Knothe, David and Bringmann, Oliver},
  title =	{{On Verifying Secret Control Flow Elimination}},
  booktitle =	{16th International Conference on Interactive Theorem Proving (ITP 2025)},
  pages =	{31:1--31:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-396-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{352},
  editor =	{Forster, Yannick and Keller, Chantal},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.31},
  URN =		{urn:nbn:de:0030-drops-246299},
  doi =		{10.4230/LIPIcs.ITP.2025.31},
  annote =	{Keywords: CompCert, small-step, linearization, side-channels, constant-time, verification, security, taint analysis}
}
Document
DOI: 10.4230/DagSemProc.08141.6
Current state of ASoC design methodology

Authors: Andreas Bernauer, Dirk Fritz, Björn Sander, Oliver Bringmann, and Wolfgang Rosenstiel

Published in: Dagstuhl Seminar Proceedings, Volume 8141, Organic Computing - Controlled Self-organization (2008)

Abstract
This paper gives an overview of the current state of ASoC design methodology and presents preliminary results on evaluating the learning classifier system XCS for the control of a QuadCore. The ASoC design methodology can determine system reliability based on activity, power and temperature analysis, together with reliability block diagrams. The evaluation of the XCS shows that in the evaluated setup, XCS can find optimal operating points, even in changed environments or with changed reward functions. This even works, though limited, without the genetic algorithm the XCS uses internally. The results motivate us to continue the evaluation for more complex setups.
Cite as

Andreas Bernauer, Dirk Fritz, Björn Sander, Oliver Bringmann, and Wolfgang Rosenstiel. Current state of ASoC design methodology. In Organic Computing - Controlled Self-organization. Dagstuhl Seminar Proceedings, Volume 8141, pp. 1-17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)

Copy BibTex To Clipboard

@InProceedings{bernauer_et_al:DagSemProc.08141.6,
  author =	{Bernauer, Andreas and Fritz, Dirk and Sander, Bj\"{o}rn and Bringmann, Oliver and Rosenstiel, Wolfgang},
  title =	{{Current state of ASoC design methodology}},
  booktitle =	{Organic Computing - Controlled Self-organization},
  pages =	{1--17},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8141},
  editor =	{Kirstie Bellman and Michael G. Hinchey and Christian M\"{u}ller-Schloer and Hartmut Schmeck and Rolf W\"{u}rtz},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.08141.6},
  URN =		{urn:nbn:de:0030-drops-15646},
  doi =		{10.4230/DagSemProc.08141.6},
  annote =	{Keywords: Dagstuhl Seminar Proceedings, System-on-Chip, design methodology, system reliability, learning classifier system, XCS, ASoC}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact