Skip to main content
zenodoopen

Benchmarks for Comparing Binary-Level Symbolic Execution Speed

<p>This dataset contains a reproducible computing environment as well as a set of synthetic benchmark applications for comparing symbolic execution speed at the binary level of several symbolic execution engines supporting the 32-bit RISC-V architecture. Specifically, the dataset compares and supports the following engines:</p> <ul> <li><a href="https://github.com/binsec/binsec">BinSec</a></li> <li><a href="https://github.com/angr/angr">angr</a></li> <li><a href="https://github.com/agra-uni-bremen/symex-vp">SymEx-VP</a></li> <li><a href="https://github.com/agra-uni-bremen/binsym">BinSym</a></li> </ul> <p>The benchmarks are designed to be easily extendable through the utilization of <a href="https://guix.gnu.org">Guix</a> (a functional package manager for <a href="https://doi.org/10.1038/s41597-022-01720-9">long-term reproducible research</a>). Currently, the supported engines perform IR-based symbolic execution using binary lifting (BinSec &amp; angr) and direct symbolic execution of RISC-V machine code (SymEx-VP &amp; BinSym). The dataset compares these approaches by fully exploring synthetic benchmark applications (e.g. sorting algorithms) with unconstrained symbolic input values and calculating an arithmetic mean over multiple executions, which is then represented as a table and a plot.</p> <p>More information on using the dataset is available in the supplementary README file.</p>

ShareScore

32/100

Overall dataset sharing score

Score breakdown

These five areas show where the dataset supports — or may limit — practical reuse.

Stewardship
4
Harmonization
4
Access
16
Reuse readiness
8
Engagement
0

Dataset details

Repository
zenodo
Published
April 3, 2024
License
mit-license
DOI
10.5281/zenodo.10925791

Scored with release 0.9.0

ScienceDex for faculty

Your academic CV and NIH biosketch

Make your CV in your school's format and your NIH biosketch from it, then download both as Word files.