publications

2023

1. Simplifying Mixed Boolean-Arithmetic Obfuscation by Program Synthesis and Term Rewriting Lee, Jaehyung, and Lee, Woosuk In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security 2023 [Abs] [PDF] [Slides]

   Mixed Boolean Arithmetic (MBA) obfuscation transforms a program expression into an equivalent but complex expression that is hard to understand. MBA obfuscation has been popular to protect programs from reverse engineering thanks to its simplicity and effectiveness. However, it is also used for evading malware detection, necessitating the development of effective MBA deobfuscation techniques. Existing deobfuscation methods suffer from either of the four limitations: (1) lack of general applicability, (2) lack of flexibility, (3) lack of scalability, and (4) lack of correctness. In this paper, we propose a versatile MBA deobfuscation method that synergistically combines program synthesis, term rewriting, and an algebraic simplification method. The key novelty of our approach is that we perform on-the-fly learning of transformation rules for deobfuscation, and apply them to rewrite the input MBA expression. We implement our method in a tool called ProMBA and evaluate it on over 4000 MBA expressions obfuscated by the state-of-the-art obfuscation tools. Experimental results show that our method outperforms the state-of-the-art MBA deobfuscation tools by a large margin, successfully simplifying a vast majority of the obfuscated expressions into their original forms.

2. Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Time-Bounded Exhaustive Search Lee, Dongkwon, Lee, Woosuk, Oh, Hakjoo, and Yi, Kwangkeun ACM Trans. Program. Lang. Syst. 2023 [Abs] [PDF]

   We present a new and general method for optimizing homomorphic evaluation circuits. Although fully homomorphic encryption (FHE) holds the promise of enabling safe and secure third party computation, building FHE applications has been challenging due to their high computational costs. Domain-specific optimizations require a great deal of expertise on the underlying FHE schemes and FHE compilers that aim to lower the hurdle, generate outcomes that are typically sub-optimal, as they rely on manually-developed optimization rules. In this article, based on the prior work of FHE compilers, we propose a method for automatically learning and using optimization rules for FHE circuits. Our method focuses on reducing the maximum multiplicative depth, the decisive performance bottleneck, of FHE circuits by combining program synthesis, term rewriting, and equality saturation. It first uses program synthesis to learn equivalences of small circuits as rewrite rules from a set of training circuits. Then, we perform term rewriting on the input circuit to obtain a new circuit that has lower multiplicative depth. Our rewriting method uses the equational matching with generalized version of the learned rules, and its soundness property is formally proven. Our optimizations also try to explore every possible alternative order of applying rewrite rules by time-bounded exhaustive search technique called equality saturation. Experimental results show that our method generates circuits that can be homomorphically evaluated 1.08\texttimes–3.17\texttimes faster (with the geometric mean of 1.56\texttimes) than the state-of-the-art method. Our method is also orthogonal to existing domain-specific optimizations.

3. Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation Yoon, Yongho, Lee, Woosuk, and Yi, Kwangkeun Proc. ACM Program. Lang. (44th ACM SIGPLAN Conference on Programming Language Design and Implementation) 2023 [Abs] [PDF] [Slides]

   A key challenge in example-based program synthesis is the gigantic search space of programs. To address this challenge, various work proposed to use abstract interpretation to prune the search space. However, most of existing approaches have focused only on forward abstract interpretation, and thus cannot fully exploit the power of abstract interpretation. In this paper, we propose a novel approach to inductive program synthesis via iterative forward-backward abstract interpretation. The forward abstract interpretation computes possible outputs of a program given inputs, while the backward abstract interpretation computes possible inputs of a program given outputs. By iteratively performing the two abstract interpretations in an alternating fashion, we can effectively determine if any completion of each partial program as a candidate can satisfy the input-output examples. We apply our approach to a standard formulation, syntax-guided synthesis (SyGuS), thereby supporting a wide range of inductive synthesis tasks. We have implemented our approach and evaluated it on a set of benchmarks from the prior work. The experimental results show that our approach significantly outperforms the state-of-the-art approaches thanks to the sophisticated abstract interpretation techniques.

4. Madusa: mobile application demo generation based on usage scenarios Lee, Jaehyung, Cho, Hangyeol, and Lee, Woosuk Journal of Automated Software Engineering 2023 [Abs] [PDF]

   Mobile applications have grown rapidly in size. This dramatic increases in size and complexity make mobile applications less accessible to a broader scope of users. The prevailing approach for better accessibility of mobile applications is to manually reimplement slimmed versions with a small but representative portion of a regular original app. Unfortunately, this approach imposes significant burden on developers. We propose a system called Madusa to enable developers to effectively customize and reduce their mobile applications for Android. Madusa takes as input an original app, an upper bound on the size of a reduced version, and usage scenarios as a high-level specification of its desired core functionality. The output is a reduced version of the app that is still correct with respect to the specification while not exceeding the size limit. Madusa constructs a graph representing dependencies among methods and resources and identifies a sub-part of the graph using integer linear programming to generate a reduced version that exhibits behaviors as similar as possible to the original app. Our experimental evaluation on a suite of 19 Android apps available on Google Play Store. Madusa effectively converges to the desired simplified apps by reducing the app size by 40% on average (maximally by 60%). We conclude our approach effectively removes redundant code and resources with respect to given usage scenarios.

5. Inductive Synthesis of Structurally Recursive Functional Programs from Non-Recursive Expressions Lee, Woosuk, and Cho, Hangyeol Proc. ACM Program. Lang. (50th ACM SIGPLAN Symposium on Principles of Programming Languages) 2023 [Abs] [PDF] [Slides]

   We present a novel approach to synthesizing recursive functional programs from input-output examples. Synthesizing a recursive function is challenging because recursive subexpressions should be constructed while the target function has not been fully defined yet. We address this challenge by using a new technique we call block-based pruning. A block refers to a recursion- and conditional-free expression (i.e., straight-line code) that yields an output from a particular input. We first synthesize as many blocks as possible for each input-output example, and then we explore the space of recursive programs, pruning candidates that are inconsistent with the blocks. Our method is based on an efficient version space learning, thereby effectively dealing with a possibly enormous number of blocks. In addition, we present a method that uses sampled input-output behaviors of library functions to enable a goal-directed search for a recursive program using the library. We have implemented our approach in a system called Trio and evaluated it on synthesis tasks from prior work and on new tasks. Our experiments show that Trio outperforms prior work by synthesizing a solution to 98% of the benchmarks in our benchmark suite.

2022

1. Datalog Static Analysis in Secrecy Kouhounestani, Mojgan, and Lee, Woosuk IEEE Access 2022 [PDF]

2021

1. Context-Aware and Data-Driven Feedback Generation for Programming Assignments Song, Dowon, Lee, Woosuk, and Oh, Hakjoo In Proceedings of the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE) 2021 [PDF]
2. Combining the Top-down Propagation and Bottom-up Enumeration for Inductive Program Synthesis Lee, Woosuk In Proceedings of the 48th ACM SIGPLAN Symposium on Principles of Programming Languages 2021 [PDF] [Slides]

2020

1. Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Term Rewriting Lee, DongKwon, Lee*, Woosuk, Oh, Hakjoo, and Yi, Kwangkeun In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation 2020 [PDF] [Slides]

2018

1. Effective Program Debloating via Reinforcement Learning Heo, Kihong*, Lee, Woosuk*, Pashakhanloo, Pardis, and Naik, Mayur In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security 2018 [PDF] [Slides]
2. Syntax-guided Synthesis of Datalog Programs Si, Xujie*, Lee, Woosuk*, Zhang, Richard, Albarghouthi, Aws, Koutris, Paraschos, and Naik, Mayur In Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering 2018 [PDF] [Slides]
3. Accelerating Search-based Program Synthesis Using Learned Probabilistic Models Lee, Woosuk, Heo, Kihong, Alur, Rajeev, and Naik, Mayur In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation 2018 [PDF] [Slides]
4. Beyond Deductive Methods in Program Analysis Kulkarni, Sulekha, Zhang, Richard, Si, Ximing, Heo, Kihong, Lee, Woosuk, and Naik, Mayur In 2018

2017

1. Sound Non-Statistical Clustering of Static Analysis Alarms Lee, Woosuk, Lee, Wonchan, Kang, Dongok, Heo, Kihong, Oh, Hakjoo, and Yi, Kwangkeun ACM Trans. Program. Lang. Syst. 2017 [PDF]

2016

1. Lee, W. (2016). Improving the Usability of Static Analyzers. Seoul National University. [PDF]

2015

1. Static Analysis with Set-Closure in Secrecy Lee, Woosuk, Hong, Hyunsook, Yi, Kwangkeun, and Cheon, Jung Hee In 22nd International Static Analysis Symposium 2015 [PDF] [Slides]

2014

1. A Progress Bar for Static Analyzers Lee, Woosuk, Oh, Hakjoo, and Yi, Kwangkeun In 21st International Static Analysis Symposium 2014 [PDF] [Slides]
2. Global Sparse Analysis Framework Oh, Hakjoo, Heo, Kihong, Lee, Wonchan, Lee, Woosuk, Park, Daejun, Kang, Jeehoon, and Yi, Kwangkeun ACM Trans. Program. Lang. Syst. 2014 [PDF]

2012

1. Sound Non-statistical Clustering of Static Analysis Alarms Lee, Woosuk, Lee, Wonchan, and Yi, Kwangkeun In Verification, Model Checking, and Abstract Interpretation 2012 [PDF] [Slides]
2. Design and Implementation of Sparse Global Analyses for C-like Languages Oh, Hakjoo, Heo, Kihong, Lee, Wonchan, Lee, Woosuk, and Yi, Kwangkeun In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation 2012 [PDF]