Alexandra Sofia Mendes

Abstract
The exponential growth in the digitisation of services implies the handling and storage of large volumes of data. Businesses and services see data sharing and crossing as an opportunity to improve and produce new business opportunities. The health sector is one area where this proves to be true, enabling better and more innovative treatments. Notwithstanding, this raises concerns regarding personal data being treated and processed. In this paper, we present a patient-centric platform for the secure sharing of health records by shifting the control over the data to the patient, therefore, providing a step further towards data sovereignty. Data sharing is performed only with the consent of the patient, allowing it to revoke access at any given time. Furthermore, we also provide a break-glass approach, resorting to Proxy Re-encryption (PRE) and the concept of a centralised trusted entity that possesses instant access to patients' medical records. Lastly, an analysis is made to assess the performance of the platform's key operations, and the impact that a PRE scheme has on those operations.

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.