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

FET：SHF：小型：混合经典和量子协议的验证框架 (VeriHCQ)

• 批准号: 2330974
• 负责人: Walter Cleaveland
• 金额: $ 60万
• 依托单位: University of Maryland, College Park
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-02-01 至 2027-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2330974&HistoricalAwards=false
• 关键词: FET; SHF; Small; Verification; Framework

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.

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