Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Interest
Topics
Details

Details

  • Name

    Alexandra Sofia Mendes
  • Cluster

    Computer Science
  • Role

    Senior Researcher
  • Since

    15th February 2018
002
Publications

2023

bGSL: An imperative language for specification and refinement of backtracking programs

Authors
Dunne, S; Ferreira, JF; Mendes, A; Ritchie, C; Stoddart, B; Zeyda, F;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
We present an imperative refinement language for the development of backtracking programs and discuss its semantic foundations. For expressivity, our language includes prospective values and preference - the latter being a variant of Nelson's biased choice that backtracks from infeasibility of a continuation. Our key contribution is to examine feasibility-preserving refinement as a basis for developing backtracking programs, and several key refinement laws that enable compositional refinement in the presence of non -monotonic program combinators.

2022

Verified Password Generation from Password Composition Policies

Authors
Grilo, M; Campos, J; Ferreira, JF; Almeida, JB; Mendes, A;

Publication
INTEGRATED FORMAL METHODS, IFM 2022

Abstract
Password managers (PMs) are important tools that enable the use of stronger passwords, freeing users from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust PMs. In this paper, we focus on a feature that most PMs offer that might impact the user's trust, which is the process of generating a random password. We present three of the most commonly used algorithms and we propose a solution for a formally verified reference implementation of a password generation algorithm. We use EasyCrypt to specify and verify our reference implementation. In addition, we present a proof-of-concept prototype that extends Bitwarden to only generate compliant passwords, solving a frequent users' frustration with PMs. This demonstrates that our formally verified component can be integrated into an existing (and widely used) PM.

2022

Extending EcoAndroid with Automated Detection of Resource Leaks

Authors
Pereira, RB; Ferreira, JF; Mendes, A; Abreu, R;

Publication
9TH IEEE/ACM INTERNATIONAL CONFERENCE ON MOBILE SOFTWARE ENGINEERING AND SYSTEMS, MOBILESOFT 2022

Abstract
When developing mobile applications, developers often have to decide when to acquire and when to release resources. This leads to resource leaks, a kind of bug where a resource is acquired but never released. This is a common problem in Android applications that can degrade energy efficiency and, in some cases, can cause resources to not function properly. In this paper, we present an extension of EcoAndroid, an Android Studio plugin that improves the energy efficiency of Android applications, with an inter-procedural static analysis that detects resource leaks. Our analysis is implemented using Soot, FlowDroid, and Heros, which provide a static-analysis environment capable of processing Android applications and performing inter-procedural analysis with the IFDS framework. It currently supports the detection of leaks related to four Android resources: Cursor, SQLite-Database, Wakelock, and Camera. We evaluated our tool with the DroidLeaks benchmark and compared it with 8 other resource leak detectors. We obtained a precision of 72.5% and a recall of 83.2%. Our tool was able to uncover 191 previously unidentified leaks in this benchmark. These results show that our analysis can help developers identify resource leaks.

2021

Exploring Usable Security to Improve the Impact of Formal Verification: A Research Agenda

Authors
Carreira, C; Ferreira, JF; Mendes, A; Christin, N;

Publication
Proceedings First Workshop on Applicable Formal Methods, AppFM@FM 2021, virtual, 23rd November 2021.

Abstract
As software becomes more complex and assumes an even greater role in our lives, formal verification is set to become the gold standard in securing software systems into the future, since it can guarantee the absence of errors and entire classes of attack. Recent advances in formal verification are being used to secure everything from unmanned drones to the internet. At the same time, the usable security research community has made huge progress in improving the usability of security products and end-users comprehension of security issues. However, there have been no human-centered studies focused on the impact of formal verification on the use and adoption of formally verified software products. We propose a research agenda to fill this gap and to contribute with the first collection of studies on people's mental models on formal verification and associated security and privacy guarantees and threats. The proposed research has the potential to increase the adoption of more secure products and it can be directly used by the security and formal methods communities to create more effective and secure software tools. © C. Carreira et al.

2021

Formal Methods Teaching - 4th International Workshop and Tutorial, FMTea 2021, Virtual Event, November 21, 2021, Proceedings

Authors
Ferreira, JF; Mendes, A; Menghi, C;

Publication
FMTea

Abstract