Formal verification for physical layer security in ISAC scenarios
Supervisor: Dr Michele Sevegnani
School: Computing Science
Description:
Integrated Sensing and Communication (ISAC) is expected to be a core capability of next-generation wireless systems, but it introduces security risks because sensing targets and other third parties can also act as eavesdroppers or jammers. Current Physical Layer Security (PLS) work for ISAC focuses on techniques such as secure beamforming and artificial noise, typically assessed via simulation or analytical bounds rather than machine-checkable guarantees. This internship applies Formal Verification to provide quantitative assurance for secure beamforming under uncertainty. The student will model a simplified multi-antenna ISAC link and verify properties such as bounds on secrecy-outage probability subject to a minimum sensing-performance proxy.