School of Computing Science

Events

Students sitting in a lecture theatre

Explore upcoming seminars, guest lectures, workshops, and other events hosted by the School of Computing Science.

Our events bring together students, researchers, industry partners, and the wider community to share ideas, showcase research, and foster collaboration.

This Week’s EventsAll Upcoming EventsPast EventsWebapp

This Week’s Events

(Hybrid) Explainable Graph-Based Early Detection of Time Synchronisation Attacks on the O-RAN Open Fronthaul

Group: Networked Systems Research Laboratory (NETLAB)
Speaker: Muhammad Arif
Date: 08 October, 2026
Time: 10:00 - 11:00
Location: SAWB 423, Sir Alwyn Williams Building

Open Radio Access Network (O-RAN) disaggregates radio and baseband functions over standardised open interfaces, making the Open Fronthaul (O-FH) and its Synchronisation Plane (S-Plane) critical to coordinated operation, which depends on accurate time and phase alignment across distributed components. IEEE~1588 Precision Time Protocol (PTP) provides high-accuracy timing, but commonly deployed configurations offer limited protection against compromised timing sources and manipulated synchronisation messages. Previous work has shown that PTP spoofing can lead to gNB failure within approximately two seconds, highlighting the need for early detection. This study presents an early and explainable graph-based framework for detecting PTP synchronisation attacks in O-RAN. A Hybrid O-RAN testbed is implemented with User Equipment (UEs) generating service traffic, a logical Radio Unit (RU), an srsRAN Distributed Unit/Central Unit (DU/CU), and a simulated Ethernet-based Lower-Layer Split Category~3 (LLS-C3) S-Plane topology over the O-FH between the RU and DU. The evaluated attack compromises a legitimate backup Grandmaster, reconfigures it to win the Best Master Clock Algorithm (BMCA) election, and then manipulates PTP timestamps to introduce progressive time synchronisation disruption. From 100 experimental runs, comprising 30 benign and 70 attack runs, topology-aware graphs are constructed from PTP and O-FH/eCPRI measurements. A three-layer Graph Attention Network (GAT)-augmented GraphSAGE classifier attains 99.21\% accuracy and 99.54\% F1-score. In live DU-side evaluation, the framework achieves a mean live detection latency of 484~ms, below the approximately two-second failure timescale reported in previous work. Integrated Gradients (IG) shows that Time Error and O-FH traffic measurements provide the main feature-level evidence, while the Boundary Clocks directly connected to the RU and DU contribute most strongly at node level. Compared with existing S-Plane approaches based on transport or cryptographic protection, auxiliary positioning measurements, and PTP packet-sequence learning, the proposed framework explicitly models distributed synchronisation relationships while combining run-level generalisation, live sub-second detection, and feature- and node-level explanation.

Upcoming events

(Hybrid) Explainable Graph-Based Early Detection of Time Synchronisation Attacks on the O-RAN Open Fronthaul

Group: Networked Systems Research Laboratory (NETLAB)
Speaker: Muhammad Arif
Date: 08 October, 2026
Time: 10:00 - 11:00
Location: SAWB 423, Sir Alwyn Williams Building

Open Radio Access Network (O-RAN) disaggregates radio and baseband functions over standardised open interfaces, making the Open Fronthaul (O-FH) and its Synchronisation Plane (S-Plane) critical to coordinated operation, which depends on accurate time and phase alignment across distributed components. IEEE~1588 Precision Time Protocol (PTP) provides high-accuracy timing, but commonly deployed configurations offer limited protection against compromised timing sources and manipulated synchronisation messages. Previous work has shown that PTP spoofing can lead to gNB failure within approximately two seconds, highlighting the need for early detection. This study presents an early and explainable graph-based framework for detecting PTP synchronisation attacks in O-RAN. A Hybrid O-RAN testbed is implemented with User Equipment (UEs) generating service traffic, a logical Radio Unit (RU), an srsRAN Distributed Unit/Central Unit (DU/CU), and a simulated Ethernet-based Lower-Layer Split Category~3 (LLS-C3) S-Plane topology over the O-FH between the RU and DU. The evaluated attack compromises a legitimate backup Grandmaster, reconfigures it to win the Best Master Clock Algorithm (BMCA) election, and then manipulates PTP timestamps to introduce progressive time synchronisation disruption. From 100 experimental runs, comprising 30 benign and 70 attack runs, topology-aware graphs are constructed from PTP and O-FH/eCPRI measurements. A three-layer Graph Attention Network (GAT)-augmented GraphSAGE classifier attains 99.21\% accuracy and 99.54\% F1-score. In live DU-side evaluation, the framework achieves a mean live detection latency of 484~ms, below the approximately two-second failure timescale reported in previous work. Integrated Gradients (IG) shows that Time Error and O-FH traffic measurements provide the main feature-level evidence, while the Boundary Clocks directly connected to the RU and DU contribute most strongly at node level. Compared with existing S-Plane approaches based on transport or cryptographic protection, auxiliary positioning measurements, and PTP packet-sequence learning, the proposed framework explicitly models distributed synchronisation relationships while combining run-level generalisation, live sub-second detection, and feature- and node-level explanation.

Single-Agent Stability in Hedonic Games with Constrained Coalition Sizes.

Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Adam Dunajski, University of Edinburgh
Date: 13 October, 2026
Time: 15:00 - 16:00
Location: 422 Sir Alwyn Williams (SAWB), University of Glasgow

Hedonic games are coalition formation games where agents form disjoint coalitions (groups) and each agent's utility depends only on the other agents within their group.

We study stability in additively separable hedonic games where coalition sizes have to respect a fixed lower and upper bound. We consider four classic notions of stability based on single-agent deviations, namely, Nash stability, individual stability, contractual Nash stability, and contractual individual stability.

For each stability notion, we consider two variants: in one, the coalition left behind by a deviator must still be of size at least the lower bound, and in the other there is no such constraint.

This talk will introduce the above model, and
provide a full picture of the existence of stable outcomes with respect to given parameters for the lower and upper bounds. Additionally, when there are only upper bounds on coalition sizes, we fully characterize the computational complexity of the associated existence problem, and for particular bounds we obtain polynomial-time algorithms for constructing stable outcomes.

This is joint work with Martin Bullinger, Edith Elkind, and Matan Gilboa, and appeared in the proceedings of SAGT.

Full paper available here: https://arxiv.org/abs/2510.12641

Containers for Dummies

Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Jake Trevor, University of Glasgow
Date: 20 October, 2026
Time: 15:00 - 16:00
Location: 422 Sir Alwyn Williams (SAWB), University of Glasgow

Recursively defined structures are ubiquitous in computer science. When formalising such structures in a system like Lean or Agda, they are required to satisfy a condition called strict positivity. Work in such a system long enough, and you will surely run into positivity problems when trying to formalise things in the natural way. Containers are a tool developed (among other reasons) to tackle positivity problems. They are flexible enough to model a variety of structures in a way which is strictly positive by construction - and therefore, amenable to use in a theorem prover like lean or agda.

Despite their usefulness, containers remain something of a mystery to many people. Part of this, I believe, is due to the presentation in the existing work, which tends to be about the category theory underpinning them. In my experience however, they are much like monads; it is not necessary to understand the theoretical underpinning to use containers or find them useful. A simpler presentation is possible.

In this talk, I will give this simpler presentation. I will explain what containers are, why they are useful, and how to use them, without reference to the categorical
underpinnings. This will be heavily motivated by examples, which have been adapted from my own research work.

TBD

Group: Networked Systems Research Laboratory (NETLAB)
Speaker: TBD
Date: 22 October, 2026
Time: 10:00 - 11:00
Location: SAWB 423, Sir Alwyn Williams Building

TBD

zkFOL: succinct cryptographic certificates for first-order logic

Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Murdoch Jamie Gabbay, Heriot-Watt University
Date: 27 October, 2026
Time: 15:00 - 16:00
Location: 422 Sir Alwyn Williams (SAWB), University of Glasgow


There is a technique in cryptography called *succinct proof*, whereby a *prover* can prove to a *verifier* that it knows some piece of information --- which may be prohibitively large, or just secret --- just by transmitting a much shorter short (`succinct') cryptographic signature.  This made the news recently when Google used cryptography to show that they knew a solution to a problem without directly revealing the solution:
 
I got interested in succinct cryptographic proofs about three years ago, and when I looked at how these proofs are constructed, I saw logic in disguise.  I developed this in a paper and associated exposition
1. Arithmetisation of computation via polynomial semantics for first-order logic,https://eprint.iacr.org/2024/954
2. Cryptographic certificates of validity for trustworthy AI,https://arxiv.org/abs/2606.23768
 
The upshot of the research is that arbitrary logical validity --- that is, actual truth of logical assertions encoded via the zkFOL translation as polynomial arithmetic --- is susceptible to succinct cryptographic proof.  I call this "zkFOL", for "zero-knowledge first-order logic", and it is a powerful generalisation of the cryptographer's notion of succinct proof to arbitrary logic.  This is extremely powerful.  
 
It also seems to me that it could be extraordinarily useful in practice.  For instance: zkFOL proofs could be used to cryptographically assure correctness of behaviour in agentic systems (a kind of "succinct-proof-carrying behaviour" safety guarantee that would be an extensional complement to proof-carrying or formally-verified code).  
Or, zkFOL succinct proofs could  be used to express compliance logic of (say) financial transactions, and these succinct proofs stored for insurance, auditing, or regulatory compliance purposes.  
IMO zkFOL-based assurances of correctness could go a long way towards making distributed systems safer and more reliable.
 
In collaboration with a cryptographer and a compiler designer, we have produced a prototype logic-based language and associated compiler.  The code is beautiful, being just first-order logic --- and it's also very fast.  In laboratory tests, zkFOL outperforms the current state of the art cryptographic proof systems by orders of magnitude.  The compiler is freely available at 
and a draft paper outlining the implementation is in the repo at

How User-AI Mistreatment Occurs and Matters in Conversational Systems?

Group: Systems Seminars
Speaker: Fanqi Zeng, University of Oxford
Date: 03 November, 2026
Time: 14:00 - 15:00
Location: Room 422, Sir Alwyn Williams Building and Teams

Abstract:
Safety research often focuses on model- generated harms, but users may also direct hostility, coercion, and adversarial pressure at models. Understanding how and when that occurs is essential for accurately interpreting model behaviour, alignment drift, and real-world deployment risks. In this paper, we audit 777K English LMSYS-Chat-1M conversations with two independent detectors: an eight-category lexicon for hostility directed at the model, and the dataset's moderation signal; and show that they capture different, weakly overlapping phenomena. The lexicon identifies insults, threats, and jailbreak coercion aimed at the assistant, while moderation flags are dominated by toxic-content solicitation rather than hostility at the model. Together, they mark about 5% of user turns; adjusting the narrower lexicon-harassment union for measured precision puts mistreatment aimed at the assistant at 0.90%. These absolute rates describe arena-style evaluation traffic and should not be read as deployment-wide base rates. We find that user hostility varies 13-fold across models, driven largely by who each model attracts rather than by model behaviour: first-turn hostility spreads far wider than post-response hostility, and more than fifteenfold separates the extremes even after deduplicating opening prompts. Within conversations, assistant apologies are consistently associated with higher odds of next-turn hostility under both detectors; the effect survives restricting to non-refused prior turns and to jailbreak-free conversations, and is positive in 20 of 23 models. Yet across models, more apologetic models receive less hostility overall. Finally, hostility also shows temporal structure, with coercive openings front-loading the first turn while affective hostility accumulates over a session. We release the lexicon, the detector cross-validation pipeline, and all derived tables.
 
Speaker's bio:
Dr Fanqi Zeng is a UKRI Metascience AI Early Career Fellow (Principal Investigator) in the Department of Sociology and a Junior Research Fellow at Wolfson College, University of Oxford. He is also a Research Associate at the Oxford Internet Institute and a Research Fellow at the Institute for New Economic Thinking at Oxford. He holds a PhD in Engineering Mathematics from the University of Bristol. His research bridges AI and the social sciences, harnessing computational methods and large-scale data to illuminate patterns within complex societal and natural systems. His current work explores the transformative impact of AI on society and human behaviour. His work has been funded by UKRI and the John Fell Fund. His research has appeared in leading interdisciplinary journals, including Science, Nature Cities, Nature Communications, PNAS, and PNAS Nexus.

"Sticking their heads out above the parapets": Lived experiences of legal risks in research

Group: Systems Seminars
Speaker: Daniel Thomas, University of Strathclyde
Date: 24 November, 2026
Time: 14:00 - 15:00
Location: Room 422, Sir Alwyn Williams Building and Teams

Overbroad computer crime, intellectual property, and other laws are well known to create legal risks that can discourage essential research. Notable examples include the US Computer Fraud and Abuse Act and the UK Computer Misuse Act. Because such laws fail to distinguish malicious hacking from good-faith testing and research, researchers face serious legal risks for public-interest research activity like identifying software or hardware vulnerabilities or scraping data. Despite the research community’s broad awareness of these risks, our understanding of their practical impacts is limited, as most of the community’s knowledge comes from anecdotal evidence rather than systematic study. We conduct the first qualitative study focused on researchers’ lived experiences, to empirically document the impacts of legal risks and threats on research and researchers, and how researchers navigate legal risk situations. Our study engages two participant groups: researchers with legal-risk experiences in the UK or the US (NR = 36), who discuss 130 projects and incidents spanning over three decades, and professionals that offer support to researchers navigating legal risks (NS = 8), who have collectively supported thousands of researchers. We thus provide an unprecedented big-picture view of researchers’ experiences with legal risks. We synthesise actionable strategies for researchers, and our findings provide evidence to support policy reform.

Past events

To view past events, please click here

Events Webapp