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的法定任务，并且使用基金会的知识分子优点和更广泛的影响审查标准，认为值得通过评估来获得支持。