DROPS

Document

DOI: 10.4230/LIPIcs.ECOOP.2024.46

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

Authors: Quan Zhou, Sixuan Dang, and Danfeng Zhang

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

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.

Cite as

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)

Copy BibTex To Clipboard

@InProceedings{zhou_et_al:LIPIcs.ECOOP.2024.46,
  author =	{Zhou, Quan and Dang, Sixuan and Zhang, Danfeng},
  title =	{{\{CtChecker\}: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{46:1--46:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.46},
  URN =		{urn:nbn:de:0030-drops-208951},
  doi =		{10.4230/LIPIcs.ECOOP.2024.46},
  annote =	{Keywords: Information flow control, static analysis, side channel, constant-time programming}
}

Document

Artifact

DOI: 10.4230/DARTS.10.2.26

CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming (Artifact)

Authors: Quan Zhou, Sixuan Dang, and Danfeng Zhang

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract

This artifact includes the implementation of the CtChecker analysis toolchain described in the corresponding paper. We provide two options to run CtChecker, building it from source or running the pre-built tool with Docker. All evaluated benchmark source code are provided in the artifact. A walkthrough of how to reproduce the evaluation results in the paper is provided in the Appendix.

Cite as

Quan Zhou, Sixuan Dang, and Danfeng Zhang. CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 26:1-26:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{zhou_et_al:DARTS.10.2.26,
  author =	{Zhou, Quan and Dang, Sixuan and Zhang, Danfeng},
  title =	{{CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming (Artifact)}},
  pages =	{26:1--26:5},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{Zhou, Quan and Dang, Sixuan and Zhang, Danfeng},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.26},
  URN =		{urn:nbn:de:0030-drops-209244},
  doi =		{10.4230/DARTS.10.2.26},
  annote =	{Keywords: Information flow control, static analysis, side channel, constant-time programming}
}

Search Results

Documents authored by Dang, Sixuan

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

Abstract

Cite as

CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming (Artifact)

Abstract

Cite as

Thanks for your feedback!

Could not send message