Publications by George Candea | EPFL Graph Search

The Case for Energy Clarity

The rapid expansion of cloud computing, especially machine learning, is leading to a significant increase in the global energy footprint of computing. Improvements in the energy efficiency of hardware and infrastructure are nearing the point of diminishing ...

ACM2025

A Conjecture Regarding SMT Instability

George Candea, Clément Pit-Claudel

Automated verifiers rely on SMT solvers as a backend for proof automation. This simplifies verification in the common case, but also creates usability challenges due to instability. Previous work proposes mitigation strategies motivated by the assumption t ...

Wiley2025

Practical Verification of System-Software Components Written in Standard C

George Candea, Clément Pit-Claudel

Systems code is challenging to verify, because it uses constructs (like raw pointers, pointer arithmetic, and bit twiddling) that are hard for tools to reason about. Existing approaches either sacrifice programmer friendliness, by demanding significant man ...

Association for Computing Machinery, Inc2024

Automatically Reasoning About How Systems Code Uses the CPU Cache

George Candea, Aikaterini Argyraki, Rishabh Ramesh Iyer

We present a technique, called CFAR, that developers can use to reason precisely about how their code, as well as third-party code, uses the CPU cache. Given a piece of systems code P, CFAR employs program analysis and binary instrumentation to automatical ...

2024

Transparent Multicore Scaling of Single-threaded Network Functions

George Candea, Sanidhya Kashyap

This paper presents NFOS, a programming model, runtime, and profiler for productively developing software network functions (NFs) that scale on multicore machines. Writing shared-state concurrent systems that are both correct and scalable is still a seriou ...

Assoc Computing Machinery2024

The Case for Performance Interfaces for Hardware Accelerators

George Candea, Aikaterini Argyraki, Rishabh Ramesh Iyer, Jiacheng Ma

While systems designers are increasingly turning to hardware accelerators for performance gains, realizing these gains is painstaking and error-prone. It can take several person-months to determine if a given accelerator is a good fit for a given piece of ...

2023

Achieving Microsecond-Scale Tail Latency Efficiently with Approximate Optimal Scheduling

George Candea, Rishabh Ramesh Iyer

Datacenter applications expect microsecond-scale service times and tightly bound tail latency, with future workloads expected to be even more demanding. To address this challenge, state-of-the-art runtimes employ theoretically optimal scheduling policies, ...

Assoc Computing Machinery2023

Performance Interfaces for Network Functions

George Candea, Aikaterini Argyraki, Rishabh Ramesh Iyer

Modern programmers routinely use third-party code, and infrastructure operators deploy software they did not write. This would not be possible without semantic interfaces---documentation, header files, specifications---that succinctly describe what that th ...

USENIX Association2022

Automated Verification of Network Function Binaries

George Candea, Aikaterini Argyraki, Solal Vincenzo Pirelli

Formally verifying the correctness of software network functions (NFs) is necessary for network reliability, yet existing techniques require full source code and mandate the use of specific data structures. We describe an automated technique to verify NF b ...

USENIX Association2022

A Simpler and Faster NIC Driver Model for Network Functions

George Candea, Solal Vincenzo Pirelli

The advent of software network functions calls for stronger correctness guarantees and higher performance at every level of the stack. Current network stacks trade simplicity for performance and flexibility, especially in their driver model. We show that p ...

2021

Verifying Software Network Functions with No Verification Expertise

George Candea, Aikaterini Argyraki, Solal Vincenzo Pirelli, Rishabh Ramesh Iyer, Luis David Figueiredo Mascarenhas Moreira Pedrosa, Matteo Rizzo

We present the design and implementation of Vigor, a software stack and toolchain for building and running software network middleboxes that are guaranteed to be correct, while preserving competitive performance and developer productivity. Developers write ...

ACM2019

Performance Contracts for Software Network Functions

George Candea, Aikaterini Argyraki, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh, Rishabh Ramesh Iyer, Luis David Figueiredo Mascarenhas Moreira Pedrosa

Software network functions (NFs), or middleboxes, promise flexibility and easy deployment of network services but face the serious challenge of unexpected performance behaviour. We propose the notion of a performance contract, a construct formulated in ter ...

USENIX ASSOC2019

A Formally Verified NAT Stack

George Candea, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh

Prior work proved a stateful NAT network function to be semantically correct, crash-free, and memory safe. Their toolchain verifies the network function code while assuming the underlying kernel-bypass framework, drivers, operating system, and hardware to ...

2018

Discover deeper bugs with dynamic symbolic execution and coverage-based fuzz testing

Vitaly Chipounov, George Candea, Bin Zhang, Chao Feng

Coverage-based fuzz testing and dynamic symbolic execution are both popular program testing techniques. However, on their own, both techniques suffer from scalability problems when considering the complexity of modern software. Hybrid testing methods attem ...

INST ENGINEERING TECHNOLOGY-IET2018

A Formally Verified NAT Stack

George Candea, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh

Prior work proved a stateful NAT network function to be, crash-free, memory safe and semantically correct [29]. Their toolchain verifies the network function code while assuming the underlying kernel-bypass framework, drivers, operating system, and hardwar ...

ASSOC COMPUTING MACHINERY2018

A Formally Verified NAT

George Candea, Aikaterini Argyraki, Solal Vincenzo Pirelli, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Assoc Computing Machinery2017

Automatic generation of program execution that reaches a given failure point

George Candea, Cristian Zamfir

An execution of a target software program that causes a particular bug to manifest itself is generated. A target software program is received. A bug report generated by an execution of the target software program is received. The bug report describes a par ...

2015

Automated Classification of Data Races Under Both Strong and Weak Memory Models

George Candea, Cristian Zamfir, Baris Can Cengiz Kasikci

Data races are one of the main causes of concurrency problems in multithreaded programs. Whether all data races are bad, or some are harmful and others are harmless, is still the subject of vigorous scientific debate [Narayanasamy et al. 2007; Boehm 2012]. ...

Assoc Computing Machinery2015

High System-Code Security with Low Overhead

Jonas Benedict Wagner, George Candea, Volodymyr Kuznetsov, Johannes Kinder

Security vulnerabilities plague modern systems because writing secure systems code is hard. Promising approaches can retrofit security automatically via runtime checks that implement the desired security policy; these checks guard critical operations, like ...

2015

Failure Sketching: A Technique for Automated Root Cause Diagnosis of In-Production Failures

George Candea, Baris Can Cengiz Kasikci, Benjamin Charles Schubert

2015