DROPS

Document

DOI: 10.4230/LIPIcs.FSTTCS.2025.44

Fall-Through Semantics for Mitigating Timing-Based Side Channel Leaks

Authors: Aniket Mishra and Abhishek Bichhawat

Published in: LIPIcs, Volume 360, 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)

Abstract

With the recent advent of exploits like Spectre and Meltdown, the mitigation of side-channel attacks has become an important concern for security researchers. In this paper, we focus on timing-based side channels introduced through conditional branching on secret information within programs. We introduce a language that allows a programmer to write conditionals branching on secrets within its syntax, but has a semantics that keeps execution time constant with respect to an adversary under an observationally equivalent memory. We differ from other approaches that use program analysis methods, opting instead to modify the operational semantics to enforce the necessary properties. We formalize the semantics for our language with timing leak mitigations in Rocq (previously, Coq) and prove that these semantics satisfy the property of timing-sensitive non-interference. Since our system describes a mitigation approach for timing leaks in a general high-level imperative language, we believe that our semantics can be used as a basis for compiler construction for other high-level imperative languages that seek to be safe from timing side channels.

Cite as

Aniket Mishra and Abhishek Bichhawat. Fall-Through Semantics for Mitigating Timing-Based Side Channel Leaks. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 360, pp. 44:1-44:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{mishra_et_al:LIPIcs.FSTTCS.2025.44,
  author =	{Mishra, Aniket and Bichhawat, Abhishek},
  title =	{{Fall-Through Semantics for Mitigating Timing-Based Side Channel Leaks}},
  booktitle =	{45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2025)},
  pages =	{44:1--44:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-406-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{360},
  editor =	{Aiswarya, C. and Mehta, Ruta and Roy, Subhajit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2025.44},
  URN =		{urn:nbn:de:0030-drops-251249},
  doi =		{10.4230/LIPIcs.FSTTCS.2025.44},
  annote =	{Keywords: Timing leaks, information flow control, runtime monitor, type system, side-channel attacks}
}

Search Results

Documents authored by Bichhawat, Abhishek

Fall-Through Semantics for Mitigating Timing-Based Side Channel Leaks

Abstract

Cite as

Thanks for your feedback!

Could not send message