Research

Our research topic range over

  • programming language theory
  • program verification
  • mining of program data
  • program security
  • other programming language related subjects.

Malware Detection

소프트웨어 바이러스는 갈수록 기승을 부리고 있으며 자기 복제 및 코드 생성하는 방식으로 발전하고 있다. 결국 특정 signature 를 찾아내어 바이러스를 검출하는 종전의 방식은 한계가 있을 수 밖에 없으며, 프로그램이 결국 어떤 일을 수행하는지를 살피는 프로그램 의미 분석을 통한 접근 방식이 해결책이 될 수 있다.

Formal Verification on Esterel Program

Esterel은 일종의 hardware description language 로서 VHDL이나 Verilog보다 좀 더 상위 level 의 모델링을 가능하게 한다. Esterel의 시간축상의 동작의 정합성을 분석하는 연구.

Synchronous Reactive Program Analysis

Esterel은 synchronous reactive programming language의 일종이다. Reactive system이란 외부환경에 끊임없이 반응하는 input-driven 시스템을 말한다. Esterel은 reactive system을 쉽게 설계하기 위해 개발된 언어이고, 하드웨어(VHDL)나 소프트웨어(C)로 변환 가능하다. 외부 input에 따라 프로그램의 행동이 결정되고 주로 종료없이 무한 수행되므로 가능한 실행 trace가 무수히 많고 각 trace의 길이에도 제한이 없다. 본 연구는 Esterel로 작성된 프로그램의 실행 가능한 모든 trace들을 프로그램 요약해석 기법을 이용해서 하나의 축약된 형태로 정리하는 연구이고, 이렇게 표현된 프로그램의 표현은 프로그램의 이해 및 검증(debugging, simulation)에 적용가능하다. 외부환경에 대한 시뮬레이션이나 복잡한 디버깅 없이 프로그램이 입력에 어떻게 반응하는지알 수 있다.

Hardware/Software Codesign

임베디드 시스템이 다양화 되면서 기존에 비해 소프트웨어가 차지하는 비중이 높아지고 있다. 임베디드 시스템을 설계하는 기존의 방법론은 하드웨어와 소프트웨어가 담당할 부분을 미리 결정하고 설계하는 것이다. 구현할 전체 시스템에 대한 완전한 이해를 가지고 각 부분이 하드웨어, 또는 소프트웨어로 구현될 것을 미리 결정한 다음 전체 시스템 디자인에 들어가는 것이다. 이 방법론은 시스템에 변경 사항이 있을 시에 하드웨어와 소프트웨어로 구현 될 요소들이 이미 결정되어 있기 때문에 소요되는 비용 및 부담이 크다. 또한 시스템이 구현되기 전에 전체 시스템에 대한 성능 및 오류 검증을 하기 힘들다. 이런 문제점들을 해결하기 위해 동시설계 방법론이 연구되고 있다. 동시설계 방법론은 기존의 방법론과 달리 하드웨어와 소프트웨어가 될 부분을 미리 정하지 않고 하나의 표현으로 설계하며, 이에 대해 Formal Verification을 수행하여 전체 시스템이 요구되는 property를 만족하는지 검증할 수 있고, 시뮬레이션을 통한 성능을 평가에 의해 최적화된 파티셔닝을 수행한다. 우리의 연구에서는 전체 시스템을 Esterel 언어와 C 언어로 표현하고 있으며, 이러한 방법론으로 임베디드 시스템을 설계하고 검증할 수 있는 Eclipse 기반의 도구를 개발하는 것을 목표로 한다.

프로그램 도용 방지

프로그램 도용 방지를 위해 code obfuscation과 소프트웨어 DNA라는 두 가지 기술을 연구한다. 코드 난독화(code obfuscation)란 프로그램 변환의 일종으로 코드를 읽기 어렵게 함을 통해 역공학(reverse engineering)을 통한 공격을 막기 위한 목적을 가지고 있다. 자바나 닷넷과 같이 중간 언어를 통해 실행하는 시스템에서는 몇 년 전부터 코드 난독화를 통하여 프로그램을 보호하고 있다. 바이너리 코드 난독화는 윈도우 실행 파일(Windows PE Executable)과 같은 기계어 실행 파일의 난독화를 방지하기 위한 방법이다. 이 방법은 악성 코드 제작자들이 안티바이러스와 같은 악성 코드 탐지 프로그램에 발견되지 않기 위해서 사용해 온 방법을 포함한다. 현재 연구하는 분야는 바이너리 코드에 대한 역공학을 방지하기 위한 난독화 방법이다. 바이너리 코드 난독화는 바이너리 코드에 대한 분석 기술과 연관이 크다. 바이너리 코드 분석 기술은 소스 코드를 확인할 수 없는 프로그램의 안정성 및 취약점을 검증하기 위하여 필수적인 기술이다. 이 연구는 바이너리 코드에서 링크 과정의 전단계인 자료 흐름 그래프(CFG)를 찾아내고 CFG를 이용하여 프로그램의 특성을 검증하는 방법을 찾아내는 것을 목표로 한다. 소프트웨어 DNA 분석은 도용된 프로그램을 찾는 연구이며, 소프트웨어 도용 탐지를 목적으로 한다. 생물의 DNA처럼 각 프로그램마다 내제된 고유한 특성인 소프트웨어 DNA를 정의하고, 두 프로그램의 DNA를 추출하여 비교한 후 같다면 이는 같은 프로그램으로 볼 수 있다. 즉 프로그램의 고유한 성질인 DNA를 정의하여 프로그램들의 유사도를 측정한다.

Program Analysis

프로그램 분석이란 Java 나 C 같이 프로그래밍 언어로 쓰여진 프로그램을 수행하기 전에 미리 분석해서, 프로그램 수행시 일어날 수 있는 다양한 오류를 미리 예측하고 검증하는 엄밀한 기법이다. 예를 들면, array-bound check 분석을 통과한 프로그램은 프로그램 수행중에 array 바운드를 넘어가는 일이 절대 일어나지 않는다. 프로그램 분석 연구의 목표는 크게 두 가지이다. 첫째는 엄밀하고 실용가능한 새로운 프로그램 분석 기법을 고안하는 것이고, 둘째는 제안된 분석 기법을 바탕으로 프로그램 오류를 미리 찾아내는 프로그램 검증 도구를 구현하는 것이다. 프로그램 분석 분야의 구체적인 연구 분야로 포인터 분석, 버퍼 오버플로우 감지, 리소스 사용 규약 검증 등이 있다. 이 밖에 PL 연구실에서 수행되는 모든 연구의 근간을 이루는 기초 이론들을 다룬다.