[Abstract]
프로그램 최적화는 어떤 원본 프로그램을 의미가 동일하면서도 어떤 측면(계산비용, 가독성 등)에서 더 나은 프로그램으로 변환하는 기술이다. 프로그램 최적화는 프로그램 의미를 보존하는 변환 규칙을 반복 적용하는 형태로 진행된다. 전통적으로 이러한 변환 규칙들은 도메인 지식을 갖춘 전문가에 의해 수동 작성되어 사용되었는데, 제한적인 변환 규칙들로 인한 탐색범위가 제한되거나, 최적이 아닌 순서로 변환규칙을 적용함에 따라 더 나은 최적화 기회를 놓치는 한계가 존재한다.
본 세미나에서는 기존 프로그램 최적화의 한계를 프로그램 합성 기술을 사용하여 극복한 사례들을 소개한다. 프로그램 합성이란 요구조건 명세에 100% 부합하는 프로그램을 자동으로 생성하는 기술로서, 다양한 탐색 알고리즘 및 프로그래밍언어 이론에 기반을 두고 있다. 기존 최적화 방법의 한계를 극복하기 위해 프로그램 합성으로 도메인 지식없이 자동으로 변환 규칙을 발견하고, 발견된 변환 규칙들을 최적에 가까운 순서로 적용하는 방법을 소개한다. 정교한 변환 규칙 발견을 위해 개발한 고성능 프로그램 합성 기술 또한 소개한다. 본 방법을 소프트웨어 보안 관련 두 응용에 적용해 본 결과도 제시한다. 평문코드를 암호화된 채로 실행할 수 있게 하는 정수 동형암호(Homomorphic encryption) 컴파일러에 적용한 결과 수동 작성된 변환규칙 대비 최대 3배이상의 빠른 실행속도를 확인할 수 있었다. 또한, 악성웨어 탐지 회피를 위해 쓰이는 연산식 난독화(Mixed boolean arithmetic obfuscation)를 단순화하는 작업에 적용한 결과, 수동 작성된 단순화 규칙 대비 평균 7배 이상의 코드 단순화 효과를 달성하였다.

[Biography]
이우석교수는 2016년 서울대학교에서 컴퓨터공학 박사학위를 취득한 후 미국 조지아텍(2016.3-2017.1)과 펜실베니아 대학교(2017.1-2018.8)에서 박사후 연구원으로 재직하였다. 2018년 9월부터 한양대학교 에리카 캠퍼스 컴퓨터학부 조교수로 재직중이다. 연구분야는 프로그래밍언어 및 소프트웨어공학이다 (세부분야: 프로그램 분석, 프로그램 자동 생성).