Eunsuk Kang Postdoctoral Researcher Department of Electrical Engineering and Computer Sciences University of California, Berkeley office: 545K Cory Hall email: eunsuk.kang at berkeley.edu

I am a postdoctoral scholar working with Prof. Stéphane Lafortune at the University of Michigan, and Prof. Stavros Tripakis at UC Berkeley. My research is supported by the NSF Expeditions in Computer Augmented Programming Engineering (ExCAPE).

I received my PhD in Computer Science from MIT, working with Prof. Daniel Jackson.

Research

My research interests lie in software engineering and programming languages. I am especially interested in leveraging lightweight formal methods to construct software systems that are safe, secure, and reliable to use.

Topics Software reliability, modeling, verification, design methodologies, and cyber-physical systems.

I've also spent summers working with Rajeev Joshi at the NASA JPL, and Ethan Jackson at Microsoft Research on FORMULA.

I was a member of the MIT Programming Languages group.

Before coming to MIT, I studied software engineering at the University of Waterloo, where I spent several terms as a member of WatForm.

Publications

• A Toolkit for Construction of Authorization Service Infrastructure for the Internet of Things.
  Hokeun Kim, Eunsuk Kang, Edward A. Lee, and David Broman.
  ACM/IEEE International Conference on Internet-of-Things Design and Implementation (IoTDI), 2017.
  Best Paper Award
• Multi-Representational Security Analysis.
  Eunsuk Kang, Aleksandar Milicevic, and Daniel Jackson.
  Symposium on the Foundations of Software Engineering (FSE), 2016.
  ACM SIGSOFT Distinguished Paper Award
• Designing Minimal Effective Normative Systems with the Help of Lightweight Formal Methods.
  Jianye Hao, Eunsuk Kang, Sun Jun, and Daniel Jackson.
  Symposium on the Foundations of Software Engineering (FSE), 2016.
• Design Space Exploration for Security.
  Eunsuk Kang.
  IEEE Conference on Cybersecurity Development (SecDev), 2016.
• Model-Based Security Analysis of a Water Treatment System.
  Eunsuk Kang, Sridhar Adepu, Daniel Jackson, and Aditya P. Mathur.
  ICSE Workshop on Smart Cyber-Physical Systems, 2016.
• Alloy*: A Higher-order Relational Constraint Solver
  Aleksandar Milicevic, Joseph P. Near, Eunsuk Kang and Daniel Jackson.
  International Conference on Software Engineering (ICSE), 2015.
  ACM SIGSOFT Distinguished Paper Award
• Detection of Design Flaws in the Android Permission Protocol through Bounded Verification.
  Hamid Bagheri, Eunsuk Kang, Sam Malek, and Daniel Jackson.
  International Symposium on Formal Methods (FM), 2015.
• Adaptive Defending Strategy for Smart Grid Attacks
  Jianye Hao, Eunsuk Kang, Daniel Jackson, and Jun Sun.
  Workshop on Smart Energy Grid Security, CCS, 2014.
• A Model-Based Framework for Security Configuration Analysis
  Eunsuk Kang and Daniel Jackson.
  Manuscript, 2012.
• A Lightweight Code Analysis and Its Role in Evaluation of a Dependability Case
  Joseph P. Near, Aleksandar Milicevic, Eunsuk Kang and Daniel Jackson.
  International Conference on Software Engineering (ICSE), 2011.
• Dependability Arguments with Trusted Bases (slides)
  Eunsuk Kang and Daniel Jackson.
  International Conference on Requirements Engineering (RE), 2010.
• Separation of Concerns for Dependable Software Design (slides)
  Daniel Jackson and Eunsuk Kang.
  FSE Workshop on the Future of Software Engineering Research, 2010.
• Components, Platforms, and Possibilities: Towards Generic Automation for MDA
  Ethan Jackson, Eunsuk Kang, Dirk Seifert, Markus Dahlweid, and Thomas Santen.
  International Conference on Embedded Software (EMSOFT), 2010.
• Patterns for Dependable Systems with Trusted Bases
  Eunsuk Kang and Daniel Jackson.
  Pattern Languages of Programs Conference (PLOP), 2010.
• An Approach for Effective Design Space Exploration
  Eunsuk Kang, Ethan Jackson, and Wolfram Schulte.
  Monterey Workshop on Software Systems, 2010.
• Property-Part Diagrams: A Dependence Notation for Software systems
  Daniel Jackson and Eunsuk Kang.
  Software Design and Requirements: The Work of Michael Jackson, 2010.
• A Framework for Dependability Analysis of Software Systems with Trusted Bases
  Eunsuk Kang.
  Master's thesis, MIT, January 2010.
• Formal Modeling and Analysis of a Flash Filesystem (slides)
  Eunsuk Kang and Daniel Jackson.
  International Conference on ASM, B, and Z (ABZ), 2008.
  An extended version in the International Journal of Software and Informatics, Vol. 3, No. 2, 2009.
• Improving the Usability of HOL through Controlled Automation Tactics (slides)
  Eunsuk Kang and Mark Aagaard.
  International Conference on Theorem Proving in Higher Order Logics (TPHOLs), 2007.

Teaching

Spring 2013 6.170 Software Studio (Curriculum Development)
IAP 2010 6.088 Introduction to C/C++ Programming (Instructor)
Fall 2009 6.00 Introduction to Computer Science and Programming (TA)
Fall 2008 6.005 Elements of Software Construction (TA)

Miscellaneous

I was a member of the CSAIL Student Committee. I also helped organize the CSAIL Student Workshop and the CSAIL Olympics.

My academic genealogy