Binary symbolic execution with KLEE-Native

Published

2019-08-30 10:50

Collected

2026-07-03 04:21

---
id: 1926
title: "Binary symbolic execution with KLEE-Native"
source_domain: blog.trailofbits.com
source_url: "https://blog.trailofbits.com/2019/08/30/binary-symbolic-execution-with-klee-native/"
published_at: "2019-08-30T10:50:08Z"
tags: ["reverse-engineering", "binary-analysis", "llvm", "program-analysis", "symbolic-execution", "klee", "paravirtualization"]
phying_url: "https://phying.com/item/1926"
lang: en
---

# Binary symbolic execution with KLEE-Native

## Summary

KLEE-Native extends the KLEE symbolic executor to binary program snapshots by dynamically lifting machine code to LLVM bitcode, enabling symbolic execution without source using paravirtualization.

## Intelligence Metadata

- **Sources:** blog.trailofbits.com
- **Published:** 2019-08-30T10:50:08Z
- **Original:** https://blog.trailofbits.com/2019/08/30/binary-symbolic-execution-with-klee-native/
- **Phying News:** https://phying.com/item/1926