VLDB 2026 Research / reviewers in the wild / expert
Pedro Fonseca 0001
dblp:11/3119-1
· DBLP profile ↗
32ranked-venue papers
6as first author
19since 2021 · last 2026
0000-0003-2480-4487ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Systems, architecture and hardware · 18 · 5 first-author · 9 since 2021Software engineering, systems software and programming languages · 14 · 1 first-author · 11 since 2021Security and privacy · 5 · 1 first-author · 3 since 2021Computer networks · 2 · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Rose: Reproducing External-Fault-Induced Failures in Distributed Systems with Lightweight InstrumentationabstractDistributed systems form the backbone of critical infrastructures, yet remain vulnerable to external-fault-induced bugs that manifest only when specific external events occur during specific application states. Existing approaches to reproducing these bugs require fine-grained information about the application, which might not be available in production, and operate within a limited fault model. Rose is a novel approach that collects traces from production and systematically generates fault schedules that reproduce these bugs. By leveraging the insight that external faults are observable through system interfaces, Rose uses lightweight tracing (2.6% overhead) to capture essential application-environment interactions. Then, it identifies the application states when faults must occur to trigger bugs, and generates schedules that consistently reproduce these bugs. Rose reproduced 20 bugs across eight production systems implemented in diverse languages (C, C++, Java, Go, Scala), including widely-used systems such as Zookeeper, MongoDB, and HBase. Sebastião Amaro, Pedro Fonseca 0001, Miguel Matos |
EuroSys | 2 |
| 2026 | UpFuzz: Detecting Data Format Incompatibility Bugs during Distributed Storage System Upgrade
P. C. Sruthi, Yayu Wang, Yaoxu Song, Bishal Basak Papan, Pedro Fonseca 0001, Yongle Zhang 0007 |
NSDI | 7 |
| 2025 | Snowplow: Effective Kernel Fuzzing with a Learned White-box Test MutatorabstractKernel fuzzers rely heavily on program mutation to automatically generate new test programs based on existing ones. In particular, program mutation can alter the test's control and data flow inside the kernel by inserting new system calls, changing the values of call arguments, or performing other program mutations. However, due to the complexity of the kernel code and its user-space interface, finding the effective mutation that can lead to the desired outcome such as increasing the coverage and reaching a target code location is extremely difficult, even with the widespread use of manually-crafted heuristics. Sishuai Gong, Wang Rui, Deniz Altinbüken, Pedro Fonseca 0001, Petros Maniatis |
ASPLOS (2) | 4 |
| 2025 | Pegasus: Transparent and Unified Kernel-Bypass Networking for Fast Local and Remote CommunicationabstractModern software architectures in cloud computing are highly reliant on interconnected local and remote services. Popular architectures, such as the service mesh, rely on the use of independent services or sidecars for a single application. While such modular approaches simplify application development and deployment, they also introduce significant communication overhead since now even local communication that is handled by the kernel becomes a performance bottleneck. This problem has been identified and partially solved for remote communication over fast NICs through the use of kernel-bypass data plane systems. However, existing kernel-bypass mechanisms challenge their practical deployment by either requiring code modification or supporting only a small subset of the network interface. Dinglan Peng, Congyu Liu, Tapti Palit, Anjo Vahldiek-Oberwagner, Mona Vij, Pedro Fonseca 0001 |
EuroSys | 6 |
| 2025 | KRR: Efficient and Scalable Kernel Record Replay
Sishuai Gong, Pedro Fonseca 0001 |
OSDI | 3 |
| 2024 | Kaleidoscope: Precise Invariant-Guided Pointer AnalysisabstractPointer analysis techniques are crucial for many software security mitigation approaches. However, these techniques suffer from imprecision; hence, the reported points-to sets are a superset of the actual points-to sets that can possibly form during program execution. To improve the precision of pointer analysis techniques, we propose Kaleidoscope. By using an invariant-guided optimistic (IGO) pointer analysis approach, Kaleidoscope makes optimistic assumptions during the pointer analysis that it later validates at runtime. If these optimistic assumptions do not hold true at runtime, Kaleidoscope falls back to an imprecise baseline analysis, thus preserving soundness. We show that Kaleidoscope reduces the average points-to set size by 13.15× across a set of 9 applications over the current state-of-the-art pointer analysis framework. Furthermore, we demonstrate how Kaleidoscope can implement control flow integrity (CFI) to increase the security of traditional CFI policies. Tapti Palit, Pedro Fonseca 0001 |
ASPLOS (3) | 2 |
| 2024 | Pronghorn: Effective Checkpoint Orchestration for Serverless Hot-StartsabstractServerless computing allows developers to deploy and scale stateless functions in ephemeral workers easily. As a result, serverless computing has been widely used for many applications, such as computer vision, video processing, and HTML generation. However, we find that the stateless nature of serverless computing wastes many of the important benefits modern language runtimes have to offer. A notable example is the extensive profiling and Just-in-Time (JIT) compilation effort that runtimes implement to achieve acceptable performance of popular high-level languages, such as Java, JavaScript, and Python. Unfortunately, when modern language runtimes are naively adopted in serverless computing, all of these efforts are lost upon worker eviction. Checkpoint-restore methods alleviate the problem by resuming workers from snapshots taken after initialization. However, production-grade language runtimes can take up to thousands of invocations to fully optimize a single function, thus rendering naive checkpoint-restore policies ineffective. Sumer Kohli, Shreyas Kharbanda, Rodrigo Bruno, Pedro Fonseca 0001 |
EuroSys | 5 |
| 2023 | Veil: A Protected Services Framework for Confidential Virtual MachinesabstractConfidential virtual machines (CVMs) enabled by AMD SEV provide a protected environment for sensitive computations on an untrusted cloud. Unfortunately, CVMs are typically deployed with huge and vulnerable operating system kernels, exposing the CVMs to attacks that exploit kernel vulnerabilities. Veil is a versatile CVM framework that efficiently protects critical system services like shielding sensitive programs, which cannot be entrusted to the buggy kernel. Veil leverages a new hardware primitive, virtual machine privilege levels (VMPL), to install a privileged security monitor inside the CVM. We overcome several challenges in designing Veil, including (a) creating unlimited secure domains with a limited number of VMPLs, (b) establishing resource-efficient domain switches, and (c) maintaining commodity kernel backwards-compatibility with only minor changes. Our evaluation shows that Veil incurs no discernible performance slowdown during normal CVM execution while incurring a modest overhead (2 -- 64%) when running its protected services across real-world use cases. Adil Ahmad, Botong Ou, Congyu Liu, Xiaokuan Zhang, Pedro Fonseca 0001 |
ASPLOS (4) | 5 |
| 2023 | KIT: Testing OS-Level Virtualization for Functional Interference BugsabstractContainer isolation is implemented through OS-level virtualization, such as Linux namespaces. Unfortunately, these mechanisms are extremely challenging to implement correctly and, in practice, suffer from functional interference bugs, which compromise container security. In particular, functional interference bugs allow an attacker to extract information from another container running on the same machine or impact its integrity by modifying kernel resources that are incorrectly isolated. Despite their impact, functional interference bugs in OS-level virtualization have received limited attention in part due to the challenges in detecting them. Instead of causing memory errors or crashes, many functional interference bugs involve hard-to-catch logic errors that silently produce semantically incorrect results. Congyu Liu, Sishuai Gong, Pedro Fonseca 0001 |
ASPLOS (2) | 3 |
| 2023 | An Extensible Orchestration and Protection Framework for Confidential Cloud Computing
Adil Ahmad, Alex Schultz, Byoungyoung Lee, Pedro Fonseca 0001 |
OSDI | 4 |
| 2023 | Snowcat: Efficient Kernel Concurrency Testing using a Learned Coverage PredictorabstractRandom-based approaches and heuristics are commonly used in kernel concurrency testing due to the massive scale of modern kernels and corresponding interleaving space. The lack of accurate and scalable approaches to analyze concurrent kernel executions makes existing testing approaches heavily rely on expensive dynamic executions to measure the effectiveness of a new test. Unfortunately, the high cost incurred by dynamic executions limits the breadth of the exploration and puts latency pressure on finding effective concurrent test inputs and schedules, hindering the overall testing effectiveness. Sishuai Gong, Dinglan Peng, Deniz Altinbüken, Pedro Fonseca 0001, Petros Maniatis |
SOSP | 4 |
| 2023 | μSwitch: Fast Kernel Context Isolation with Implicit Context SwitchesabstractIsolating application components is crucial to limit the exposure of sensitive data and code to vulnerabilities in the untrusted components. Process-based isolation is the de facto isolation used in practice, e.g., web browsers. However, it incurs significant performance overhead and is typically infeasible when frequent switches between isolation domains are expected. To address this problem, many intra-process memory isolation techniques have been proposed using novel kernel abstractions, recent CPU extensions (e.g., Intel®MPK), and software-based fault isolation (e.g., WebAssembly). However, these techniques insufficiently isolate kernel resources, such as file descriptors, or do so by incurring high overheads when resources are accessed. Other work virtualizes the kernel context inside a privileged user space domain, but this is ad-hoc, error-prone, and provides only limited kernel functionalities.We propose μSwitch, an efficient kernel context isolation mechanism with memory protection that addresses these limitations. We use a protected structure, shared by the kernel and the user space, for context switching and propose implicit context switching to improve its performance by deferring the kernel resource switch to the next system call. We apply μSWITCH to isolate libraries in the Firefox web browser and an HTTP server, and reduce the overhead of isolation by 32.7% to 98.4% compared with other isolation techniques. Dinglan Peng, Congyu Liu, Tapti Palit, Pedro Fonseca 0001, Anjo Vahldiek-Oberwagner, Mona Vij |
SP | 4 |
| 2021 | Kard: lightweight data race detection with per-thread memory protectionabstractFinding data race bugs in multi-threaded programs has proven challenging. A promising direction is to use dynamic detectors that monitor the program’s execution for data races. However, despite extensive work on dynamic data race detection, most proposed systems for commodity hardware incur prohibitive overheads due to expensive compiler instrumentation of memory accesses; hence, they are not efficient enough to be used in all development and testing settings. Adil Ahmad, Sangho Lee 0001, Pedro Fonseca 0001, Byoungyoung Lee |
ASPLOS | 3 |
| 2021 | On-demand-fork: a microsecond fork for memory-intensive and latency-sensitive applicationsabstractFork has long been the process creation system call for Unix. At its inception, fork was hailed as an efficient system call due to its use of copy-on-write on memory shared between parent and child processes. However, application memory demand has increased drastically since the early days and the cost incurred by fork to simply set up virtual memory (e.g., copy page tables) is now a concern, even for applications that only require hundreds of MBs of memory. In practice, fork performance already holds back system efficiency and latency across a range of uses cases that fork large processes, such as fault-tolerant systems, serverless frameworks, and testing frameworks. Kaiyang Zhao 0002, Sishuai Gong, Pedro Fonseca 0001 |
EuroSys | 3 |
| 2021 | From warm to hot starts: leveraging runtimes for the serverless eraabstractThe serverless computing model leverages high-level languages, such as JavaScript and Java, to raise the level of abstraction for cloud programming. However, today's design of serverless computing platforms based on stateless short-lived functions leads to missed opportunities for modern runtimes to optimize serverless functions through techniques such as JIT compilation and code profiling. Sumer Kohli, Rodrigo Bruno, Pedro Fonseca 0001 |
HotOS | 4 |
| 2021 | CHANCEL: Efficient Multi-client Isolation Under Adversarial Programs
Adil Ahmad, Juhee Kim, Jaebaek Seo, Insik Shin, Pedro Fonseca 0001, Byoungyoung Lee |
NDSS | 5 |
| 2021 | Execution reconstruction: harnessing failure reoccurrences for failure reproductionabstractReproducing production failures is crucial for software reliability. Alas, existing bug reproduction approaches are not suitable for production systems because they are not simultaneously efficient, effective, and accurate. In this work, we survey prior techniques and show that existing approaches over-prioritize a subset of these properties, and sacrifice the remaining ones. As a result, existing tools do not enable the plethora of proposed failure reproduction use-cases (e.g., debugging, security forensics, fuzzing) for production failures. Gefei Zuo, Jiacheng Ma 0001, Andrew Quinn 0001, Pramod Bhatotia, Pedro Fonseca 0001, Baris Kasikci |
PLDI | 5 |
| 2021 | Snowboard: Finding Kernel Concurrency Bugs through Systematic Inter-thread Communication AnalysisabstractKernel concurrency bugs are challenging to find because they depend on very specific thread interleavings and test inputs. While separately exploring kernel thread interleavings or test inputs has been closely examined, jointly exploring interleavings and test inputs has received little attention, in part due to the resulting vast search space. Using precious, limited testing resources to explore this search space and execute just the right concurrent tests in the proper order is critical. Sishuai Gong, Deniz Altinbüken, Pedro Fonseca 0001, Petros Maniatis |
SOSP | 3 |
| 2021 | SHARD: Fine-Grained Kernel Specialization with Context-Aware Hardening
Muhammad Abubakar, Adil Ahmad, Pedro Fonseca 0001, Dongyan Xu |
USENIX Security Symposium | 3 |
| 2020 | SoK: Understanding the Prevailing Security Vulnerabilities in TrustZone-assisted TEE SystemsabstractHundreds of millions of mobile devices worldwide rely on Trusted Execution Environments (TEEs) built with Arm TrustZone for the protection of security-critical applications (e.g., DRM) and operating system (OS) components (e.g., Android keystore). TEEs are often assumed to be highly secure; however, over the past years, TEEs have been successfully attacked multiple times, with highly damaging impact across various platforms. Unfortunately, these attacks have been possible by the presence of security flaws in TEE systems. In this paper, we aim to understand which types of vulnerabilities and limitations affect existing TrustZone-assisted TEE systems, what are the main challenges to build them correctly, and what contributions can be borrowed from the research community to overcome them. To this end, we present a security analysis of popular TrustZone-assisted TEE systems (targeting Cortex-A processors) developed by Qualcomm, Trustonic, Huawei, Nvidia, and Linaro. By studying publicly documented exploits and vulnerabilities as well as by reverse engineering the TEE firmware, we identified several critical vulnerabilities across existing systems which makes it legitimate to raise reasonable concerns about the security of commercial TEE implementations. David Cerdeira, Nuno Santos 0001, Pedro Fonseca 0001, Sandro Pinto 0001 |
SP | 3 |
| 2019 | Cirrus: a Serverless Framework for End-to-end ML WorkflowsabstractMachine learning (ML) workflows are extremely complex. The typical workflow consists of distinct stages of user interaction, such as preprocessing, training, and tuning, that are repeatedly executed by users but have heterogeneous computational requirements. This complexity makes it challenging for ML users to correctly provision and manage resources and, in practice, constitutes a significant burden that frequently causes over-provisioning and impairs user productivity. Serverless computing is a compelling model to address the resource management problem, in general, but there are numerous challenges to adopt it for existing ML frameworks due to significant restrictions on local resources. Pedro Fonseca 0001, Alexey Tumanov, Randy H. Katz |
SoCC | 2 |
| 2018 | MultiNyx: a multi-level abstraction framework for systematic analysis of hypervisorsabstractMultiNyx is a new framework designed to systematically analyze modern virtual machine monitors (VMMs), which rely on complex processor extensions to enhance their efficiency. To achieve better scalability, MultiNyx introduces selective, multi-level symbolic execution: it analyzes most instructions at a high semantic level, and leverages an executable specification (e.g., the Bochs CPU emulator) to analyze complex instructions at a low semantic level. MultiNyx seamlessly transitions between these different semantic levels of analysis by converting their state. Pedro Fonseca 0001, Xi Wang 0005, Arvind Krishnamurthy |
EuroSys | 1 |
| 2018 | Cntr: Lightweight OS Containers
Jörg Thalheim, Pramod Bhatotia, Pedro Fonseca 0001, Baris Kasikci |
USENIX ATC | 3 |
| 2017 | An Empirical Study on the Correctness of Formally Verified Distributed SystemsabstractRecent advances in formal verification techniques enabled the implementation of distributed systems with machine-checked proofs. While results are encouraging, the importance of distributed systems warrants a large scale evaluation of the results and verification practices. Pedro Fonseca 0001, Kaiyuan Zhang 0001, Xi Wang 0005, Arvind Krishnamurthy |
EuroSys | 1 |
| 2016 | Diamond: Automating Data Management and Storage for Wide-Area, Reactive Applications
Irene Zhang, Niel Lebeck, Pedro Fonseca 0001, Brandon Holt, Raymond Cheng 0001, Ariadna Norberg, Arvind Krishnamurthy, Henry M. Levy |
OSDI | 3 |
| 2015 | iThreads: A Threading Library for Parallel Incremental ComputationabstractIncremental computation strives for efficient successive runs of applications by re-executing only those parts of the computation that are affected by a given input change instead of recomputing everything from scratch. To realize these benefits automatically, we describe iThreads, a threading library for parallel incremental computation. iThreads supports unmodified shared-memory multithreaded programs: it can be used as a replacement for pthreads by a simple exchange of dynamically linked libraries, without even recompiling the application code. To enable such an interface, we designed algorithms and an implementation to operate at the compiled binary code level by leveraging MMU-assisted memory access tracking and process-based thread isolation. Our evaluation on a multicore platform using applications from the PARSEC and Phoenix benchmarks and two case-studies shows significant performance gains. Pramod Bhatotia, Pedro Fonseca 0001, Umut A. Acar, Björn B. Brandenburg, Rodrigo Rodrigues 0001 |
ASPLOS | 2 |
| 2014 | SKI: Exposing Kernel Concurrency Bugs through Systematic Schedule Exploration
Pedro Fonseca 0001, Rodrigo Rodrigues 0001, Björn B. Brandenburg |
OSDI | 1 |
| 2013 | Composing OS extensions safely and efficiently with BasculeabstractLibrary OS (LibOS) architectures implement the OS personality as a user-mode library, giving each application the flexibility to choose its LibOS. This approach is appealing for many reasons, not least the ability to extend or customise the LibOS. Recent work with Drawbridge [29] showed that an existing commodity OS (Windows 7) could be refactored to produce a LibOS while retaining application compatibility. Andrew Baumann, Pedro Fonseca 0001, Lisa Glendenning, Jacob R. Lorch, Barry Bond, Reuben Olinsky, Galen C. Hunt |
EuroSys | 3 |
| 2011 | Finding complex concurrency bugs in large multi-threaded applicationsabstractParallel software is increasingly necessary to take advantage of multi-core architectures, but it is also prone to concurrency bugs which are particularly hard to avoid, find, and fix, since their occurrence depends on specific thread interleavings. In this paper we propose a concurrency bug detector that automatically identifies when an execution of a program triggers a concurrency bug. Unlike previous concurrency bug detectors, we are able to find two particularly hard classes of bugs. The first are bugs that manifest themselves by subtle violation of application semantics, such as returning an incorrect result. The second are latent bugs, which silently corrupt internal data structures, and are especially hard to detect because when these bugs are triggered they do not become immediately visible. Pike detects these concurrency bugs by checking both the output and the internal state of the application for linearizability at the level of user requests. This paper presents this technique for finding concurrency bugs, its application in the context of a testing tool that systematically searches for such problems, and our experience in applying our approach to MySQL, a large-scale complex multi-threaded application. We were able to find several concurrency bugs in a stable version of the application, including subtle violations of application semantics, latent bugs, and incorrect error replies. Pedro Fonseca 0001, Cheng Li 0001, Rodrigo Rodrigues 0001 |
EuroSys | 1 |
| 2010 | A study of the internal and external effects of concurrency bugsabstractConcurrent programming is increasingly important for achieving performance gains in the multi-core era, but it is also a difficult and error-prone task. Concurrency bugs are particularly difficult to avoid and diagnose, and therefore in order to improve methods for handling such bugs, we need a better understanding of their characteristics. In this paper we present a study of concurrency bugs in MySQL, a widely used database server. While previous studies of real-world concurrency bugs exist, they have centered their attention on the causes of these bugs. In this paper we provide a complementary focus on their effects, which is important for understanding how to detect or tolerate such bugs at run-time. Our study uncovered several interesting facts, such as the existence of a significant number of latent concurrency bugs, which silently corrupt data structures and are exposed to the user potentially much later. We also highlight several implications of our findings for the design of reliable concurrent systems. Pedro Fonseca 0001, Cheng Li 0001, Vishal Singhal, Rodrigo Rodrigues 0001 |
DSN | 1 |
| 2009 | Zeno: Eventually Consistent Byzantine-Fault Tolerance
Atul Singh, Pedro Fonseca 0001, Petr Kuznetsov, Rodrigo Rodrigues 0001, Petros Maniatis |
NSDI | 2 |
| 2009 | Full-Information Lookups for Peer-to-Peer OverlaysabstractMost peer-to-peer lookup schemes keep a small amount of routing state per node, typically logarithmic in the number of overlay nodes. This design assumes that routing information at each member node must be kept small so that the bookkeeping required to respond to system membership changes is also small, given that aggressive membership dynamics are expected. As a consequence, lookups have high latency as each lookup requires contacting several nodes in sequence. In this paper, we question these assumptions by presenting a peer-to-peer routing algorithm with small lookup paths. Our algorithm, called ldquoOneHop,rdquo maintains full information about the system membership at each node, routing in a single hop whenever that information is up to date and in a small number of hops otherwise. We show how to disseminate information about membership changes quickly enough so that nodes maintain accurate complete membership information. We also present analytic bandwidth requirements for our scheme that demonstrate that it could be deployed in systems with hundreds of thousands of nodes and high churn. We validate our analytic model using a simulated environment and a real implementation. Our results confirm that OneHop is able to achieve high efficiency, usually reaching the correct node directly 99 percent of the time. Pedro Fonseca 0001, Rodrigo Rodrigues 0001, Barbara Liskov |
IEEE Trans. Parallel Distributed Syst. | 1 |