# Breaking Kryptonite's obfuscation: a static analysis approach relying on symbolic execution

DevFeed: [Breaking Kryptonite's obfuscation: a static analysis approach relying on symbolic execution](<https://devfeed.tech/articles/breaking-kryptonite-s-obfuscation-a-static-analysis-approach-relying-on-symbolic-execution-39691.md>)

Original publisher: [Read original article](<https://doar-e.github.io/blog/2013/09/16/breaking-kryptonites-obfuscation-with-symbolic-execution/>)

Author: Axel "0vercl0k" Souchet

Published: 2013-09-16T18:47:00Z

Content type: tutorial

Language: en

Sources: [Diary of a reverse-engineer](<https://devfeed.tech/sources/diary-of-a-reverse-engineer.md>)

Topics: [obfuscation](<https://devfeed.tech/topics/obfuscation.md>), [execution](<https://devfeed.tech/topics/execution.md>), [LLVM](<https://devfeed.tech/topics/llvm.md>), [clang](<https://devfeed.tech/topics/clang.md>), [Assembly](<https://devfeed.tech/topics/assembly.md>), [x86](<https://devfeed.tech/topics/x86.md>), [Code](<https://devfeed.tech/topics/code.md>)

Tags: [analysis](<https://devfeed.tech/tags/analysis.md>), [asm](<https://devfeed.tech/tags/asm.md>), [assembly](<https://devfeed.tech/tags/assembly.md>), [clang](<https://devfeed.tech/tags/clang.md>), [code](<https://devfeed.tech/tags/code.md>), [llvm](<https://devfeed.tech/tags/llvm.md>), [obfuscation](<https://devfeed.tech/tags/obfuscation.md>), [reverse-engineering](<https://devfeed.tech/tags/reverse-engineering.md>), [static](<https://devfeed.tech/tags/static.md>), [symbolic-execution](<https://devfeed.tech/tags/symbolic-execution.md>), [x86](<https://devfeed.tech/tags/x86.md>)

## AI overview

This tutorial demonstrates how symbolic execution can break Kryptonite, a proof-of-concept obfuscator that applies semantics-preserving transformations at the LLVM intermediate representation level. It describes a small symbolic execution engine built with IDAPy and Z3Py, using an x86 binary generated from LLVM code for a 32-bit adder.

## Source excerpt

Introduction Kryptonite was a proof-of-concept I built to obfuscate codes at the LLVM intermediate representation level. The idea was to use semantic-preserving transformations in order to not break the original program. One of the main idea was for example to build a home-made 32 bits adder to replace the add ...