Carolina Carreira

McKenna McCall, Carolina Carreira, Miguel Flores et al.

Trusted Execution Environments (TEEs) protect confidentiality and integrity of trusted applications by creating an isolated environment for executing code. Prior work has shown that users may feel more comfortable sharing data when they know it will be protected by a TEE, especially if they understand what a TEE is. In this study, we evaluated text-based explanations introducing TEEs to non-experts. We analyzed existing TEE explanations to develop candidate explanations and evaluated them via vignette scenarios with 966 crowdworkers. The explanations that enhanced understanding most were non-technical ones that highlighted specific threats that can be prevented by a TEE. Surprisingly, even the explanations that enhanced understanding had little effect on willingness to use the TEE-enhanced technology. These results provide insights into ways to communicate technical security concepts more effectively but also suggest that explaining security technology might not be enough to address users' privacy concerns.

Carolina Carreira, Nuno Saavedra, Alexandra Mendes et al.

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.

Carolina Carreira, João F. Ferreira, Alexandra Mendes et al.

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.