Researchers Showcase Advances in Formal Verification for Security Protocols and O-RAN at SEFM24, DataMod24, and IRC-CSS
22 Nov, 2024
Dr. Roberto Metere and Dr. Kangfeng Ye, researchers from the University of York, recently participated in three prominent events: the 22nd International Conference on Software Engineering and Formal Methods (SEFM24), the 12th International Symposium From Data to Models and Back (DataMod24), and a talk hosted by the IRC for Communication Systems and Sensing (IRC-CSS) in Saudi Arabia. Their research highlights the transformative use of formal verification in security protocols and O-RAN (Open Radio Access Networks) for 6G technologies.
Innovations in Security Protocols
At SEFM24, Dr. Ye presented the paper titled “User-Guided Verification of Security Protocols via Sound Animation”, a collaborative work with Dr. Metere and Dr. Poonam Yadav. This research addresses the challenges of making formal verification more accessible to security protocol designers. By introducing sound animation, the team developed an iterative workflow that enables designers to identify bugs early in the design process, with the assurance that detected issues represent real flaws. The innovation lies in the automatic generation of animators from security protocol models, streamlining the process and allowing designers to deliver secure protocols efficiently without compromising on accuracy.
Balancing Energy Efficiency and Service Availability in 6G O-RAN
At DataMod24, Dr. Metere presented the paper titled “Towards Achieving Energy Efficiency and Service Availability in 6G O-RAN via Formal Verification”. This research, conducted in collaboration with experts from the University of York, the University of Glasgow, and Imperial College London, tackles the challenge of logical inconsistencies that arise during the adoption of O-RAN and deployment of AI/ML-driven xApps.
Using probabilistic model checkers (PRISM and Storm), the study demonstrates how to compute optimal thresholds between energy efficiency and service availability for a defined policy in dynamic scenarios. The findings help prevent misconfigurations and enhance the reliability of AI-driven applications in network management, ensuring that decisions are logically consistent and robust.
Formal Verification to Inform a Verifiable 6G
In early October, Dr. Michele Sevegnani from the University of Glasgow delivered a talk at IRC-CSS in Saudi Arabia titled “Formal Verification of 5G Advanced Protocols to Inform a Verifiable 6G”. His presentation showcased the ongoing application of formal verification to two key O-RAN scenarios:
1. Safeguarding resource allocation optimisation xApps generated by Large Language Models (LLMs).
2. Computing optimal thresholds between energy efficiency and service availability using the PRISM model checker.
This work emphasises the importance of leveraging formal verification to ensure network decisions remain reliable as 6G technologies evolve.
Advancing the Frontiers of Secure and Efficient 6G Networks
These contributions underscore the importance of formal verification in ensuring secure, efficient, and logically consistent networks as we transition into the 6G era. By addressing key challenges in security protocols and O-RAN, this research paves the way for advancements that will shape the future of telecommunications.
