Symbolic execution

Résumé

In computer science, symbolic execution (also symbolic evaluation or symbex) is a means of analyzing a program to determine what inputs cause each part of a program to execute. An interpreter follows the program, assuming symbolic values for inputs rather than obtaining actual inputs as normal execution of the program would. It thus arrives at expressions in terms of those symbols for expressions and variables in the program, and constraints in terms of those symbols for the possible outcomes of each conditional branch. Finally, the possible inputs that trigger a branch can be determined by solving the constraints. The field of symbolic simulation applies the same concept to hardware. Symbolic computation applies the concept to the analysis of mathematical expressions. Example Consider the program below, which reads in a value and fails if the input is 6. int f() { ... y = read(); z = y * 2; if (z == 12) { fail(); } else { printf("OK"); } } During

Source officielle

https://en.wikipedia.org/wiki/Symbolic_execution

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Publications associées (16)

Publications associées

Chargement

Personnes associées (5)

Personnes associées

Chargement

Unités associées (5)

Unités associées

Chargement

Concepts associés

Chargement

Cours associés (2)

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to use formal verification tools and explain the theory and the practice behind them.

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language into the new web standard for portable binaries called WebAssembly ( https://webassembly.org/ )

Cours associés

Chargement

Séances de cours associées (4)

Séances de cours associées

Chargement

-Overify: Optimizing Programs for Fast Verification

George Candea, Volodymyr Kuznetsov, Jonas Benedict Wagner

Developers rely on automated testing and verification tools to gain confidence in their software. The input to such tools is often generated by compilers that have been designed to generate code that runs fast, not code that can be verified easily and quickly. This makes the verification tool's task unnecessarily hard. We propose that compilers support a new kind of switch, -Overify, that generates code optimized for the needs of verification tools. We implemented this idea for one class of verification (symbolic execution) and found that, when run on the Coreutils suite of UNIX utilities, it reduces verification time by up to 95x.

2013

Chargement

A Formally Verified NAT

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

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 network functions and proves properties specific to network configuration, such as reachability and absence of loops. Our proof applies directly to the C code of a network function, and it demonstrates the absence of implementation bugs. Prior work argued that this is not feasible (i.e., that verifying a real, stateful network function written in C does not scale) but we demonstrate otherwise: NAT is one of the most popular network functions and maintains per-flow state that needs to be properly updated and expired, which is a typical source of verification challenges. We tackle the scalability challenge with a new combination of symbolic execution and proof checking using separation logic; this combination matches well the typical structure of a network function. We then demonstrate that formally proven correctness in this case does not come at the cost of performance. The NAT code, proof toolchain, and proofs are available at https://vignat.github.io/

Assoc Computing Machinery2017

Chargement

Performance Contracts for Software Network Functions

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

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 terms of performance critical variables, that provides a precise description of NF performance. Performance contracts enable fine-grained prediction and scrutiny of NF performance for arbitrary workloads, without having to run the NF itself. We describe BOLT, a technique and tool for computing such performance contracts for the entire software stack of NFs written in C, including the core NF logic, DPDK packet processing framework, and NIC driver. BOLT takes as input the NF implementation code and outputs the corresponding contract. Under the covers, it combines pre-analysis of a library of stateful NF data structures with automated symbolic execution of the NF’s code. We evaluate BOLT on four NFs—a Maglev-like load balancer, a NAT, an LPM router, and a MAC bridge—and show that its performance contracts predict the dynamic instruction count and memory access count with a maximum gap of 7% between the real execution and the conservatively predicted upper bound. With further engineering, this gap can be reduced.

USENIX ASSOC2019

Chargement