Document Open Access Logo

{CtChecker}: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming

Authors Quan Zhou , Sixuan Dang , Danfeng Zhang

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2024.46.pdf
  • Filesize: 0.94 MB
  • 26 pages

Document Identifiers

Author Details

Quan Zhou
  • Penn State University, University Park, PA, USA
Sixuan Dang
  • Duke University, Durham, NC, USA
Danfeng Zhang
  • Duke University, Durham, NC, USA

Funding

This work was supported by the NSF under grants 2401182, 2401496, 1942851 and 1956032.

Acknowledgements

We express our sincere gratitude to the anonymous reviewers for their insightful feedback and suggestions. We would like to thank Shuai Wang for sharing detailed CacheS evaluation results, and Ernest DeFoy III and Xiang Li for their contributions in the early stage of the project.

Cite As Get BibTex

Quan Zhou, Sixuan Dang, and Danfeng Zhang. {CtChecker}: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 46:1-46:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ECOOP.2024.46

Abstract

Timing channel attacks are emerging as real-world threats to computer security. In cryptographic systems, an effective countermeasure against timing attacks is the constant-time programming discipline. However, strictly enforcing the discipline manually is both time-consuming and error-prone. While various tools exist for analyzing/verifying constant-time programs, they sacrifice at least one feature among precision, soundness and efficiency.
In this paper, we build CtChecker, a sound static analysis for constant-time programming. Under the hood, CtChecker uses a static information flow analysis to identify violations of constant-time discipline. Despite the common wisdom that sound, static information flow analysis lacks precision for real-world applications, we show that by enabling field-sensitivity, context-sensitivity and partial flow-sensitivity, CtChecker reports fewer false positives compared with existing sound tools. Evaluation on real-world cryptographic systems shows that CtChecker analyzes 24K lines of source code in under one minute. Moreover, CtChecker reveals that some repaired code generated by program rewriters supposedly remove timing channels are still not constant-time.

Subject Classification

ACM Subject Classification
  • Security and privacy → Information flow control
Keywords
  • Information flow control
  • static analysis
  • side channel
  • constant-time programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. Verifying constant-time implementations. In USENIX Security Symposium, pages 53-70, 2016. Google Scholar
  2. Lars Ole Andersen. Program analysis and specialization for the c programming language. Ph.D. Thesis, 1994. Google Scholar
  3. Gilles Barthe, Gustavo Betarte, Juan Campo, Carlos Luna, and David Pichardie. System-level non-interference for constant-time cryptography. In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, CCS '14, pages 1267-1279, New York, NY, USA, 2014. ACM. URL: https://doi.org/10.1145/2660267.2660283.
  4. Gilles Barthe, Juan Manuel Crespo, and César Kunz. Relational verification using product programs. In International Symposium on Formal Methods, pages 200-214. Springer, 2011. Google Scholar
  5. Gilles Barthe, Pedro R D'argenio, and Tamara Rezk. Secure information flow by self-composition. Mathematical Structures in Computer Science, 21(6):1207-1252, 2011. Google Scholar
  6. Daniel J Bernstein, Joachim Breitner, Daniel Genkin, Leon Groot Bruinderink, Nadia Heninger, Tanja Lange, Christine van Vredendaal, and Yuval Yarom. Sliding right into disaster: Left-to-right sliding windows leak. In International Conference on Cryptographic Hardware and Embedded Systems, pages 555-576. Springer, 2017. Google Scholar
  7. 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, pages 715-733, 2021. Google Scholar
  8. 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. IEEE, 2019. Google Scholar
  9. Robert Brotzman, Danfeng Zhang, Mahmut Taylan Kandemir, and Gang Tan. Specsafe: detecting cache side channels in a speculative world. Proceedings of the ACM on Programming Languages, 5(OOPSLA):1-28, 2021. Google Scholar
  10. David Brumley and Dan Boneh. Remote timing attacks are practical. Computer Networks, 48(5):701-716, 2005. Google Scholar
  11. 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, pages 174-189, 2019. Google Scholar
  12. GnuPG community. Libgcrypt. https://gnupg.org/software/libgcrypt/index.html, 2022.
  13. Dorothy E. Denning. A lattice model of secure information flow. Communication of the ACM, 19(5):236-243, 1976. Google Scholar
  14. William Enck, Peter Gilbert, Seungyeop Han, Vasant Tendulkar, Byung-Gon Chun, Landon P Cox, Jaeyeon Jung, Patrick McDaniel, and Anmol N Sheth. Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones. ACM Transactions on Computer Systems (TOCS), 32(2):1-29, 2014. Google Scholar
  15. OpenSSL Software Foundation. Openssl: Cryptography and ssl/tls toolkit. https://www.openssl.org/, 2022.
  16. Joseph A Goguen and José Meseguer. Security policies and security models. In IEEE Symposium on Security and Privacy, pages 11-20. IEEE, 1982. Google Scholar
  17. David Gullasch, Endre Bangerter, and Stephan Krenn. Cache games-bringing access-based cache attacks on aes to practice. In 2011 IEEE Symposium on Security and Privacy, pages 490-505. IEEE, 2011. Google Scholar
  18. Andrew Johnson, Lucas Waye, Scott Moore, and Stephen Chong. Exploring and enforcing security guarantees via program dependence graphs. ACM SIGPLAN Notices, 50(6):291-302, 2015. Google Scholar
  19. JuliaHubOSS. Llvm c backend. https://github.com/JuliaHubOSS/llvm-cbe, 2018.
  20. Dave King, Boniface Hicks, Michael Hicks, and Trent Jaeger. Implicit flows: Can’t live with ‘em, can’t live without ‘em. In Information Systems Security: 4th International Conference, ICISS 2008, Hyderabad, India, December 16-20, 2008. Proceedings 4, pages 56-70. Springer, 2008. Google Scholar
  21. Paul C Kocher. Timing attacks on implementations of diffie-hellman, rsa, dss, and other systems. In Annual International Cryptology Conference, pages 104-113. Springer, 1996. Google Scholar
  22. Chris Lattner, Andrew Lenharth, and Vikram Adve. Making context-sensitive points-to analysis with heap cloning practical for the real world. ACM SIGPLAN Notices, 42(6):278-289, 2007. Google Scholar
  23. Andrew C Myers. Jflow: Practical mostly-static information flow control. In Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 228-241, 1999. Google Scholar
  24. James Newsome and Dawn Xiaodong Song. Dynamic taint analysis for automatic detection, analysis, and signaturegeneration of exploits on commodity software. In NDSS, volume 5, pages 3-4, 2005. Google Scholar
  25. Zvonimir Pavlinovic, Tim King, and Thomas Wies. Finding minimum type error sources. ACM SIGPLAN Notices, 49(10):525-542, 2014. Google Scholar
  26. Colin Percival. Cache missing for fun and profit, 2005. Google Scholar
  27. Cesar Pereida García, Billy Bob Brumley, and Yuval Yarom. Make sure dsa signing exponentiations really are constant-time. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pages 1639-1650, 2016. Google Scholar
  28. Thomas Pornin. Constant-time in bearssl. https://bearssl.org/constanttime.html, 2018.
  29. Thomas Pornin. Bearssl is an implementation of the ssl/tls protocol (rfc 5246) written in c. https://bearssl.org, 2022.
  30. François Pottier and Vincent Simonet. Information flow inference for ml. In Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 319-330, 2002. Google Scholar
  31. Jakob Rehof et al. Tractable constraints in finite semilattices. Science of Computer Programming, 35(2-3):191-221, 1999. Google Scholar
  32. Bruno Rodrigues, Fernando Magno Quintão Pereira, and Diego F. Aranha. Sparse representation of implicit flows with applications to side-channel detection. In Proceedings of the 25th International Conference on Compiler Construction, CC 2016, pages 110-120, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2892208.2892230.
  33. Andrei Sabelfeld and Andrew C Myers. Language-based information-flow security. IEEE Journal on selected areas in communications, 21(1):5-19, 2003. Google Scholar
  34. Georgios Sakkas, Madeline Endres, Benjamin Cosman, Westley Weimer, and Ranjit Jhala. Type error feedback via analytic program repair. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 16-30, 2020. Google Scholar
  35. Luigi Soares and Fernando Magno Quintãn Pereira. Memory-safe elimination of side channels. In 2021 IEEE/ACM International Symposium on Code Generation and Optimization (CGO), pages 200-210. IEEE, 2021. Google Scholar
  36. Juraj Somorovsky. Curious padding oracle in openssl (cve-2016-2107), 2016. Last Retrieved: Jan 2024. URL: https://web-in-security.blogspot.co.uk/2016/05/curious-padding-oracle-in-openssl-cve.html.
  37. Juraj Somorovsky. Systematic fuzzing and testing of tls libraries. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, CCS '16, pages 1492-1504, New York, NY, USA, 2016. ACM. URL: https://doi.org/10.1145/2976749.2978411.
  38. Bjarne Steensgaard. Points-to analysis in almost linear time. In Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 32-41, 1996. Google Scholar
  39. G Edward Suh, Jae W Lee, David Zhang, and Srinivas Devadas. Secure program execution via dynamic information flow tracking. ACM Sigplan Notices, 39(11):85-96, 2004. Google Scholar
  40. Yulei Sui and Jingling Xue. Svf: interprocedural static value-flow analysis in llvm. In Proceedings of the 25th international conference on compiler construction, pages 265-266. ACM, 2016. Google Scholar
  41. TrustedFirmware. Mbed tls. https://www.trustedfirmware.org/projects/mbed-tls, 2022.
  42. Dennis Volpano and Geoffrey Smith. A type-based approach to program security. In TAPSOFT'97: Theory and Practice of Software Development: 7th International Joint Conference CAAP/FASE Lille, France, April 14-18, 1997 Proceedings 22, pages 607-621. Springer, 1997. Google Scholar
  43. Guanhua Wang, Sudipta Chattopadhyay, Ivan Gotovchits, Tulika Mitra, and Abhik Roychoudhury. oo7: Low-overhead defense against spectre attacks via program analysis. IEEE Transactions on Software Engineering, 47(11):2504-2519, 2019. Google Scholar
  44. Shuai Wang, Yuyan Bao, Xiao Liu, Pei Wang, Danfeng Zhang, and Dinghao Wu. Identifying Cache-Based side channels through Secret-Augmented abstract interpretation. In 28th USENIX security symposium (USENIX security 19), pages 657-674, 2019. Google Scholar
  45. Shuai Wang, Pei Wang, Xiao Liu, Danfeng Zhang, and Dinghao Wu. Cached: Identifying cache-based timing channels in production software. In Proceedings of the 26th USENIX Security Symposium, pages 235-252, 2017. Google Scholar
  46. 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, pages 15-26, 2018. Google Scholar
  47. Yuval Yarom, Daniel Genkin, and Nadia Heninger. Cachebleed: a timing attack on openssl constant-time rsa. Journal of Cryptographic Engineering, 7:99-112, 2017. Google Scholar
  48. Anna Zaks and Amir Pnueli. Covac: Compiler validation by program analysis of the cross-product. In International Symposium on Formal Methods, pages 35-51. Springer, 2008. Google Scholar
  49. Danfeng Zhang, Aslan Askarov, and Andrew C Myers. Language-based control and mitigation of timing channels. In Proceedings of the 33rd ACM SIGPLAN conference on Programming Language Design and Implementation, pages 99-110, 2012. Google Scholar
  50. Danfeng Zhang and Andrew C Myers. Toward general diagnosis of static errors. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 569-581, 2014. Google Scholar
  51. Danfeng Zhang, Yao Wang, G Edward Suh, and Andrew C Myers. A hardware design language for timing-sensitive information-flow security. ACM SIGPLAN Notices, 50(4):503-516, 2015. Google Scholar
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact