Jinseong Jeon

Research Interests

• Static analysis: program logic, symbolic execution, program synthesis
• Formal verification: SAT/SMT, temporal logic
• Security & privacy: security policy, static/dynamic enforcement
• Compiler optimization: memory system, parallelism

Publications

• Android Security and Privacy
• SymDroid: Symbolic Execution for Dalvik Bytecode. [doi]
  Jinseong Jeon, Kristopher K. Micinski, and Jeffrey S. Foster. CS-TR-5022, Department of Computer Science, University of Maryland, College Park, Jul 2012.
• Dr. Android and Mr. Hide: Fine-grained Permissions in Android Applications. [doi][slides]
  Jinseong Jeon, Kristopher K. Micinski, Jeffrey A. Vaughan, Ari Fogel, Nikhilesh Reddy, Jeffery S. Foster, and Todd Millstein. In ACM CCS Workshop on Security and Privacy in Smartphones and Mobile Devices (SPSM '12), Oct 2012.
• Systematic Testing
• Troyd: Integration Testing for Android. [doi]
  Jinseong Jeon and Jeffrey S. Foster. CS-TR-5013, Department of Computer Science, University of Maryland, College Park, Aug 2012.
• SAT-based On-line Fault Isolation in Serial Systems. [doi]
  Jinseong Jeon, Sangwon Kim, and Dongkeun Lee. In International Conference on Advances in System Testing and Validation Lifecycle (VALID '09), Sep 2009.
• Memory Layout Optimization
• Abstracting Access Patterns of Dynamic Memory Using Regular Expressions. [doi]
  Jinseong Jeon, Keoncheol Shin, and Hwansoo Han. ACM Transactions on Architecture and Code Optimization (TACO), Vol. 5(4), Article 18, Mar 2009.
• Layout Transformations for Heap Objects Using Static Access Patterns. [doi]
  Jinseong Jeon, Keoncheol Shin, and Hwansoo Han. In International Conference on Compiler Construction (CC '07), Mar 2007.
• Static Transformation for Heap Layout Using Memory Access Patterns. [slides]
  Jinseong Jeon, Master Thesis, KAIST, 2007. (Outstanding master's thesis)

Software

• Troyd: Integration Testing for Android
• Redexer: Binary Instrumentation Framework for Dalvik
• RTFA: Memory Layout Optimizer for C Programs

Projects

• Expeditions in Computer Augmented Program Engineering (ExCAPE): Harnessing Synthesis for Software Design
  • National Science Foundation (NSF), 2012. 4 ~ current
• Program Analysis for Smartphone Application Security
  • National Science Foundation (NSF), 2011. 4 ~ current
• Airborne Tactical ELINT (ELectronic INTelligence) System
  • Agency for Defense Development (ADD), 2007. 11 ~ 2010. 7
• Scalable and Precise Buffer Overrun Analyzer for Real World C Applications
  • Microsoft Research Asia (MSRA), University Grant Program, 2006. 3 ~ 2007. 2
• Source Code Vulnerability Detection Using Partial Compilation
  • National Security Research Institute (NSRI), 2005. 4 ~ 2005. 11

Education & Experience

• 2010. 8 ~ current, Ph.D. student, Computer Science, UMD
• 2007. 2 ~ 2010. 7, Researcher, Agency for Defense Development, Korea
• 2005. 3 ~ 2007. 2, M.S., Computer Science, KAIST
• 2001. 3 ~ 2005. 2, B.S., Computer Science, KAIST
• 1999. 3 ~ 2001. 2, Graduated from Kwangju Science High School