Awesome

hardbound-vp

SystemC-based Virtual Prototype with symbolic execution support and HardBound path analyzer.

About

This is a fork of symex-vp which provides a HardBound-based path analyzer for finding spatial memory safety violations in low-level code for constrained devices using symbolic execution. The implementation is further described in the 2022 ASP-DAC publication Automated Detection of Spatial Memory Safety Violations for Constrained Devices.

Installation

Refer to the original symex-vp cloning and installation instructions. Software which should be checked for spatial memory safety violations must be compiled with hardbound-llvm.

Acknowledgements

This work was supported in part by the German Federal Ministry of Education and Research (BMBF) within the project Scale4Edge under contract no. 16ME0127 and within the project VerSys under contract no. 01IW19001.

License

The original riscv-vp code is licensed under MIT (see LICENSE.MIT). All modifications made for the integration of symbolic execution with riscv-vp are licensed under GPLv3+ (see LICENSE.GPL). Consult the copyright headers of individual files for more information.