Pith. sign in

REVIEW 2 major objections 5 minor 1 cited by

How to Kill Symbolic Deobfuscation for Free; or Unleashing the Potential of Path-Oriented Protections

T0 review · 2 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Path-oriented protections that fork on single-valued input variables can make dynamic symbolic execution time out on every tested program while keeping runtime overhead at or below 1.3x.

desk verdict A cheap, well-analyzed anti-DSE protection that works on current tools—but the 'defeats all DSE' claim needs scoping to engines without loop summarization. read the letter →

arxiv 1908.01549 v2 pith:DLYEHKAI submitted 2019-08-05 cs.CR

Mathilde Ollivier , Sébastien Bardin , Richard Bonichon , Jean-Yves Marion This is my paper · ORCID
classification cs.CR
keywords codeobfuscationdynamicsymbolicexecutionpath-orientedprotectionsinglevaluepathexplosiondeobfuscationforkingpointanti-DSE
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper proposes that the most effective way to defeat Dynamic Symbolic Execution (DSE) is not to make constraints harder to solve, but to make path exploration explode. It formalizes path-oriented protections as forking points inserted into code, and introduces the single value path (SVP) property: a forking point where a variable can take exactly one value per created path. Its main scheme, For, replaces input-dependent assignments with byte-sized loops, so each loop forces up to $2^8$ paths and chaining $k$ loops multiplies paths by $2^{8k}$ while adding only linear overhead. In experiments, five chained SVP loops made all tested DSE tools time out on every benchmark program for both path exploration and secret finding, with runtime overhead at or below 1.3x. The authors claim this makes symbolic deobfuscation intractable in practice at essentially no cost.

What carries the argument

The central object is the forking point $F(a,x,\gamma)$: a code location at address $a$ that branches on variable $x$ and creates up to $\gamma$ new paths. A forking point is Single Value Path (SVP) when $x$ takes exactly one value along each path the protection creates. The SVP mechanism is implemented by the For scheme, a loop whose iteration count is bounded by one input byte, and by the self-modifying Write scheme; chaining $k$ independent SVP forking points gives the exponential path multiplication of Theorem 1. A second load-bearing component is the anchorage policy: forking points must be placed so that every original path hits at least $k$ of them, and so that the forked variables are independent. A third component is resistance by design: if every variable of the forking point is relevant (has Def-Use chains from an input and to an output), then sound taint and slicing analyses cannot simplify it.

What would settle it

Equip a dynamic symbolic execution engine with a loop-summarization or generalized path-merging step, run it on the paper's $k=5$ protected programs from the first dataset, and check whether it reaches full path coverage or finds the secret within the stated timeouts (3 hours for coverage, 1 hour for secret finding); if it succeeds, the paper's blanket timeout claim is refuted.

Watch

Extended reading notes

Core claim

The central discovery is that a forking point with the single value path property transforms DSE's path-exploration weakness into a controlled combinatorial explosion. Concretely, if a loop's trip count is governed by one input byte, a DSE engine that cannot summarize the loop must explore up to $2^8$ distinct paths for that single point; forking on each of the bytes of an input independently gives up to $2^{8k}$ paths, and the paper proves (Theorem 1) that when every original path passes through at least $k$ independent SVP forking points the total number of paths is at least $\#\Pi_P \cdot \theta^k$, with $\theta$ the minimum number of paths each forking point inserts. With $k=5$ this took every DSE engine tested beyond its timeout on both attacker goals, while the longest execution trace grows only by $5\cdot 2^8$ steps. The paper's claim is therefore not that DSE is impossible in principle, but that this particular mechanism forces any non-summarizing DSE to behave as brute force.

Load-bearing premise

The protection only works if a DSE engine cannot summarize or merge a byte-controlled loop, so that each of the loop's up to 256 possible trip counts must be explored as a separate path.

Editorial extensions

If this is right

  • Programs protected with $k=5$ SVP loops become unexplorable by current DSE engines on the tested benchmarks: every program timed out for both full path coverage and secret finding.
  • Defender cost stays small: runtime overhead at most $\times 1.3$ and code size increase $\times 1.0$ to $\times 1.1$, in contrast with nested virtualization which costs up to $\times 1600$ or more.
  • Non-SVP protections such as Split can delay path exploration but remain weak at secret finding; SVP is the property that makes a protection uniformly strong against both attacker goals.
  • Increasing protection strength by raising $k$ is cheap: overhead stays below 5% for up to about 250 loops, so defenders can scale the protection far beyond the tested $k=5$.
  • If DSE engines acquire loop summarization or generalized path merging, the exponential explosion could be compressed; the paper identifies this as an open problem.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Beyond the paper's DSE focus, the SVP mechanism should transfer to any path-unrolling analysis, including bounded model checking and trace-partitioning abstract interpretation, because those methods also pay per path.
  • Beyond the paper, the byte-loop pattern is a template: any input-dependent function with exactly one output per input value can serve as an SVP forking point, so the design space for new schemes is large.
  • An untested extension suggested by the paper's P2 variant is to pair For with opaque predicates or MBA arithmetic specifically to defeat pattern-matching optimizers; a pattern-diversity benchmark could measure how far this goes.
  • A further prediction not developed in the paper is that memory, not solver time, becomes the limiting resource as $k$ grows, since path count scales as $2^{8k}$; this could be tested by monitoring memory exhaustion in a DSE run before timeout.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper proposes a class of anti-DSE obfuscations called path-oriented protections, which inflate the number of feasible paths that a Dynamic Symbolic Execution (DSE) engine must explore. The authors introduce a formal framework with the Single Value Path (SVP) criterion, present two new schemes (For and Write), prove composition and resistance-by-design theorems, and experimentally evaluate the schemes against KLEE, Binsec, and Triton on 53 programs across two attack scenarios (full path coverage and secret finding). The headline empirical result is that For with five forking points per path causes all tested engines to time out on every benchmark, while runtime overhead stays at or below a factor of about 1.3.

Significance. If the claims are accepted with appropriate scoping, this is a useful contribution: it identifies path exploration rather than constraint solving as the weak spot of DSE, provides a clean criterion (SVP) that separates weak from strong protections, introduces a cheap and simple protection whose effectiveness is confirmed by several independent engines, and includes an honest discussion of limits in Section 10.3. The two theorems are simple and correct under their stated assumptions, and the experimental protocol is substantially more careful than most papers in this area, including multiple tools, binary- and source-level settings, and robustness tests against slicing, tainting, and compilers. The main weakness is that the strongest claims are phrased universally ('discard all DSE attacks') even though the evidence and the authors' own discussion scope them to current DSE engines without loop summarization.

major comments (2)
  1. [§8.3, Table 3; §10.3] The headline claim that For(k=5) 'discard[s] all DSE attacks on our benchmarks' is not established against DSE engines equipped with even lightweight loop summarization. Section 10.3 explicitly concedes that advanced loop semantics for under-approximation methods such as DSE is 'still largely open' and that path merging 'lacks a generalization step allowing to completely capture loop semantics.' For the concrete For encoding, each byte-level loop is semantically equivalent to a simple affine relation between the input byte and the accumulated value, so an engine that recognizes this family of loops could collapse the 2^(8k) spurious paths into one or a few paths. The abstract and conclusion phrase the result as a general property of the construction rather than a property of current engines; the authors should either scope the claim explicitly ('all tested DSE engines') or prove a statement under a formal model of DSE that excludes loop summarization.
  2. [§8.2, Dataset #1] The experimental protocol excludes 2 of the 48 Banescu et al. programs because full coverage took 'considerably longer' than the others, and the 1-byte input programs are rewritten to 8-byte inputs by adding fresh bytes unused by the original program. The exclusion removes exactly the harder cases for the attacker and therefore supports the 'all benchmarks' conclusion, while the rewriting changes the input space that the protections draw on. Please report results for the excluded programs (even if only qualitatively) and make explicit how the rewritten 8-byte inputs affect the secret-finding scenario, where the added bytes are initially dead and only the protections make them relevant.
minor comments (5)
  1. [Throughout] There are numerous typos and grammatical slips, e.g., 'More informaion' (Sec. 5), 'showned' (Appendix A), 'resitance' (Sec. 6.2), 'exemple' (Appendix A), and 'Fore more readable' (Sec. 8.3). The paper would benefit from a careful proofreading pass.
  2. [§8.3, Table 3] The main-body results are reported as binary timeout counts rather than measured times; the appendix does give slowdown ranges, but the body should at least include the average slowdown for the non-timeout cases so that the reader can calibrate how close those cases are to the timeout threshold.
  3. [§8.4, Table 4] The runtime overhead is reported as an average over all programs; the REC variant of For shows roughly a 3x slowdown (vs. 1.3x for the plain variant), which is inconsistent with the 'for free' phrasing in the title. The paper should state that the low-overhead claim applies to the canonical For, not to all variants, and ideally report the range of overhead values across programs.
  4. [§7.2, Table 2] The stealth column uses '∼' for Write without definition; please explain this notation in the table caption or text.
  5. [§5, For] The text says a byte-level For 'generates up to 2^8 additional paths' with 'additional path length of 2^8'. It would be clearer to say 'up to 2^8 paths' and 'at most 256 loop iterations per forking point', since the word 'additional' is ambiguous in both places.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the SVP/strength link is an independent analytical claim, and the central results are empirical, measured against external DSE tools.

full rationale

The paper's central claim is that SVP path-oriented protections (For) cause DSE path explosion. The SVP definition (Def. 5) is stated in terms of a variable having a single possible value along each created path, not in terms of DSE timeout; the connection to DSE cost is argued through path-counting (Sec. 6.1, Thm. 1) and then tested empirically with the external tools KLEE, Triton and Binsec (Sec. 8.3). No fitted parameter is relabeled as a prediction: k is an input parameter, and the timeouts are measured. The framework's qualitative prediction that SVP schemes outperform non-SVP Split is confirmed on independent datasets rather than being built into the definition. Citations to the authors' own prior work (BINSEC [24], backward-bounded DSE [8], Salwan et al. [35]) appear only as tooling or related work and do not carry the load of the anti-DSE claim. Section 10.3 explicitly concedes that loop summarization by DSE is an open problem; that is a generality/robustness limitation of the universal phrasing, not a circular derivation. There is therefore no equation or definitional reduction that makes the result equivalent to its inputs.

Assumptions & free parameters 3 free parameters · 4 assumptions · 0 invented entities

The central claim rests on an attacker model where DSE lacks loop summarization, on the multiplicative independence of forking points, and on hand-chosen parameters k and byte-size. No hidden fitted constants are used; the prediction that For times out at k=5 is a direct experimental outcome, not a fitted value.

free parameters (3)
  • k (number of forking points per path) = 5 for the headline result; experiments also use 1, 2, 3, 4, 10, 13, 17, 50
    Protection-strength knob chosen by hand; the claim that For k=5 makes all benchmarks time out depends on this value.
  • Byte-size restriction for For loops = 8 bits
    For on 32 or 64-bit variables is intractable, as shown by WORD giving x2.6e3 overhead in Table 4, so the scheme is restricted to one-byte variables, an ad hoc design choice that bounds both path count and overhead.
  • Replacement input width for 1-byte programs = 8 bytes
    Dataset #1 programs with 1-byte input were automatically converted to 8-byte inputs with unused extra bytes in Sec 8.2 to make them non-trivial, a data modification that affects the measured timeouts.
assumptions (4)
  • domain assumption An all-powerful symbolic adversary runs a correct but incomplete DSE engine that enumerates paths by solving path constraints.
    Stated in Sec 2.1; the entire threat model and the strength definition assume DSE cannot skip feasible paths or summarize loops.
  • domain assumption SVP forking points create one new path per possible value of their variable.
    Definition 5 in Sec 4.3; used to argue For creates up to 2^8 paths per byte-level loop.
  • domain assumption Forking points based on independent variables compose multiplicatively.
    Definition 6 and Theorem 1 in Sec 6.1; assumes placement can route every original path through k independent forking points via CFG and dataflow analysis, which is described but not implemented or evaluated.
  • domain assumption Sound taint and slice analyses mark all relevant variables.
    Theorem 2 in Sec 6.2; underlies the resistance-by-design claim, assuming the analyses are sound and the variables in the forking point are relevant.

how reviews work

0 comments
Cite this review

Pith. "Pith review of How to Kill Symbolic Deobfuscation for Free; or Unleashing the Potential of Path-Oriented Protections." pith.science (2026). https://pith.science/paper/DLYEHKAI

@misc{pith2026190801549,
  author       = {Pith},
  title        = {Pith review of: How to Kill Symbolic Deobfuscation for Free; or Unleashing the Potential of Path-Oriented Protections},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/DLYEHKAI}},
  note         = {Machine review of arXiv:1908.01549}
}
read the original abstract

Code obfuscation is a major tool for protecting software intellectual property from attacks such as reverse engineering or code tampering. Yet, recently proposed (automated) attacks based on Dynamic Symbolic Execution (DSE) shows very promising results, hence threatening software integrity. Current defenses are not fully satisfactory, being either not efficient against symbolic reasoning, or affecting runtime performance too much, or being too easy to spot. We present and study a new class of anti-DSE protections coined as path-oriented protections targeting the weakest spot of DSE, namely path exploration. We propose a lightweight, efficient, resistant and analytically proved class of obfuscation algorithms designed to hinder DSE-based attacks. Extensive evaluation demonstrates that these approaches critically counter symbolic deobfuscation while yielding only a very slight overhead.

Figures

Figures reproduced from arXiv: 1908.01549 by the authors.

Figure 1
Figure 1. Manticore crackme code structure binary code) to both find a winning input and explore all paths. Standard protections. Let us now protect the pro￾gram with standard obfuscations to measure their impact on symbolic deobfuscation. We will rely on Tigress [21], a widely used tool for systematic eval￾uation of deobfuscation methods [5, 8, 35], to apply (nested) virtualization, a most effective obfuscation [5]. Yet, [P… view at source ↗
Figure 2
Figure 2. Unoptimized obfuscation of check char 0 Divider [5] — adds a number k of conditional state￾ments depending on new fresh inputs, increasing the number of paths to explore by a factor of 2k . Also, in this implementation we use a junk variable garb and two additional inputs ch1 and ch2 unrelated to the original code. The novel obfuscation For (Sec. 5) adds k loops whose upper bound depends on distinct input bytes and … view at source ↗
Figure 3
Figure 3. Enhanced For – check char 0 Question: How to protect path-oriented protections against code analysis-based attacks (slicing, tainting, patterns)? The goal of this paper is to define, analyze and explore in a systematic way the potential of path￾oriented transformations as anti-DSE protections. We define a predictive framework (Sec. 4) and propose several new concrete protections (Sec. 5). In particular, our framewor… view at source ↗
Figures from the paper (7 more)
Figure 4
Figure 4. Figure 4: Path-Oriented Obfuscation Framework 4.1 Basic definitions This paper deals with a specific kind of protections tar￾geting DSE: path-oriented protections. Transforming a program P into P 0 using path-oriented protections ensures that P 0 is functionally equivalent to P …
Figure 6
Figure 6. Figure 6: Split obfuscation Split [5]. This transformation ( [PITH_FULL_IMAGE:figures/full_fig_p007_6.png]
Figure 7
Figure 7. Figure 7: Write obfuscation Symbolic execution engines are not likely to relate a and input, thus thinking that a is constant across all executions. If the dynamic part of the engine spots that a may have different values, it will iterate over every possible values of input, cre…
Figure 8
Figure 8. Figure 8: Several encodings of protection For 7.1 Pattern attacks Pattern attacks search for specific patterns in the code of a program to identify, and remove, known obfus￾cations. This kind of analysis assumes more or less similar constructions across all implementations of an…
Figure 10
Figure 10. Figure 10: Impact of variable size to For strength and cost Pattern Paths Loop iterations int func ( int x) { int var = 0 ; fo r ( int i =0; i<x ; i++) { var++; } return var ; } 2 32 ≤ 2 32 int func ( int x ) { char tmp[4] = x; char var [ 4 ] = {0}; fo r ( int i =0; i<tmp[0] ; i…
Figure 9
Figure 9. Figure 9: Step by Step execution of Write with the runtime value of input being 100 1 L : mov [ a ] , [ i n p u t ] → L1 : mov L2+o f f , [ i n p u t ] L2 : mov [ a ] , 0 2 L : mov [ a ] , [ i n p u t ] L1 : mov L2+o f f , [ i n p u t ] → L2 : mov [ a ] , runtime val 3 L : mov […
Figure 11
Figure 11. Figure 11: Runtime overhead w.r.t. to the number of [PITH_FULL_IMAGE:figures/full_fig_p022_11.png]

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

  1. SATURN -- Software Deobfuscation Framework Based on LLVM

    cs.CR 2019-09 conditional novelty 6.0 of 10

    SATURN automatically lifts obfuscated x86_64 binaries to LLVM-IR, recovers control flow, detects and removes opaque predicates, reconstructs stack and arguments, and recompiles a cleaned version.

Reference graph

Works this paper leans on

50 extracted references · 50 canonical work pages · cited by 1 Pith paper

  1. [1]

    http://tigress.cs.arizona.edu/challenges.html

    Tigress challenge. http://tigress.cs.arizona.edu/challenges.html

    work page

  2. [2]

    Anand, E

    S. Anand, E. K. Burke, T. Y. Chen, J. Clark, M. B. Cohen, W. Grieskamp, M. Harman, M. J. Harrold, and P. McMinn. An orchestrated survey of methodologies for automated software test case generation. Journal of Systems and Software , 2013

    work page 2013

  3. [3]

    Enhancing symbolic ex- ecution with veritesting

    Thanassis Avgerinos, Alexandre Rebert, Sang Kil Cha, and David Brumley. Enhancing symbolic ex- ecution with veritesting. Commun. ACM, 59(6), 2016

    work page 2016

  4. [4]

    Gogul Balakrishnan and Thomas W. Reps. WYS- INWYX: what you see is not what you execute. ACM Trans. Program. Lang. Syst., 32, 2010

    work page 2010

  5. [5]

    Collberg, Vi- jay Ganesh, Zack Newsham, and Alexander Pretschner

    Sebastian Banescu, Christian S. Collberg, Vi- jay Ganesh, Zack Newsham, and Alexander Pretschner. Code obfuscation against symbolic execution attacks. In Annual Conference on Com- puter Security Applications, ACSAC 2016 , 2016

    work page 2016

  6. [6]

    Collberg, and Alexander Pretschner

    Sebastian Banescu, Christian S. Collberg, and Alexander Pretschner. Predicting the resilience of obfuscated code against symbolic execution at- tacks via machine learning. In USENIX Security Symposium, 2017

    work page 2017

  7. [7]

    Vadhan, and Ke Yang

    Boaz Barak, Oded Goldreich, Russell Impagli- azzo, Steven Rudich, Amit Sahai, Salil P. Vadhan, and Ke Yang. On the (im)possibility of obfus- cating programs. In Advances in Cryptology - CRYPTO, 2001

    work page 2001

  8. [8]

    Backward-bounded DSE: targeting in- feasibility questions on obfuscated codes

    S´ ebastien Bardin, Robin David, and Jean-Yves Marion. Backward-bounded DSE: targeting in- feasibility questions on obfuscated codes. In 2017 IEEE Symposium on Security and Privacy, SP , 2017

    work page 2017

Show all 50 references
  1. [9]

    Satisfiability Modulo Theories

    Clark Barrett and Cesare Tinelli. Satisfiability Modulo Theories. Springer International Publish- ing, 2018

    2018

  2. [10]

    Bounded Model Checking

    Armin Biere. Bounded Model Checking. In Hand- book of Satisfiability. 2009

    2009

  3. [11]

    Effectiveness of synthesis in concolic deobfuscation

    Fabrizio Biondi, S´ ebastien Josse, Axel Legay, and Thomas Sirvent. Effectiveness of synthesis in concolic deobfuscation. Computers & Security , 70, 2017. 17

    2017

  4. [12]

    Fernandez, Jean- Yves Marion, Benjamin Rouxel, Fabrice Sabatier, and Aur´ elien Thierry

    Guillaume Bonfante, Jos´ e M. Fernandez, Jean- Yves Marion, Benjamin Rouxel, Fabrice Sabatier, and Aur´ elien Thierry. Codisasm: Medium scale concatic disassembly of self-modifying binaries with overlapping instructions. In Conference on Computer and Communications Security , 2015

    2015

  5. [13]

    Boolector: An efficient SMT solver for bit-vectors and ar- rays

    Robert Brummayer and Armin Biere. Boolector: An efficient SMT solver for bit-vectors and ar- rays. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2009

    2009

  6. [14]

    Code obfuscation against abstract model checking attacks

    Roberto Bruni, Roberto Giacobazzi, and Roberta Gori. Code obfuscation against abstract model checking attacks. In Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI, 2018

    2018

  7. [15]

    Targeted program transforma- tions for symbolic execution

    Cristian Cadar. Targeted program transforma- tions for symbolic execution. In Meeting on Foun- dations of Software Engineering, ESEC/FSE , 2015

    2015

  8. [16]

    Cristian Cadar, Daniel Dunbar, and Dawson R. Engler. KLEE: unassisted and automatic gener- ation of high-coverage tests for complex systems programs. In 8th USENIX Symposium on Oper- ating Systems Design and Implementation, OSDI , 2008

    2008

  9. [17]

    Symbolic exe- cution for software testing: three decades later

    Cristian Cadar and Koushik Sen. Symbolic exe- cution for software testing: three decades later. Commun. ACM, 56(2), 2013

    2013

  10. [18]

    Unleashing mayhem on binary code

    Sang Kil Cha, Thanassis Avgerinos, Alexandre Rebert, and David Brumley. Unleashing mayhem on binary code. In Symposium on Security and Privacy, SP, 2012

    2012

  11. [19]

    Surrepti- tious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection

    Christian Collberg and Jasvir Nagra. Surrepti- tious Software: Obfuscation, Watermarking, and Tamperproofing for Software Protection. Addison- Wesley Professional, 1st edition, 2009

    2009

  12. [20]

    A taxonomy of obfuscating transfor- mations, 1997

    Christian Collberg, Clark Thomborson, and Dou- glas Low. A taxonomy of obfuscating transfor- mations, 1997

    1997

  13. [21]

    Collberg, Sam Martin, Jonathan Myers, and Jasvir Nagra

    Christian S. Collberg, Sam Martin, Jonathan Myers, and Jasvir Nagra. Distributed applica- tion tamper detection via continuous software updates. In Annual Computer Security Applica- tions Conference, ACSAC, 2012

    2012

  14. [22]

    Kevin Coogan, Gen Lu, and Saumya K. Debray. Deobfuscation of virtualization-obfuscated soft- ware: a semantics-based approach. In Confer- ence on Computer and Communications Security, CCS, 2011

    2011

  15. [23]

    Specifica- tion of concretization and symbolization policies in symbolic execution

    Robin David, S´ ebastien Bardin, Josselin Feist, Laurent Mounier, Marie-Laure Potet, Thanh Dinh Ta, and Jean-Yves Marion. Specifica- tion of concretization and symbolization policies in symbolic execution. In International Sympo- sium on Software Testing and Analysis, ISSTA 2016, 2016

    2016

  16. [24]

    BINSEC/SE: A dynamic symbolic execution toolkit for binary- level analysis

    Robin David, S´ ebastien Bardin, Thanh Dinh Ta, Laurent Mounier, Josselin Feist, Marie-Laure Potet, and Jean-Yves Marion. BINSEC/SE: A dynamic symbolic execution toolkit for binary- level analysis. In IEEE 23rd International Con- ference on Software Analysis, Evolution, and Re...

    2016

  17. [25]

    Z3: an efficient SMT solver

    Leonardo Mendon¸ ca de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS, 2008

    2008

  18. [26]

    Debray and Jay Patel

    Saumya K. Debray and Jay Patel. Reverse engi- neering self-modifying code: Unpacker extraction. In Working Conference on Reverse Engineering, WCRE, 2010

    2010

  19. [27]

    Defeating mba-based obfuscation

    Ninon Eyrolles, Louis Goubin, and Marion Videau. Defeating mba-based obfuscation. In Proceedings of the 2016 ACM Workshop on Soft- ware PROtection, SPRO@CCS 2016 , 2016

    2016

  20. [28]

    Levin, and David A

    Patrice Godefroid, Michael Y. Levin, and David A. Molnar. SAGE: whitebox fuzzing for security testing. Commun. ACM, 55(3), 2012

    2012

  21. [29]

    Henzinger, Ranjit Jhala, Rupak Ma- jumdar, and Gr´ egoire Sutre

    Thomas A. Henzinger, Ranjit Jhala, Rupak Ma- jumdar, and Gr´ egoire Sutre. Lazy abstraction. 18 In The 29th SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) , 2002

    2002

  22. [30]

    Renovo: a hidden code extractor for packed executables

    Min Gyung Kang, Pongsin Poosankam, and Heng Yin. Renovo: a hidden code extractor for packed executables. In ACM Workshop Recurring Mal- code (WORM). ACM, 2007

    2007

  23. [31]

    Towards static analysis of virtualization-obfuscated binaries

    Johannes Kinder. Towards static analysis of virtualization-obfuscated binaries. In 19th Work- ing Conference on Reverse Engineering, WCRE , 2012

    2012

  24. [32]

    Implicit flows: Can’t live with ’em, can’t live without ’em

    Dave King, Boniface Hicks, Michael Hicks, and Trent Jaeger. Implicit flows: Can’t live with ’em, can’t live without ’em. In Information Systems Security, 4th International Conference, ICISS , 2008

    2008

  25. [33]

    Static information flow analysis with handling of implicit flows and a study on effects of implicit flows vs explicit flows

    Yin Liu and Ana Milanova. Static information flow analysis with handling of implicit flows and a study on effects of implicit flows vs explicit flows. In 14th European Conference on Software Maintenance and Reengineering, CSMR, 2010

    2010

  26. [34]

    Gebo- tys, Krzysztof Czarnecki, and Vijay Ganesh

    Saeed Nejati, Jia Hui Liang, Catherine H. Gebo- tys, Krzysztof Czarnecki, and Vijay Ganesh. Adaptive restart and cegar-based solver for in- verting cryptographic hash functions. In Verified Software. Theories, Tools, and Experiments - 9th International Conference, VSTTE 2017 , 2017

    2017

  27. [35]

    Symbolic deobfuscation: from vir- tualized code back to the original

    Jonathan Salwan, Sbastien Bardin, and Marie- Laure Potet. Symbolic deobfuscation: from vir- tualized code back to the original. In 5th Con- ference on Detection of Intrusions and malware & Vulnerability Assessment (DIMVA), 2018

    2018

  28. [36]

    Triton : Framework d’excution concolique

    Florent Saudel and Jonathan Salwan. Triton : Framework d’excution concolique. In SSTIC, 2015

    2015

  29. [37]

    Protecting software through obfuscation: Can it keep pace with progress in code analysis? ACM Comput

    Sebastian Schrittwieser, Stefan Katzenbeisser, Johannes Kinder, Georg Merzdovnik, and Edgar Weippl. Protecting software through obfuscation: Can it keep pace with progress in code analysis? ACM Comput. Surv. , 49(1), 2016

    2016

  30. [38]

    Schwartz, Thanassis Avgerinos, and David Brumley

    Edward J. Schwartz, Thanassis Avgerinos, and David Brumley. All you ever wanted to know about dynamic taint analysis and forward sym- bolic execution (but might have been afraid to ask). In Symposium on Security and Privacy, S&P, 2010

    2010

  31. [39]

    The geometry of innocent flesh on the bone: return-into-libc without function calls (on the x86)

    Hovav Shacham. The geometry of innocent flesh on the bone: return-into-libc without function calls (on the x86). In Conference on Computer and Communications Security, CCS , 2007

    2007

  32. [40]

    Sharif, Andrea Lanzi, Jonathon T

    Monirul I. Sharif, Andrea Lanzi, Jonathon T. Giffin, and Wenke Lee. Impeding malware anal- ysis using conditional code obfuscation. In Net- work and Distributed System Security Symposium, NDSS, 2008

    2008

  33. [41]

    SOK: (state of) the art of war: Offensive tech- niques in binary analysis

    Yan Shoshitaishvili, Ruoyu Wang, Christopher Salls, Nick Stephens, Mario Polino, Andrew Dutcher, John Grosen, Siji Feng, Christophe Hauser, Christopher Kr¨ ugel, and Giovanni Vigna. SOK: (state of) the art of war: Offensive tech- niques in binary analysis. In IEEE Symposium on ...

    2016

  34. [42]

    Venkatesh Srinivasan and Thomas W. Reps. An improved algorithm for slicing machine code. In Proceedings of the 2016 ACM SIGPLAN Interna- tional Conference on Object-Oriented Program- ming, Systems, Languages, and Applications, OOPSLA 2016. ACM

    2016

  35. [43]

    Coll- berg, Saumya Debray, and Carlos Scheidegger

    Jon Stephens, Babak Yadegari, Christian S. Coll- berg, Saumya Debray, and Carlos Scheidegger. Probabilistic obfuscation through covert chan- nels. In European Symposium on Security and Privacy, EuroS&P, 2018

    2018

  36. [44]

    SMT solvers in software security

    Julien Vanegue and Sean Heelan. SMT solvers in software security. In 6th USENIX Workshop on Offensive Technologies, WOOT’12 , 2012

    2012

  37. [45]

    Software tamper resistance: Ob- structing static analysis of programs

    Chenxi Wang, Jonathan Hill, John Knight, and Jack Davidson. Software tamper resistance: Ob- structing static analysis of programs. Technical report, Charlottesville, VA, USA, 2000. 19

    2000

  38. [46]

    Knight, and Jack W

    Chenxi Wang, Jonathan Hill, John C. Knight, and Jack W. Davidson. Protection of software- based survivability mechanisms. In International Conference on Dependable Systems and Networks (DSN), 2001

    2001

  39. [47]

    Linear obfuscation to combat symbolic execution

    Zhi Wang, Jiang Ming, Chunfu Jia, and Debin Gao. Linear obfuscation to combat symbolic execution. In European Symposium on Research in Computer Security, ESORICS , 2011

    2011

  40. [48]

    Symbolic execution of obfuscated code

    Babak Yadegari and Saumya Debray. Symbolic execution of obfuscated code. In Conference on Computer and Communications Security (CCS) , 2015

    2015

  41. [49]

    A generic approach to automatic deobfuscation of executable code

    Babak Yadegari, Brian Johannesmeyer, Ben Whitely, and Saumya Debray. A generic approach to automatic deobfuscation of executable code. In Symposium on Security and Privacy, SP , 2015

    2015

  42. [50]

    Information hiding in software with mixed boolean-arithmetic transforms

    Yongxin Zhou, Alec Main, Yuan Xiang Gu, and Harold Johnson. Information hiding in software with mixed boolean-arithmetic transforms. In Information Security Applications, WISA , 2007. 20 A Additional information on patterns Write. In this section we give more details about the...

    2007

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.