Document Open Access Logo

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

Authors Aniket Mishra , Abhishek Bichhawat

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSTTCS.2025.44.pdf
  • Filesize: 0.78 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Operational semantics
  • Theory of computation → Logic and verification
Keywords
  • Timing leaks
  • information flow control
  • runtime monitor
  • type system
  • side-channel attacks

Metrics

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 Get BibTex

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) https://doi.org/10.4230/LIPIcs.FSTTCS.2025.44

Author Details

Aniket Mishra
  • Indian Institute of Technology Gandhinagar, India
Abhishek Bichhawat
  • Indian Institute of Technology Gandhinagar, India

Funding

This work is funded in part by the DST Inspire Faculty Fellowship and the SERB Startup Research Grant.

Acknowledgements

We would like to thank the anonymous reviewers for their feedback on this work.

Supplementary Materials

References

  1. Johan Agat. Transforming out timing leaks. In Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '00, pages 40-53, New York, NY, USA, 2000. Association for Computing Machinery. URL: https://doi.org/10.1145/325694.325702.
  2. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, and Pierre-Yves Strub. Jasmin: High-Assurance and High-Speed Cryptography. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pages 1807-1823, Dallas Texas USA, October 2017. ACM. URL: https://doi.org/10.1145/3133956.3134078.
  3. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. Verifying constant-time implementations. In Proceedings of the 25th USENIX Conference on Security Symposium, SEC'16, pages 53-70, USA, 2016. USENIX Association. event-place: Austin, TX, USA. URL: https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida.
  4. Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, and Swarn Priya. Enforcing fine-grained constant-time policies. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS '22, pages 83-96, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3548606.3560689.
  5. Timos Antonopoulos, Paul Gazzillo, Michael Hicks, Eric Koskinen, Tachio Terauchi, and Shiyi Wei. Decomposition instead of self-composition for proving the absence of timing channels. In Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 362-375, Barcelona Spain, June 2017. ACM. URL: https://doi.org/10.1145/3062341.3062378.
  6. Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, and Vincent Laporte. Preservation of speculative constant-time by compilation. Proc. ACM Program. Lang., 9(POPL), January 2025. URL: https://doi.org/10.1145/3704880.
  7. Thomas H. Austin and Cormac Flanagan. Efficient purely-dynamic information flow analysis. In Proc. ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security, pages 113-124, 2009. URL: https://doi.org/10.1145/1554339.1554353.
  8. J. Bacelar Almeida, Manuel Barbosa, Jorge S. Pinto, and Bárbara Vieira. Formal verification of side-channel countermeasures using self-composition. Science of Computer Programming, 78(7):796-812, July 2013. URL: https://doi.org/10.1016/j.scico.2011.10.008.
  9. Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, and Peter Schwabe. High-Assurance Cryptography in the Spectre Era. In S&P 2021 - IEEE Symposium of Security and Privacy, Virtual, France, May 2021. URL: https://doi.org/10.1109/SP40001.2021.00046.
  10. Gilles Barthe, Benjamin Grégoire, and Vincent Laporte. Secure compilation of side-channel countermeasures: The case of cryptographic “constant-time”. In 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pages 328-343, 2018. URL: https://doi.org/10.1109/CSF.2018.00031.
  11. Iulia Basys, Maximilian Algehed, Alexander Sjösten, and Andrei Sabelfeld. Secwasm: Information flow control for webassembly. In Gagandeep Singh and Caterina Urban, editors, Static Analysis, pages 74-103, Cham, 2022. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-22308-2_5.
  12. Pietro Borrello, Daniele Cono D'Elia, Leonardo Querzoni, and Cristiano Giuffrida. Constantine: Automatic side-channel resistance using efficient control and data flow linearization. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, CCS '21, pages 715-733, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3460120.3484583.
  13. Robert Brotzman, Shen Liu, Danfeng Zhang, Gang Tan, and Mahmut Kandemir. Casym: Cache aware symbolic execution for side channel detection and mitigation. In 2019 IEEE Symposium on Security and Privacy (SP), pages 505-521, 2019. URL: https://doi.org/10.1109/SP.2019.00022.
  14. Luwei Cai, Fu Song, and Taolue Chen. Towards efficient verification of constant-time cryptographic implementations. Proc. ACM Softw. Eng., 1(FSE), July 2024. URL: https://doi.org/10.1145/3643772.
  15. Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. Constant-time foundations for the new spectre era. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020, pages 913-926, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3385412.3385970.
  16. Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, and Deian Stefan. Fact: a dsl for timing-sensitive computation. In Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, pages 174-189, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3314221.3314605.
  17. Jia Chen, Yu Feng, and Isil Dillig. Precise Detection of Side-Channel Vulnerabilities using Quantitative Cartesian Hoare Logic. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, pages 875-890, Dallas Texas USA, October 2017. ACM. URL: https://doi.org/10.1145/3133956.3134058.
  18. Goran Doychev, Boris Köpf, Laurent Mauborgne, and Jan Reineke. Cacheaudit: A tool for the static analysis of cache side channels. ACM Trans. Inf. Syst. Secur., 18(1), June 2015. URL: https://doi.org/10.1145/2756550.
  19. Xaver Fabian, Marco Patrignani, Marco Guarnieri, and Michael Backes. Do you even lift? strengthening compiler security guarantees against spectre attacks. Proc. ACM Program. Lang., 9(POPL), January 2025. URL: https://doi.org/10.1145/3704867.
  20. Lukas Gerlach, Robert Pietsch, and Michael Schwarz. Do compilers break constant-time guarantees? In Financial Cryptography and Data Security (FC), 2025. Google Scholar
  21. Joseph A. Goguen and José Meseguer. Security policies and security models. In Proc. 1982 IEEE Symposium on Security and Privacy, pages 11-20, 1982. URL: https://doi.org/10.1109/SP.1982.10014.
  22. Guidelines for mitigating timing side channels against cryptographic implementations. https://www.intel.com/content/www/us/en/developer/articles/technical/software-security-guidance/secure-coding/mitigate-timing-side-channel-crypto-implementation.html, 2022.
  23. Liyan Huang, Junzhou He, Chao Wang, and Weihang Wang. Wascr: A webassembly instruction-timing side channel repairer. In Proceedings of the ACM on Web Conference 2025, WWW '25, pages 4562-4571, New York, NY, USA, 2025. Association for Computing Machinery. URL: https://doi.org/10.1145/3696410.3714693.
  24. Paul C. Kocher. Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems. In Proceedings of the 16th Annual International Cryptology Conference on Advances in Cryptology, CRYPTO '96, pages 104-113, Berlin, Heidelberg, 1996. Springer-Verlag. URL: https://doi.org/10.1007/3-540-68697-5_9.
  25. Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi, Marco Patrignani, Marco Vassena, Ranjit Jhala, and Deian Stefan. Robust constant-time cryptography. Proc. ACM Program. Lang., 9(PLDI), June 2025. URL: https://doi.org/10.1145/3729310.
  26. Rui Lima, João F. Ferreira, and Alexandra Mendes. Automatic repair of java code with timing side-channel vulnerabilities. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering Workshops (ASEW), pages 1-8, 2021. URL: https://doi.org/10.1109/ASEW52652.2021.00014.
  27. Cong Ma, Dinghao Wu, Gang Tan, Mahmut Taylan Kandemir, and Danfeng Zhang. Quantifying and mitigating cache side channel leakage with differential set. Proc. ACM Program. Lang., 7(OOPSLA2), October 2023. URL: https://doi.org/10.1145/3622850.
  28. Machine checked proofs. https://anonymous.4open.science/r/timing-side-channels-47BE, 2025.
  29. David Molnar, Matt Piotrowski, David Schultz, and David Wagner. The program counter security model: automatic detection and removal of control-flow side channel attacks. In Proceedings of the 8th International Conference on Information Security and Cryptology, ICISC'05, pages 156-168, Berlin, Heidelberg, 2005. Springer-Verlag. URL: https://doi.org/10.1007/11734727_14.
  30. Shravan Narayan, Craig Disselkoen, Daniel Moghimi, Sunjay Cauligi, Evan Johnson, Zhao Gang, Anjo Vahldiek-Oberwagner, Ravi Sahita, Hovav Shacham, Dean Tullsen, and Deian Stefan. Swivel: Hardening WebAssembly against spectre. In 30th USENIX Security Symposium (USENIX Security 21), pages 1433-1450. USENIX Association, August 2021. URL: https://www.usenix.org/conference/usenixsecurity21/presentation/narayan.
  31. Van Chan Ngo, Mario Dehesa-Azuara, Matthew Fredrikson, and Jan Hoffmann. Verifying and Synthesizing Constant-Resource Implementations with Types. In 2017 IEEE Symposium on Security and Privacy (SP), pages 710-728, San Jose, CA, May 2017. IEEE. URL: https://doi.org/10.1109/SP.2017.53.
  32. Brandon Paulsen, Chungha Sung, Peter A. H. Peterson, and Chao Wang. Debreach: mitigating compression side channels via static analysis and transformation. In Proceedings of the 34th IEEE/ACM International Conference on Automated Software Engineering, ASE '19, pages 899-911. IEEE Press, 2020. URL: https://doi.org/10.1109/ASE.2019.00088.
  33. Swarn Priya. Formally computer-verified protections against timing-based side-channel attacks. Theses, Université Côte d'Azur, November 2023. URL: https://hal.science/tel-04331805.
  34. Jonathan Protzenko, Jean-Karim Zinzindohoué, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, and Nikhil Swamy. Verified low-level programming embedded in F*. Proceedings of the ACM on Programming Languages, 1(ICFP):1-29, August 2017. URL: https://doi.org/10.1145/3110261.
  35. Qi Qin, JulianAndres JiYang, Fu Song, Taolue Chen, and Xinyu Xing. Dejitleak: eliminating jit-induced timing side-channel leaks. In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2022, pages 872-884, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3540250.3549150.
  36. Ashay Rane, Calvin Lin, and Mohit Tiwari. Raccoon: closing digital side-channels through obfuscated execution. In Proceedings of the 24th USENIX Conference on Security Symposium, SEC'15, pages 431-446, USA, 2015. USENIX Association. URL: https://www.usenix.org/conference/usenixsecurity15/technical-sessions/presentation/rane.
  37. Dorothy Elizabeth Robling Denning. Cryptography and Data Security. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1982. Google Scholar
  38. Rocq theorem prover. https://github.com/rocq-prover/rocq, 2025.
  39. Haifeng Ruan, Yannic Noller, Saeid Tizpaz-Niari, Sudipta Chattopadhyay, and Abhik Roychoudhury. Timing side-channel mitigation via automated program repair. ACM Trans. Softw. Eng. Methodol., 33(8), November 2024. URL: https://doi.org/10.1145/3678169.
  40. Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Gregoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, and Lucas Tabary-Maujean. Typing High-Speed Cryptography against Spectre v1 . In 2023 IEEE Symposium on Security and Privacy (SP), pages 1094-1111, Los Alamitos, CA, USA, May 2023. IEEE Computer Society. URL: https://doi.org/10.1109/SP46215.2023.10179418.
  41. Luigi Soares, Michael Canesche, and Fernando Magno Quintão Pereira. Side-channel elimination via partial control-flow linearization. ACM Trans. Program. Lang. Syst., 45(2), June 2023. URL: https://doi.org/10.1145/3594736.
  42. Meng Wu, Shengjian Guo, Patrick Schaumont, and Chao Wang. Eliminating timing side-channel leaks using program repair. In Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2018, pages 15-26, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3213846.3213851.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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