Federated learning synchronizes models through gradient transmission and aggregation. However, these gradients pose significant privacy risks, as sensitive training data is embedded within them. Existing gradient inversion attacks suffer from significantly degraded reconstruction performance when gradients are perturbed by noise-a common defense mechanism. In this paper, we introduce gradient-guided conditional diffusion models for reconstructing private images from leaked gradients, without prior knowledge of the target data distribution. Our approach leverages the inherent denoising capability of diffusion models to circumvent the partial protection offered by noise perturbation, thereby improving attack performance under such defenses. We further provide a theoretical analysis of the reconstruction error bounds and the convergence properties of the attack loss, characterizing the impact of key factors—such as noise magnitude and attacked model architecture—on reconstruction quality. Extensive experiments demonstrate our attack's superior reconstruction performance with Gaussian noise-perturbed gradients, and confirm our theoretical findings.

As the marine economy continues to expand, the importance of efficient and reliable marine data collection has become increasingly evident. This paper investigates a multi-unmanned aerial vehicle (UAV)-assisted marine data collection network system, where multiple UAVs are deployed within a designated area to collect data from water buoy sensors (WBSs) and act as relays to offload the collected data to a central ship. The primary objective is to minimize the total system energy consumption, subject to constraints on access relationships, power scheduling, and movement trajectories. The formulated optimization problem is non-convex and highly complex due to the coupling of multiple variables. To address this challenge, we propose an alternating optimization algorithm that jointly optimizes the trajectories of multiple UAVs, the access selection of WBSs, the trajectory of the ship, the data offloading decisions, and the UAV transmit power scheduling in an iterative manner. The algorithm leverages techniques such as successive convex approximation (SCA) and greedy strategies to efficiently solve the decomposed sub-problems. Simulation results demonstrate that the proposed approach achieves significant performance improvements compared to several benchmark algorithms, highlighting its effectiveness in enhancing energy efficiency and system robustness in dynamic marine environments.

As artificial intelligence continues to drive advancements in computer vision, particularly in areas such as image analysis, object detection, and facial recognition, the ability to accurately recognize patterns in visual data has become a central focus of research. However, alongside these advances, concerns about the privacy risks associated with the training data used in AI models have also gained prominence. Deep learning models, frequently employed in computer vision tasks, can unintentionally expose sensitive information from the data they are trained on, raising the need for comprehensive research into privacy-preserving techniques. This paper explores the intersection of AI-driven pattern recognition and the privacy risks involved in training models on image data. Existing studies show that attackers can exploit the gradients from deep learning processes to reconstruct original image data, including personal and identifiable information, such as facial features. By iteratively adjusting input data, attackers can minimize the difference between the gradients of the random and stolen data, leading to the full reconstruction of private images. Current privacy protection methods fall short of explaining the relationship between an attacker’s capacity to recover visual data and the structure of the targeted model. This paper introduces a novel privacy auditing framework that directly assesses the extent to which gradient-based attacks can reconstruct sensitive data. Unlike traditional methods, which mainly focus on mitigating privacy risks through model regularization or data obfuscation, our approach provides a systematic and quantitative evaluation of gradient leakage, filling a critical gap in existing privacy protection techniques. This paper investigates the relationships among reconstructed data, model gradients, and the original input data in the context of computer vision. By formalizing the connection between gradient similarity and data similarity, we propose a novel methodology that quantifies the vulnerability of deep learning models to data reconstruction attacks. Building on these insights, we propose a novel privacy auditing method aimed at evaluating the privacy risks associated with deep learning models used in pattern recognition for image data.

Automatic Program Repair (APR) is a practical research topic that studies techniques to automatically repair programs to fix bugs. Most existing APR techniques are designed for imperative programming languages, such as C and Java, and rely on analyzing correct and incorrect executions of programs to identify and repair suspicious statements.

Automated program repair (APR) techniques have shown great success in automatically finding fixes for programs in programming languages such as C or Java. In this work, we focus on repairing formal specifications, in particular for the Alloy specification language. As opposed to most APR tools, our approach to repair Alloy specifications, named ICEBAR, does not use test-based oracles for patch assessment. Instead, ICEBAR relies on the use of property-based oracles, commonly found in Alloy specifications as predicates and assertions. These property-based oracles define stronger conditions for patch assessment, thus reducing the notorious overfitting issue caused by using test-based oracles, typically observed in APR contexts. Moreover, as assertions and predicates are inherent to Alloy, whereas test cases are not, our tool is potentially more appealing to Alloy users than test-based Alloy repair tools.

The rising popularity of declarative languages and the hard to debug nature thereof have motivated the need for applicable, automated repair techniques for such languages. However, despite significant advances in the program repair of imperative languages, there is a dearth of repair techniques for declarative languages. This paper presents BeAFix, an automated repair technique for faulty models written in Alloy, a declarative language based on first-order relational logic. BeAFix is backed with a novel strategy for bounded exhaustive, yet scalable, exploration of the spaces of fix candidates and a formally rigorous, sound pruning of such spaces. Moreover, different from the state-of-the-art in Alloy automated repair, that relies on the availability of unit tests, BeAFix does not require tests and can work with assertions that are naturally used in formal declarative languages. Our experience with using BeAFix to repair thousands of real-world faulty models, collected by other researchers, corroborates its ability to effectively generate correct repairs and outperform the state-of-the-art.

Fault localization is a practical research topic that helps developers identify code locations that might cause bugs in a program. Most existing fault localization techniques are designed for imperative programs (e.g., C and Java) and rely on analyzing correct and incorrect executions of the program to identify suspicious statements. In this work, we introduce a fault localization approach for models written in a declarative language, where the models are not "executed," but rather converted into a logical formula and solved using backend constraint solvers. We present FLACK, a tool that takes as input an Alloy model consisting of some violated assertion and returns a ranked list of suspicious expressions contributing to the assertion violation. The key idea is to analyze the differences between counterexamples, i.e., instances of the model that do not satisfy the assertion, and instances that do satisfy the assertion to find suspicious expressions in the input model. The experimental results show that FLACK is efficient (can handle complex, real-world Alloy models with thousand lines of code within 5 seconds), accurate (can consistently rank buggy expressions in the top 1.9% of the suspicious list), and useful (can often narrow down the error to the exact location within the suspicious expressions).

This paper describes BeAFix, a tool for automated repair of faulty Alloy models. The tool builds upon the Alloy Analyzer, the analysis tool for Alloy. It generates repair candidates by mutating a faulty Alloy model, and employs a bounded-exhaustive approach to traverse the space of repair candidates. Since BeAFix’s mutation operators make the space of repair candidates to quickly grow, the tool supports some sound pruning techniques, that allow it to fix Alloy models with more than one faulty line or expression. Additionally, BeAFix does not require tests as a patch acceptance criterion. Although BeAFix supports tests as oracles, our tool is also able to leverage property-based oracles, which are more commonly found in Alloy models in the form of predicate satisfiability and assertion validity checks.A video demonstration of BeAFix can be found at https://youtu.be/5RG40SmlFXQ. The tool’s binaries and further details about its usage, can all be found at https://sites.google.com/view/beafixevaluation/beafix. The tool is also available in a public archive at https://doi.org/10.5281/zenodo.5296466.

Fault localization can help developers identify buggy statements or expressions in programs. Existing fault localization techniques are often designed for imperative programs (e.g., C and Java) and rely on tests to compare correct and incorrect execution traces to identify suspicious statements. In this demo paper, we present FLACK, a tool to automatically locate faults for models written in Alloy, a declarative language where the models are not executed but instead converted into a logical formula and solved using a SAT solver. FLACK takes as input an Alloy model that violates some assertions and returns a ranked list of suspicious expressions contributing to the violation. The key idea is to analyze the differences between counterexamples, i.e., instances of the model that do not satisfy the assertion and instances that do satisfy the assertion to find suspicious expressions in the input model. An experiment with 157 Alloy models with various bugs shows the efficiency and accuracy of FLACK in localizing the causes of these bugs. FLACK and its evaluation benchmark and results can be downloaded from https://github.com/guolong-zheng/flack. The video demonstration is available at https://youtu.be/FKa2ohqIUms.

Alloy is a lightweight specification language based on relational logic, with an analysis engine that relies on SAT solvers to automate bounded verification of specifications. In spite of its strengths, the reliance of the Alloy Analyzer on computationally heavy solvers means that it can take a significant amount of time to verify software properties, even within limited bounds. This challenge is exacerbated by the ever-evolving nature of complex software systems. This paper presents Platinum , a technique for efficient analysis of evolving Alloy specifications, that recognizes opportunities for constraint reduction and reuse of previously identified constraint solutions. The insight behind Platinum is that formula constraints recur often during the analysis of a single specification and across its revisions, and constraint solutions can be reused over sequences of analyses performed on evolving specifications. Our empirical results show that Platinum substantially reduces (by 66.4% on average) the analysis time required on specifications extracted from real-world software systems.

Debugging, which involves both fault localization and bug repair, is critical for developers to identify and remove bugs in a program. Most existing debugging research techniques focus on imperative programs (e.g., C and Java) and rely on test suite to analyze correct and incorrect executions of the program to identify and repair suspicious statements.We propose a new debugging framework for models written in a declarative language, where the models are not "executed", but rather converted into a logical formula solvable using a constraint solver. In recent work, we developed a fault localization tool that takes as input an Alloy model consisting of a violated assertion and returns a ranked list of suspicious expressions contributing to the violation. Preliminary results show that the fault localization tool is accurate, useful, and scales to complex, real-world Alloy models.In this work, we propose a new repair technique and tool that can be integrated with our fault localization tool or used as a stand-alone tool. We aim to automatic repair bugs violating given assertions in Alloy models. We plan to adopt guided search and pattern-based repair techniques from imperative automatic program repair and modify DFA learning algorithms to synthesis repairs.

We introduce a new dynamic analysis technique to discover invariants in separation logic for heap-manipulating programs. First, we use a debugger to obtain rich program execution traces at locations of interest on sample inputs. These traces consist of heap and stack information of variables that point to dynamically allocated data structures. Next, we iteratively analyze separate memory regions related to each pointer variable and search for a formula over predefined heap predicates in separation logic to model these regions. Finally, we combine the computed formulae into an invariant that describes the shape of explored memory regions.