Sébastien Bardin

As quantum computing becomes an emerging reality, designing efficient quantum programming capabilities is becoming more and more important. Particularly, the debugging and validation of quantum programs is of paramount importance, as these programs are by definition hard to test. Static analysis and formal verification methods for quantum programs started to emerge a few years now, yet they often miss hybrid quantum/classical reasoning facilities with, e.g., generic quantum control, classical control and classical computation instructions. In this paper, we lay out the foundations of a framework for the automated formal verification of (full) hybrid quantum programs featuring both classical and quantum control, measurement and hybrid data structures. In particular, we propose: (1) a novel symbolic representation for describing and manipulating sets of hybrid quantum/classical states called Hybrid Path-Sums (HPS); (2) a set of rewriting rules providing a rich mechanism for simplifying and reasoning on these symbolic hybrid states, and (3) a core assertion language to specify equivalence of hybrid quantum programs, the satisfaction of properties on (parts of) hybrid states, and the extraction of probabilistic statements about the program behavior. We prove the correctness of the novel symbolic representation, of its rewriting system and of the specification system. Finally, we propose a full implementation of this framework as a dedicated symbolic execution engine for hybrid programs. We present an evaluation of a set of representative hybrid case-studies from the literature, showcasing the advantage of our approach and its efficiency compared to state-of-the-art solutions.

The PQDSS standardization process requires cryptographic primitives to be free from vulnerabilities, including timing and cache side-channels. Resistance to timing leakage is therefore an essential property, and achieving this typically relies on software implementations that follow constant-time principles. Moreover, ensuring that all implementations are constant-time is crucial for fair performance comparisons, as secure implementations often incur additional overhead. Such analysis also helps identify scheme proposals that are inherently difficult to implement in constant time. Because constant-time properties can be broken during compilation, it is often necessary to analyze the compiled binary directly. Since manual binary analysis is extremely challenging, automated analysis becomes highly important. Although several tools exist to assist with such analysis, they often have usability limitations and are difficult to set up correctly. To support the developers besides the NIST committee in verifying candidates, we developed a toolchain that automates configuration, execution, and result analysis for several widely used constant-time analysis tools. We selected TIMECOP and Binsec/Rel2 to verify constant-time policy compliance at the binary level, and dudect and RTLF to detect side-channel vulnerabilities through statistical analysis of execution time behavior. We demonstrate its effectiveness and practicability by evaluating the NIST PQDSS round 1 and round 2 implementations. We reported 26 issues in total to the respective developers, and 5 of them have already been fixed. We also discuss our different findings, as well as the benefits of shortcomings of the different tools.

Program annotations in the form of function pre/postconditions play a crucial role in various software engineering and program verification tasks. However, the frequent unavailability of these annotations necessitates manual retrofitting. This paper shows how constraint acquisition, a learning framework derived from constraint programming and version space learning, can be extended for automatically inferring program preconditions. Our approach performs this inference in a black-box manner through automatic query generation and input-output observations of program executions. We introduce PreCA, the first-ever precondition inference framework leveraging query-based constraint acquisition. Notably, we specialize PreCA to handle memory-related preconditions on binary code, which pose significant challenges in data and information management systems. In contrast to prior black-box techniques, PreCA provides well-defined guarantees. Specifically, it employs a sound and complete method to generate preconditions consistent with all the observed input-output relationships of the program. Furthermore, empirical evaluations on our benchmark demonstrate that PreCA outperforms the results of state-of-the-art approaches, delivering comparable or superior results in 5s, as opposed to the 1-hour runtime of existing approaches on identical machines. We also present two successful use cases from the standard libc and the mbedtls cryptographic library. PreCA notably infers for the former one a more precise precondition than specified in the documentation.

Most software analysis techniques focus on bug reachability. However, this approach is not ideal for security evaluation as it does not take into account the difficulty of triggering said bugs. The recently introduced notion of robust reachability tackles this issue by distinguishing between bugs that can be reached independently from uncontrolled inputs, from those that cannot. Yet, this qualitative notion is too strong in practice as it cannot distinguish mostly replicable bugs from truly unrealistic ones. In this work we propose a more flexible quantitative version of robust reachability together with a dedicated form of symbolic execution, in order to automatically measure the difficulty of triggering bugs. This Quantitative Robust Symbolic Execution (QRSE) relies on a variant of model counting, which allows to account for the asymmetry between attacker-controlled and uncontrolled variables. While this specific model counting problem has been studied in AI research fields such as Bayesian networks, knowledge representation and probabilistic planning, its use within the context of formal verification presents new challenges. We show the applicability of our solutions through security-oriented case studies, including real-world vulnerabilities such as CVE-2019-20839 from libvncserver.

This is the RCR report of the artifact for the article “Fine-grained Coverage-based Fuzzing.” This report contains scripts and pre-build binary programs to reproduce the results presented in the main article. The artifact is released on Zenodo with DOI: 10.5281/zenodo.7275184. We claim the artifact to be available, functional, and reusable. The technology skills needed to review the artifact are knowing how to use Linux/Unix terminal and a basic understanding of Docker.