Recherche

Afficher tous les résultats pour

Accueil

Personne

George Candea

Cette personne a quitté l’EPFL

À propos
Confidentialité
Mentions légales

Graph Chatbot

Publications associées (67)

Page 2 sur 4

Practical Verification of System-Software Components Written in Standard C

Yonghao Zou, George Candea, Clément Pit-Claudel, Diyu Zhou, Can Cebeci

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

Deadlock Immunity: Enabling Systems To Defend Against Deadlocks

George Candea, Cristian Zamfir, Horatiu Jula

Deadlock immunity is a property by which programs, once afflicted by a given deadlock, develop resistance against future occurrences of that and similar deadlocks. We describe a technique that enables programs to automatically gain such immunity without as ...

2008

A Scalable, Predictable Join Operator for Highly Concurrent Data Warehouses

George Candea

Conventional data warehouses employ the query-at-a-time model, which maps each query to a distinct physical plan. When several queries execute concurrently, this model introduces contention, because the physical plans—unaware of each other—compete for acce ...

2009

Prototyping Symbolic Execution Engines for Interpreted Languages

George Candea, Johannes Kinder, Stefan Bucur

Symbolic execution is being successfully used to automatically test statically compiled code. However, increasingly more systems and applications are written in dynamic interpreted languages like Python. Building a new symbolic execution engine is a monume ...

ACM2014

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

George Candea, Vitaly Chipounov

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

The Case for Performance Interfaces for Hardware Accelerators

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

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

Drivolution: Rethinking the Database Driver Lifecycle

George Candea, Emmanuel Cecchet

The current design of database drivers – a necessary evil for interacting with a DBMS – imposes undue burdens on those who install, upgrade, and manage database systems and their applications. In this paper, we introduce Drivolution, a new architecture for ...

2009

Lightweight Snapshots and System-level Backtracking

George Candea, Edouard Bugnion, Vitaly Chipounov

We propose a new system-level abstraction, the lightweight immutable execution snapshot, which combines the immutable characteristics of checkpoints with the direct integration into the virtual memory subsystem of standard mutable address spaces. The abstr ...

USENIX2013

iProve: A Scalable Approach to Consumer-Verifiable Software Guarantees

George Candea, Horatiu Jula, Silviu Andrica

Formally proving complex program properties is still considered impractical for systems with over a million lines of code (MLOC). We present iProve, an approach that enables the generation and verification of proofs for interesting program properties in la ...

Ieee Service Center, 445 Hoes Lane, Po Box 1331, Piscataway, Nj 08855-1331 Usa2010

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

Reverse-Engineering Drivers for Safety and Portability

George Candea, Vitaly Chipounov

Device drivers today lack two important properties: guaranteed safety and cross-platform portability. We present an approach to incrementally achieving these properties in drivers, without requiring any changes in the drivers or operating system kernels. W ...

2008

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

LFI: A Practical and General Library-Level Fault Injector

George Candea

Fault injection, a critical aspect of testing robust systems, is often overlooked in the development of general-purpose software. We believe this is due to the absence of easy-to-use tools and to the extensive manual labor required to perform fault injecti ...

2009

Enabling Sophisticated Analysis of x86 Binaries with RevGen

George Candea, Vitaly Chipounov

Current state-of-the-art static analysis tools for binary software operate on ad-hoc intermediate representations (IR) of the machine code. Therefore, even though IRs facilitate program analysis by abstracting away the source language, it is hard to reuse ...

2011

Reverse Engineering of Binary Device Drivers with RevNIC

George Candea, Vitaly Chipounov

This paper presents a technique that helps automate the reverse engineering of device drivers. It takes a closed-source binary driver, automatically reverse engineers the driver’s logic, and synthesizes new device driver code that implements the exact same ...

2010

Finding Trojan Message Vulnerabilities in Distributed Systems

Rachid Guerraoui, George Candea, Radu Banabic

Trojan messages are messages that seem correct to the receiver but cannot be generated by any correct sender. Such messages constitute major vulnerability points of a distributed system---they constitute ideal targets for a malicious actor and facilitate f ...

ACM2014

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

Achieving Microsecond-Scale Tail Latency Efficiently with Approximate Optimal Scheduling

George Candea, Rishabh Ramesh Iyer, Musa Sadik Ünal

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

Advantageous State Merging During Symbolic Analysis

George Candea, Johannes Kinder, Volodymyr Kuznetsov, Stefan Bucur

A determination is made regarding whether to merge two symbolic analysis states. A first state corresponds to a first path through a program to a program location and a second state corresponds to a second path through the program to the program location. ...

2013

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