Formal Logic-guided Robust Federated Learning against Poisoning Attacks

TL;DR

FLORAL is presented, a defense mechanism designed to mitigate poisoning attacks in federated learning for time-series tasks, even in scenarios with heterogeneous client data and a large number of adversarial participants, highlighting its potential to enhance the robustness of FL to time series applications.

Abstract

Federated Learning (FL) offers a promising solution to the privacy concerns associated with centralized Machine Learning (ML) by enabling decentralized, collaborative learning. However, FL is vulnerable to various security threats, including poisoning attacks, where adversarial clients manipulate the training data or model updates to degrade overall model performance. Recognizing this threat, researchers have focused on developing defense mechanisms to counteract poisoning attacks in FL systems. However, existing robust FL methods predominantly focus on computer vision tasks, leaving a gap in addressing the unique challenges of FL with time series data. In this paper, we present FLORAL, a defense mechanism designed to mitigate poisoning attacks in federated learning for time-series tasks, even in scenarios with heterogeneous client data and a large number of adversarial participants. Unlike traditional model-centric defenses, FLORAL leverages logical reasoning to evaluate client trustworthiness by aligning their predictions with global time-series patterns, rather than relying solely on the similarity of client updates. Our approach extracts logical reasoning properties from clients, then hierarchically infers global properties, and uses these to verify client updates. Through formal logic verification, we assess the robustness of each client contribution, identifying deviations indicative of adversarial behavior. Experimental results on two datasets demonstrate the superior performance of our approach compared to existing baseline methods, highlighting its potential to enhance the robustness of FL to time series applications. Notably, FLORAL reduced the prediction error by 93.27% in the best-case scenario compared to the second-best baseline. Our code is available at https://anonymous.4open.science/r/FLORAL-Robust-FTS.

Figures (4)

• Figure 1: Illustration of logical verification given by benign and malicious clients' predictions. The global property here is $\square_{(0, 10]} (\hat{y}(t) \leq p_1) \wedge \square_{(10, 20]} (\hat{y}(t) \leq p_2) \wedge \square_{(20, 30]} (\hat{y}(t) \leq p_3) \wedge \square_{(30, 40]} (\hat{y}(t) \leq p_4)$. Examples of points violating this property are marked with x.
• Figure 2: Overview of FLORAL. For each training round, FLORAL first conducts local logic inference to acquire the local reasoning properties; which are then used as criterion to cluster clients. Global property $\varphi_g$ is calculated by aggregation of clustered properties. Using $\varphi_g$, the server $\mathcal{S}$ verifies the satisfaction scores $\theta$ for each clients and use them to determine the suspicious updates to be removed from final aggregation.
• Figure 3: Zoom-in analysis of our method's robustness against Byzantine Attacks, compared to various defense mechanisms under different attack ratios $\epsilon$.
• Figure 4: Zoom-in robustness of our method when applied with different model architectures.

Theorems & Definitions (8)

• Definition 1: STL syntax
• Definition 2: STL property inference
• Example 1: Example of STL inference
• Definition 3: STL property inference under a tight bound
• Definition 4: Robustness Score $\theta$
• Example 2: Example of STL verification
• Definition 5: STL Qualitative Semantics
• Definition 6: STL Quantitative Semantics