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

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-checking framework to automatically verify properties of HCQ protocols; and a certified compiler from the process algebra to 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.