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

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

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.