FET: SHF: Small: A Verification Framework for Hybrid Classical and Quantum Protocols (VeriHCQ)

量子计算和通信依赖于量子物理中的基本现象来提供高效的计算问题解决和安全通信。特别是，量子系统中的状态可以处于叠加状态，即同时处于许多传统状态，所有这些状态都可以使用量子操作同时处理。此外，量子信息不能被复制，这意味着量子通信系统中的信息传递比传统的数据通信系统要安全得多。这些大规模并行和安全通信的可能性一直是人们对量子计算兴趣持续激增的主要驱动因素。然而，实用的量子计算和通信平台的发展进展非常缓慢。在某种程度上，这是由于对量子硬件进步的需求。另一个问题是缺乏量子和量子-经典混合计算系统的编程模型。目前这些系统的编程范例需要有量子物理学的重要背景，而且非常低级——类似于传统计算中的机器代码。这两个因素都阻碍了计算机和通信工程师大规模开发量子平台的能力。该项目的重点是为建模和验证量子通信系统开发原则性的高级形式化。目标是允许对混合经典和量子（HCQ）网络和安全协议的量子硬件进行定义、自动验证和编译。总体方法依赖于将基本的量子操作（如量子隐形传态和超密编码）视为黑盒子，这些黑盒子以过程代数的方式被赋予抽象的非量子操作语义。这种语义解释旨在为以下方面提供基础：正式而抽象的HCQ协议规范；自动验证HCQ协议属性的模型检查框架；一个经过认证的过程代数编译器是一种中间语言，可以翻译成不同的量子体系结构。该框架利用现有的形式化方法和网络编程框架，包括时间逻辑模型检查器和软件定义的网络平台。正在进行涉及一系列HCQ网络和安全协议的案例研究，以说明这项工作的力量和效用。该项目还吸引了代表性不足的群体的成员，以扩大对量子计算研究的参与。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Quantum computing and communication rely on basic phenomena in quantum physics to provide highly efficient computational problem solving and secure communication. In particular, states in a quantum system can be in superposition, meaning in many traditional states at the same time, all of which can be processed simultaneously using quantum operations. Also, quantum messages cannot be copied, meaning that message delivery in quantum communication systems can be much more secure than in traditional data-communications systems. These possibilities for massive parallelism and secure communication have been major drivers for the ongoing surge of interest in quantum computing. However, the development of practical quantum-computing and -communication platforms has progressed very slowly. In part, this is due to the need for advances in quantum hardware. Another concern is the lack of programming models for quantum, and hybrid quantum-classical, computing systems. Current programming paradigms for these systems require significant background in quantum physics and are also very low-level - a level analogous to machine code in traditional computing. Both of these factors impede the ability of computer and communications engineers to develop quantum platforms at scale.This project is focused on developing principled, high-level formalisms for modeling and verifying quantum communication systems. The goal is to permit the definition, automatic verification, and compilation to quantum hardware of hybrid classical and quantum (HCQ) network and security protocols. The over-all approach relies on treating basic quantum operations, such as quantum teleportation and superdense coding, as black boxes that are given an abstract, non-quantum operational semantics in the style of process algebra. This semantic account is intended to provide a basis for: formal yet abstract specification of HCQ protocols; a model-checkingframework to automatically verify properties of HCQ protocols; and a certified compiler from the process algebrato an intermediate language that can be translated to different quantum architectures. The framework leverages existing formal-methods and network-programming frameworks, including temporal-logic model checkers and software-defined network platforms. Case studies involving a range of HCQ network and security protocols are being undertaken to illustrate the power and utility of the work. The project effort is also engaging members of under-represented groups in order to broaden participation in quantum-computing research.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.