Formalisation of Security for Federated Learning with DP and Attacker Advantage in IIIf for Satellite Swarms -- Extended Version
Florian Kammüller
TL;DR
This work formalizes the intersection of Federated Learning (FL) and Differential Privacy (DP) within the Isabelle Infrastructure and Insider framework (IIIf), enabling rigorous verification of privacy properties in dynamic distributed settings. It extends prior NI-FL-DP formalism by introducing Attacker Advantage and a probabilistic noninterference framework, complemented by a compositionality theorem that reduces global DP guarantees to client-level reasoning. The satellite swarm case study demonstrates how these formal tools quantify information leakage via FL updates under realistic data-partitioning, linking cryptographic security notions to DP guarantees. By connecting Adv to DP factors, the approach provides interpretable security metrics that can guide defense mechanisms such as gradient sparsification in federated learning. Overall, the work offers a principled, verifiable framework for assessing and bounding information flows in distributed space systems and similar infrastructures.
Abstract
In distributed applications, like swarms of satellites, machine learning can be efficiently applied even on small devices by using Federated Learning (FL). This allows to reduce the learning complexity by transmitting only updates to the general model in the server in the form of differences in stochastic gradient descent. FL naturally supports differential privacy but new attacks, so called Data Leakage from Gradient (DLG) have been discovered recently. There has been work on defenses against DLG but there is a lack of foundation and rigorous evaluation of their security. In the current work, we extend existing work on a formal notion of Differential Privacy for Federated Learning distributed dynamic systems and relate it to the notion of the attacker advantage. This formalisation is carried out within the Isabelle Insider and Infrastructure framework (IIIf) allowing the machine supported verification of theory and applications within the proof assistant Isabelle. Satellite swarm systems are used as a motivating use case but also as a validation case study.