Abstract
Vulnerability detection and repair is a demanding and expensive part of the software development process. As such, there has been an effort to develop new and better ways to automatically detect and repair vulnerabilities. DifFuzz is a state-of-the-art tool for automatic detection of timing side-channel vulnerabilities, a type of vulnerability that is particularly difficult to detect and correct. Despite recent progress made with tools such as DifFuzz, work on tools capable of automatically repairing timing side-channel vulnerabilities is scarce. In this paper, we propose DifFuzzAR, a tool for automatic repair of timing side-channel vulnerabilities in Java code. The tool works in conjunction with DifFuzz and it is able to repair 56% of the vulnerabilities identified in DifFuzz's dataset. The results show that the tool can automatically correct timing side-channel vulnerabilities, being more effective with those that are control-flow based. In addition, the results of a user study show that users generally trust the refactorings produced by DifFuzzAR and that they see value in such a tool, in particular for more critical code.

Abstract
This research idea paper proposes leveraging Large Language Models (LLMs) to enhance the productivity of Dafny developers. Although the use of verification-aware languages, such as Dafny, has increased considerably in the last decade, these are still not widely adopted. Often the cost of using such languages is too high, due to the level of expertise required from the developers and challenges that they often face when trying to prove a program correct. Even though Dafny automates a lot of the verification process, sometimes there are steps that are too complex for Dafny to perform on its own. One such case is that of missing lemmas, i.e. Dafny is unable to prove a result without being given further help in the form of a theorem that can assist it in the proof of the step. In this paper, we describe preliminary work on using LLMs to assist developers by generating suggestions for relevant lemmas that Dafny is unable to discover and use. Moreover, for the lemmas that cannot be proved automatically, we attempt to provide accompanying calculational proofs. We also discuss ideas for future work by describing a research agenda on using LLMs to increase the adoption of verification-aware languages in general, by increasing developers productivity and by reducing the level of expertise required for crafting formal specifications and proving program properties.

Abstract

Abstract
Formal contracts and assertions are effective methods to enhance software quality by enforcing preconditions, postconditions, and invariants. However, the adoption and impact of contracts in the context of mobile application development, particularly of Android applications, remain unexplored. We present the first large-scale empirical study on the presence and use of contracts in Android applications, written in Java or Kotlin. We consider 2,390 applications and five categories of contract elements: conditional runtime exceptions, APIs, annotations, assertions, and other. We show that most contracts are annotation-based and are concentrated in a small number of applications. © 2024 IEEE Computer Society. All rights reserved.

Abstract
AbstractBreakthroughs in sequencing technologies led to an exponential growth of genomic data, providing unprecedented biological in-sights and new therapeutic applications. However, analyzing such large amounts of sensitive data raises key concerns regarding data privacy, specifically when the information is outsourced to third-party infrastructures for data storage and processing (e.g., cloud computing). Current solutions for data privacy protection resort to centralized designs or cryptographic primitives that impose considerable computational overheads, limiting their applicability to large-scale genomic analysis.We introduce Gyosa, a secure and privacy-preserving distributed genomic analysis solution. Unlike in previous work, Gyosafollows a distributed processing design that enables handling larger amounts of genomic data in a scalable and efficient fashion. Further, by leveraging trusted execution environments (TEEs), namely Intel SGX, Gyosaallows users to confidentially delegate their GWAS analysis to untrusted third-party infrastructures. To overcome the memory limitations of SGX, we implement a computation partitioning scheme within Gyosa. This scheme reduces the number of operations done inside the TEEs while safeguarding the users’ genomic data privacy. By integrating this security scheme inGlow, Gyosaprovides a secure and distributed environment that facilitates diverse GWAS studies. The experimental evaluation validates the applicability and scalability of Gyosa, reinforcing its ability to provide enhanced security guarantees. Further, the results show that, by distributing GWASes computations, one can achieve a practical and usable privacy-preserving solution.

Abstract
The correction of artifacts in Magnetic Resonance Imaging (MRI) is increasingly relevant as voluntary and involuntary artifacts can hinder data acquisition. Reverting from corrupted to artifact-free images is a complex task. Deep Learning (DL) models have been employed to preserve data characteristics and to identify and correct those artifacts. We propose MOANA, a novel DL-based solution to correct artifacts in multi-contrast brain MRI scans. MOANA offers two models: the simulation and the correction models. The simulation model introduces perturbations similar to those occurring in an exam while preserving the original image as ground truth; this is required as publicly available datasets rarely have motion-corrupted images. It allows the addition of three types of artifacts with different degrees of severity. The DL-based correction model adds a fourth contrast to state-of-the-art solutions while improving the overall performance of the models. MOANA achieved the highest results in the FLAIR contrast, with a Structural Similarity Index Measure (SSIM) of 0.9803 and a Normalized Mutual Information (NMI) of 0.8030. With this, the MOANA model can correct large volumes of images in less time and adapt to different levels of artifact severity, allowing for better diagnosis.