面向卫星编队的联邦学习安全正式化：基于DP与IIIf中的攻击优势
密码学与安全
2025-12-09 v1 计算机科学中的逻辑
摘要
在分布式应用中，如卫星编队，可通过联邦学习（Federated Learning, FL）即使在小型设备上也可高效应用。这允许仅以服务器中模型差异的形式传输更新来减少学习复杂度。联邦学习天然支持差分隐私，但最近发现了名为数据泄露从梯度（DLG）的新型攻击。针对DLG的防御工作已有，但缺乏其安全性的基础和严格评估。本文扩展了现有关于联邦学习分布式动态系统差分隐私正式概念的工作，并将其与攻击优势概念相关联。该正式化在Isabelle Insider and Infrastructure framework（IIIf）中完成，允许在Isabelle证明助手中对理论和应用进行机器支持验证。卫星编队系统用作激励用例，也用作验证案例研究。
引用
@article{arxiv.2512.06467,
title = {Formalisation of Security for Federated Learning with DP and Attacker Advantage in IIIf for Satellite Swarms -- Extended Version},
author = {Florian Kammüller},
journal= {arXiv preprint arXiv:2512.06467},
year = {2025}
}