Towards Efficient Verification of Constant-Time Cryptographic Implementations

• URL: http://arxiv.org/abs/2402.13506v1
• Date: Wed, 21 Feb 2024 03:39:14 GMT
• Title: Towards Efficient Verification of Constant-Time Cryptographic Implementations
• Authors: Luwei Cai and Fu Song and Taolue Chen
• Abstract summary: Constant-time programming discipline is an effective software-based countermeasure against timing side-channel attacks. We put forward practical verification approaches based on a novel synergy of taint analysis and safety verification of self-composed programs. Our approach is implemented as a cross-platform and fully automated tool CT-Prover.
• Score: 5.433710892250037
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Timing side-channel attacks exploit secret-dependent execution time to fully or partially recover secrets of cryptographic implementations, posing a severe threat to software security. Constant-time programming discipline is an effective software-based countermeasure against timing side-channel attacks, but developing constant-time implementations turns out to be challenging and error-prone. Current verification approaches/tools suffer from scalability and precision issues when applied to production software in practice. In this paper, we put forward practical verification approaches based on a novel synergy of taint analysis and safety verification of self-composed programs. Specifically, we first use an IFDS-based lightweight taint analysis to prove that a large number of potential (timing) side-channel sources do not actually leak secrets. We then resort to a precise taint analysis and a safety verification approach to determine whether the remaining potential side-channel sources can actually leak secrets. These include novel constructions of taint-directed semi-cross-product of the original program and its Boolean abstraction, and a taint-directed self-composition of the program. Our approach is implemented as a cross-platform and fully automated tool CT-Prover. The experiments confirm its efficiency and effectiveness in verifying real-world benchmarks from modern cryptographic and SSL/TLS libraries. In particular, CT-Prover identify new, confirmed vulnerabilities of open-source SSL libraries (e.g., Mbed SSL, BearSSL) and significantly outperforms the state-of-the-art tools.

Related papers

• Secret Breach Prevention in Software Issue Reports [2.8747015994080285]
  This paper presents a novel technique for secret breach detection in software issue reports. We highlight the challenges posed by noise, such as log files, URLs, commit IDs, stack traces, and dummy passwords. We propose an approach combining the strengths of state-of-the-artes with the contextual understanding of language models.
  arXiv  Detail & Related papers  (2024-10-31T06:14:17Z)
• Divide and Conquer based Symbolic Vulnerability Detection [0.16385815610837165]
  This paper presents a vulnerability detection approach based on symbolic execution and control flow graph analysis. Our approach employs a divide-and-conquer algorithm to eliminate irrelevant program information.
  arXiv  Detail & Related papers  (2024-09-20T13:09:07Z)
• The Impact of SBOM Generators on Vulnerability Assessment in Python: A Comparison and a Novel Approach [56.4040698609393]
  Software Bill of Materials (SBOM) has been promoted as a tool to increase transparency and verifiability in software composition. Current SBOM generation tools often suffer from inaccuracies in identifying components and dependencies. We propose PIP-sbom, a novel pip-inspired solution that addresses their shortcomings.
  arXiv  Detail & Related papers  (2024-09-10T10:12:37Z)
• An Extensive Comparison of Static Application Security Testing Tools [1.3927943269211593]
  Static Application Security Testing Tools (SASTTs) identify software vulnerabilities to support the security and reliability of software applications. Several studies have suggested that alternative solutions may be more effective than SASTTs due to their tendency to generate false alarms. Our SASTTs evaluation is based on a controlled, though synthetic, Java.
  arXiv  Detail & Related papers  (2024-03-14T09:37:54Z)
• QTFlow: Quantitative Timing-Sensitive Information Flow for Security-Aware Hardware Design on RTL [0.3679557794795275]
  We introduce QTFlow, a timing-sensitive framework for quantifying hardware information leakages during the design phase. QTFlow autonomously identifies timing channels and diminishes all false positives arising from time-agnostic analysis.
  arXiv  Detail & Related papers  (2024-01-31T13:22:57Z)
• SOCI^+: An Enhanced Toolkit for Secure OutsourcedComputation on Integers [50.608828039206365]
  We propose SOCI+ which significantly improves the performance of SOCI. SOCI+ employs a novel (2, 2)-threshold Paillier cryptosystem with fast encryption and decryption as its cryptographic primitive. Compared with SOCI, our experimental evaluation shows that SOCI+ is up to 5.4 times more efficient in computation and 40% less in communication overhead.
  arXiv  Detail & Related papers  (2023-09-27T05:19:32Z)
• Empirical Analysis of Software Vulnerabilities Causing Timing Side Channels [2.0794749869068005]
  This study examines the timing attack-related vulnerabilities in non-cryptographic software. We found that a majority of the timing attack-related vulnerabilities were introduced due to not following known secure coding practices. The findings of this study are expected to help the software security community gain evidence-based information about the nature and causes of the vulnerabilities related to timing attacks.
  arXiv  Detail & Related papers  (2023-08-23T01:38:03Z)
• Using Machine Learning To Identify Software Weaknesses From Software Requirement Specifications [49.1574468325115]
  This research focuses on finding an efficient machine learning algorithm to identify software weaknesses from requirement specifications. Keywords extracted using latent semantic analysis help map the CWE categories to PROMISE_exp. Naive Bayes, support vector machine (SVM), decision trees, neural network, and convolutional neural network (CNN) algorithms were tested.
  arXiv  Detail & Related papers  (2023-08-10T13:19:10Z)
• Quantization-aware Interval Bound Propagation for Training Certifiably Robust Quantized Neural Networks [58.195261590442406]
  We study the problem of training and certifying adversarially robust quantized neural networks (QNNs) Recent work has shown that floating-point neural networks that have been verified to be robust can become vulnerable to adversarial attacks after quantization. We present quantization-aware interval bound propagation (QA-IBP), a novel method for training robust QNNs.
  arXiv  Detail & Related papers  (2022-11-29T13:32:38Z)
• Log Barriers for Safe Black-box Optimization with Application to Safe Reinforcement Learning [72.97229770329214]
  We introduce a general approach for seeking high dimensional non-linear optimization problems in which maintaining safety during learning is crucial. Our approach called LBSGD is based on applying a logarithmic barrier approximation with a carefully chosen step size. We demonstrate the effectiveness of our approach on minimizing violation in policy tasks in safe reinforcement learning.
  arXiv  Detail & Related papers  (2022-07-21T11:14:47Z)
• VELVET: a noVel Ensemble Learning approach to automatically locate VulnErable sTatements [62.93814803258067]
  This paper presents VELVET, a novel ensemble learning approach to locate vulnerable statements in source code. Our model combines graph-based and sequence-based neural networks to successfully capture the local and global context of a program graph. VELVET achieves 99.6% and 43.6% top-1 accuracy over synthetic data and real-world data, respectively.
  arXiv  Detail & Related papers  (2021-12-20T22:45:27Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.