arXiv subjects

João F. Ferreira

Publications and source records attributed to João F. Ferreira.

At least 19 recordsLinked to original sources

arXiv2026

A Systematic Review of Security Communication Strategies: Guidelines and Open Challenges

Cybersecurity incidents such as data breaches have become increasingly common, affecting millions of users and organizations worldwide. The complexity of cybersecurity threats challenges the effectiveness of existing security communication strategies. Through a systematic review of over 3,400 papers, we identify specific user difficulties including information overload, technical jargon comprehension, and balancing security awareness with comfort. Our findings reveal consistent communication paradoxes: users require technical details for credibility yet struggle with jargon and need risk awareness without experiencing anxiety. We propose seven evidence-based guidelines to improve security communication and identify critical research gaps including limited studies with older adults, children, and non-US populations, insufficient longitudinal research, and limited protocol sharing for reproducibility. Our guidelines emphasize user-centric communication adapted to cultural and demographic differences while ensuring security advice remains actionable. This work contributes to more effective security communication practices that enable users to recognize and respond to cybersecurity threats appropriately.

cs.CR↗

arXiv2026

The Ultimate Configuration Management Tool? Lessons from a Mixed Methods Study of Ansible's Challenges

Infrastructure as Code (IaC) tools have transformed the way IT infrastructure is automated and managed, but their growing adoption has also exposed numerous challenges for practitioners. In this paper, we investigate these challenges through the lens of Ansible, a popular IaC tool. Using a mixed methods approach, we investigate challenges faced by practitioners. We analyze 59,157 posts from Stack Overflow, Reddit, and the Ansible Forum to identify common pain points, complemented by 20 semi-structured interviews with practitioners of varying expertise levels. Based on our findings, we highlight key directions for improving Ansible, with implications for other IaC technologies, including stronger failure locality to support debugging, clearer separation of language and templating boundaries, targeted documentation, and improved execution backends to address performance issues. By grounding these insights in the real-world struggles of Ansible users, this study provides actionable guidance for tool designers and for the broader IaC community, and contributes to a deeper understanding of the trade-offs inherent in IaC tools.

cs.SE↗

arXiv2025

Environmental Impact of CI/CD Pipelines

CI/CD pipelines are widely used in software development, yet their environmental impact, particularly carbon and water footprints (CWF), remains largely unknown to developers, as CI service providers typically do not disclose such information. With the growing environmental impact of cloud computing, understanding the CWF of CI/CD services has become increasingly important. This work investigates the CWF of using GitHub Actions, focusing on open-source repositories where usage is free and unlimited for standard runners. We build upon a methodology from the Cloud Carbon Footprint framework and we use the largest dataset of workflow runs reported in the literature to date, comprising over 2.2 million workflow runs from more than 18,000 repositories. Our analysis reveals that the GitHub Actions ecosystem results in a substantial CWF. Our estimates for the carbon footprint in 2024 range from 150.5 MTCO2e in the most optimistic scenario to 994.9 MTCO2e in the most pessimistic scenario, while the water footprint ranges from 1,989.6 to 37,664.5 kiloliters. The most likely scenario estimates are 456.9 MTCO2e for carbon footprint and 5,738.2 kiloliters for water footprint. To provide perspective, the carbon footprint in the most likely scenario is equivalent to the carbon captured by 7,615 urban trees in a year, and the water footprint is comparable to the water consumed by an average American family over 5,053 years. We explore strategies to mitigate this impact, primarily by reducing wasted computational resources. Key recommendations include deploying runners in regions whose energy production has a low environmental impact such as France and the United Kingdom, implementing stricter deactivation policies for scheduled runs and aligning their execution with periods when the regional energy mix is more environmentally favorable, and reducing the size of repositories.

cs.SE↗

arXiv2025

Structuring Security: A Survey of Cybersecurity Ontologies, Semantic Log Processing, and LLMs Application

This survey investigates how ontologies, semantic log processing, and Large Language Models (LLMs) enhance cybersecurity. Ontologies structure domain knowledge, enabling interoperability, data integration, and advanced threat analysis. Security logs, though critical, are often unstructured and complex. To address this, automated construction of Knowledge Graphs (KGs) from raw logs is emerging as a key strategy for organizing and reasoning over security data. LLMs enrich this process by providing contextual understanding and extracting insights from unstructured content. This work aligns with European Union (EU) efforts such as NIS 2 and the Cybersecurity Taxonomy, highlighting challenges and opportunities in intelligent ontology-driven cyber defense.

cs.CR↗

arXiv2025

Are Users More Willing to Use Formally Verified Password Managers?

Formal verification has recently been increasingly used to prove the correctness and security of many applications. It is attractive because it can prove the absence of errors with the same certainty as mathematicians proving theorems. However, while most security experts recognize the value of formal verification, the views of non-technical users on this topic are unknown. To address this issue, we designed and implemented two experiments to understand how formal verification impacts users. Our approach started with a formative study involving 15 participants, followed by the main quantitative study with 200 individuals. We focus on the application domain of password managers since it has been documented that the lack of trust in password managers might lead to lower adoption. Moreover, recent efforts have focused on formally verifying (parts of) password managers. We conclude that formal verification is seen as desirable by users and identify three actional recommendations to improve formal verification communication efforts.

cs.CR↗

arXiv2025

InfraFix: Technology-Agnostic Repair of Infrastructure as Code

Infrastructure as Code (IaC) enables scalable and automated IT infrastructure management but is prone to errors that can lead to security vulnerabilities, outages, and data loss. While prior research has focused on detecting IaC issues, Automated Program Repair (APR) remains underexplored, largely due to the lack of suitable specifications. In this work, we propose InfraFix, the first technology-agnostic framework for repairing IaC scripts. Unlike prior approaches, InfraFix allows APR techniques to be guided by diverse information sources. Additionally, we introduce a novel approach for generating repair scenarios, enabling large-scale evaluation of APR techniques for IaC. We implement and evaluate InfraFix using an SMT-based repair module and a state inference module that uses system calls, demonstrating its effectiveness across 254,288 repair scenarios with a success rate of 95.7%. Our work provides a foundation for advancing APR in IaC by enabling researchers to experiment with new state inference and repair techniques using InfraFix and to evaluate their approaches at scale with our repair scenario generation method.

cs.SE↗

arXiv2025

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

Formal verification using proof assistants, such as Coq, enables the creation of high-quality software. However, the verification process requires significant expertise and manual effort to write proofs. Recent work has explored automating proof synthesis using machine learning and large language models (LLMs). This work has shown that identifying relevant premises, such as lemmas and definitions, can aid synthesis. We present Rango, a fully automated proof synthesis tool for Coq that automatically identifies relevant premises and also similar proofs from the current project and uses them during synthesis. Rango uses retrieval augmentation at every step of the proof to automatically determine which proofs and premises to include in the context of its fine-tuned LLM. In this way, Rango adapts to the project and to the evolving state of the proof. We create a new dataset, CoqStoq, of 2,226 open-source Coq projects and 196,929 theorems from GitHub, which includes both training data and a curated evaluation benchmark of well-maintained projects. On this benchmark, Rango synthesizes proofs for 32.0% of the theorems, which is 29% more theorems than the prior state-of-the-art tool Tactician. Our evaluation also shows that Rango adding relevant proofs to its context leads to a 47% increase in the number of theorems proven.

cs.SE↗

arXiv2024

CoqPyt: Proof Navigation in Python in the Era of LLMs

Proof assistants enable users to develop machine-checked proofs regarding software-related properties. Unfortunately, the interactive nature of these proof assistants imposes most of the proof burden on the user, making formal verification a complex, and time-consuming endeavor. Recent automation techniques based on neural methods address this issue, but require good programmatic support for collecting data and interacting with proof assistants. This paper presents CoqPyt, a Python tool for interacting with the Coq proof assistant. CoqPyt improves on other Coq-related tools by providing novel features, such as the extraction of rich premise data. We expect our work to aid development of tools and techniques, especially LLM-based, designed for proof synthesis and repair. A video describing and demonstrating CoqPyt is available at: https://youtu.be/fk74o0rePM8.

cs.SE↗

arXiv2024

Skeptic: Automatic, Justified and Privacy-Preserving Password Composition Policy Selection

The choice of password composition policy to enforce on a password-protected system represents a critical security decision, and has been shown to significantly affect the vulnerability of user-chosen passwords to guessing attacks. In practice, however, this choice is not usually rigorous or justifiable, with a tendency for system administrators to choose password composition policies based on intuition alone. In this work, we propose a novel methodology that draws on password probability distributions constructed from large sets of real-world password data which have been filtered according to various password composition policies. Password probabilities are then redistributed to simulate different user password reselection behaviours in order to automatically determine the password composition policy that will induce the distribution of user-chosen passwords with the greatest uniformity, a metric which we show to be a useful proxy to measure overall resistance to password guessing attacks. Further, we show that by fitting power-law equations to the password probability distributions we generate, we can justify our choice of password composition policy without any direct access to user password data. Finally, we present Skeptic -- a software toolkit that implements this methodology, including a DSL to enable system administrators with no background in password security to compare and rank password composition policies without resorting to expensive and time-consuming user studies. Drawing on 205,176,321 pass words across 3 datasets, we lend validity to our approach by demonstrating that the results we obtain align closely with findings from a previous empirical study into password composition policy effectiveness.

cs.CR↗

arXiv2024

Contract Usage and Evolution in Android Mobile Applications

Formal contracts and assertions are effective methods to enhance software quality by enforcing preconditions, postconditions, and invariants. Previous research has demonstrated the value of contracts in traditional software development contexts. However, the adoption and impact of contracts in the context of mobile application development, particularly of Android applications, remain unexplored. To address this, 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 different types of contract elements divided into five categories: conditional runtime exceptions, APIs, annotations, assertions, and other. We analyzed 2,390 Android applications from the F-Droid repository and processed more than 51,749 KLOC to determine 1) how and to what extent contracts are used, 2) how contract usage evolves, and 3) whether contracts are used safely in the context of program evolution and inheritance. Our findings include: 1) although most applications do not specify contracts, annotation-based approaches are the most popular among practitioners; 2) applications that use contracts continue to use them in later versions, but the number of methods increases at a higher rate than the number of contracts; and 3) there are many potentially unsafe specification changes when applications evolve and in subtyping relationships, which indicates a lack of specification stability. Our findings show that it would be desirable to have libraries that standardize contract specifications in Java and Kotlin, and tools that aid practitioners in writing stronger contracts and in detecting contract violations in the context of program evolution and inheritance.

cs.SE↗

arXiv2024

Leveraging Large Language Models to Boost Dafny's Developers Productivity

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 a new Dafny plugin that leverages 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, the plugin also attempts 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.

cs.SE↗

arXiv2023

Evolution of Automated Weakness Detection in Ethereum Bytecode: a Comprehensive Study

Blockchain programs (also known as smart contracts) manage valuable assets like cryptocurrencies and tokens, and implement protocols in domains like decentralized finance (DeFi) and supply-chain management. These types of applications require a high level of security that is hard to achieve due to the transparency of public blockchains. Numerous tools support developers and auditors in the task of detecting weaknesses. As a young technology, blockchains and utilities evolve fast, making it challenging for tools and developers to keep up with the pace. In this work, we study the robustness of code analysis tools and the evolution of weakness detection on a dataset representing six years of blockchain activity. We focus on Ethereum as the crypto ecosystem with the largest number of developers and deployed programs. We investigate the behavior of single tools as well as the agreement of several tools addressing similar weaknesses. Our study is the first that is based on the entire body of deployed bytecode on Ethereum's main chain. We achieve this coverage by considering bytecodes as equivalent if they share the same skeleton. The skeleton of a bytecode is obtained by omitting functionally irrelevant parts. This reduces the 48 million contracts deployed on Ethereum up to January 2022 to 248328 contracts with distinct skeletons. For bulk execution, we utilize the open-source framework SmartBugs that facilitates the analysis of Solidity smart contracts, and enhance it to accept also bytecode as the only input. Moreover, we integrate six further tools for bytecode analysis. The execution of the 12 tools included in our study on the dataset took 30 CPU years. While the tools report a total of 1307486 potential weaknesses, we observe a decrease in reported weaknesses over time, as well as a degradation of tools to varying degrees.

cs.CR↗

arXiv2023

Polyglot Code Smell Detection for Infrastructure as Code with GLITCH

This paper presents GLITCH, a new technology-agnostic framework that enables automated polyglot code smell detection for Infrastructure as Code scripts. GLITCH uses an intermediate representation on which different code smell detectors can be defined. It currently supports the detection of nine security smells and nine design & implementation smells in scripts written in Ansible, Chef, Docker, Puppet, or Terraform. Studies conducted with GLITCH not only show that GLITCH can reduce the effort of writing code smell analyses for multiple IaC technologies, but also that it has higher precision and recall than current state-of-the-art tools. A video describing and demonstrating GLITCH is available at: https://youtu.be/E4RhCcZjWbk

cs.CR↗

arXiv2023

SmartBugs 2.0: An Execution Framework for Weakness Detection in Ethereum Smart Contracts

Smart contracts are blockchain programs that often handle valuable assets. Writing secure smart contracts is far from trivial, and any vulnerability may lead to significant financial losses. To support developers in identifying and eliminating vulnerabilities, methods and tools for the automated analysis have been proposed. However, the lack of commonly accepted benchmark suites and performance metrics makes it difficult to compare and evaluate such tools. Moreover, the tools are heterogeneous in their interfaces and reports as well as their runtime requirements, and installing several tools is time-consuming. In this paper, we present SmartBugs 2.0, a modular execution framework. It provides a uniform interface to 19 tools aimed at smart contract analysis and accepts both Solidity source code and EVM bytecode as input. After describing its architecture, we highlight the features of the framework. We evaluate the framework via its reception by the community and illustrate its scalability by describing its role in a study involving 3.25 million analyses.

cs.CR↗

arXiv2023

MUFIN: Improving Neural Repair Models with Back-Translation

Automated program repair is the task of automatically repairing software bugs. A promising direction in this field is self-supervised learning, a learning paradigm in which repair models are trained without commits representing pairs of bug/fix. In self-supervised neural program repair, those bug/fix pairs are generated in some ways. The main problem is to generate interesting and diverse pairs that maximize the effectiveness of training. As a contribution to this problem, we propose to use back-translation, a technique coming from neural machine translation. We devise and implement MUFIN, a back-translation training technique for program repair, with specifically designed code critics to select high-quality training samples. Our results show that MUFIN's back-translation loop generates valuable training samples in a fully automated, self-supervised manner, generating more than half-a-million pairs of bug/fix. The code critic design is key because of a fundamental trade-off between how restrictive a critic is and how many samples are available for optimization during back-translation.

cs.SE↗

arXiv2022

GLITCH: Automated Polyglot Security Smell Detection in Infrastructure as Code

Infrastructure as Code (IaC) is the process of managing IT infrastructure via programmable configuration files (also called IaC scripts). Like other software artifacts, IaC scripts may contain security smells, which are coding patterns that can result in security weaknesses. Automated analysis tools to detect security smells in IaC scripts exist, but they focus on specific technologies such as Puppet, Ansible, or Chef. This means that when the detection of a new smell is implemented in one of the tools, it is not immediately available for the technologies supported by the other tools -- the only option is to duplicate the effort. This paper presents an approach that enables consistent security smell detection across different IaC technologies. We conduct a large-scale empirical study that analyzes security smells on three large datasets containing 196,755 IaC scripts and 12,281,251 LOC. We show that all categories of security smells are identified across all datasets and we identify some smells that might affect many IaC projects. To conduct this study, we developed GLITCH, a new technology-agnostic framework that enables automated polyglot smell detection by transforming IaC scripts into an intermediate representation, on which different security smell detectors can be defined. GLITCH currently supports the detection of nine different security smells in scripts written in Ansible, Chef, or Puppet. We compare GLITCH with state-of-the-art security smell detectors. The results obtained not only show that GLITCH can reduce the effort of writing security smell analyses for multiple IaC technologies, but also that it has higher precision and recall than the current state-of-the-art tools.

cs.CR↗

arXiv2022

Asteroid astrometry by stellar occultations: Accuracy of the existing sample from orbital fitting

Context: Stellar occultations, greatly enhanced by the publication of the Gaia data releases, permit not only the determination of asteroid size and shape, but also the retrieval of additional, accurate astrometry, with a possible relevant impact on the study of dynamical properties. The use of Gaia as reference catalogue and the recent implementation of an improved error model for occultation astrometry offer the opportunity to test its global astrometric performance on the existing data set of observed events, dominated by minor planets belonging to the main belt. Aims: We aim to explore the performance on orbit accuracy brought by reducing occultations by stellar positions given in Gaia Data Release 2 (DR2) and Early Data Release 3 (EDR3), exploited jointly with the new occultation error model. Our goal is to verify that the quality of DR2 and EDR3 provides a logical progression in the exploitation of occultation astrometry with respect to previous catalogues. We also want to compare the post-fit residuals to the error model. Methods: We began with accurate orbit adjustment to occultation data, either alone or joined to the other available ground-based observations. We then analyzed the orbit accuracy and the post-fit residuals. Results: Gaia EDR3 and DR2 bring a noticeable improvement to the accuracy of occultation data, bringing an average reduction of their residuals upon fitting an orbit of about a factor of 5 when compared to other catalogues. This is particularly visible when occultations alone are used, resulting in very good orbits for a large fraction of objects. We demonstrate that occultation astrometry can reach the performance of Gaia on small asteroids. The joint use of archival data and occultations remains more challenging due to the higher uncertainties and systematic errors of other data, mainly obtained by traditional CCD imaging.

astro-ph.EP↗

arXiv2021

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

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.

cs.HC↗