프로그래밍언어논문지 제21권 제1호 (2007년 4월)

목차: [.PDF 471KB] 연구논문 자바 메모리 모델을 이용한 SAT 기반 멀티 스레드 자바 소프트웨어 검증 이태훈, 권기현 (경기대학교) 가상기계를 위한 네이티브 인터페이스 정의 언어 박지우 (동국대학교); 이창환 (링크젠); 오세만 (동국대학교) CAM(Copy-Add-Move)을 이용한 바이너리 패치 방법 이민재, 한경숙 (한국산업기술대학교); 우덕균 (한국전자통신연구원) 웹 응용 프로그램의 보안 취약성 분석 김영민, 안준선 (한국항공대학교)

본문

자바 메모리 모델을 이용한 SAT 기반 멀티 스레드 자바 소프트웨어 검증 [.PDF 456KB]

• 저자: 이태훈, 권기현 (경기대학교)
• 쪽: 1-10
• 요약:
  최신의 컴파일러는 프로그램의 실행 속도를 높이기 위해서 최적화 작업을 수행한다. 최적화 작업중에 프로그램의 구문의 실행 순서가 바뀔수 있다. 단일 스레드 소프트웨어에서는 구문의 재배치가 결과에 영향을 주지 않지만 멀티 스레드 소프트웨어에서는 구문의 재배치로 인해서 예상하지 못한 결과값이 나올 수 있다. 이런 점은 멀티 스레드 소프트웨어의 오류를 찾기 힘들게 한다. 자바 메모리 모델에ㅅ는 구문의 재배치를 고려하여 멀티 스레드 소프트웨어의 가능한 실행 과정을 정형 명세 하였다. 하지만 현재 나와있는 대부분의 멀티스레드 소프트웨어 검증 도구는 메모리모델에 대해서 고려를 하고 있지 못하다. 본 논문에서는 자바 메모리 모델을 이용하여 소프트웨어의 제약 사항 위반 검사 기법을 설명한다. 이를 이용하여 기존 소프트웨어 검증 도구인 JavaPathFinder에서 오류가 없다고한 소프트웨어의 오류를 찾아내었다.

가상기계를 위한 네이티브 인터페이스 정의 언어 [.PDF 383KB | .HWP 547KB]

• 저자: 박지우 (동국대학교); 이창환 (링크젠); 오세만 (동국대학교)
• 쪽: 11-21
• 요약:
  가상기계란 하드웨어로 이루어진 물리적인 시스템과는 달리 소프트웨어로 제작되어 논리적인 시스템 구성을 갖는 개념적인 컴퓨터이다. 가상기계에서 실행되는 프로그램은 플랫폼 독립적인 장점이 있지만, 가상기계에서 제공하지 않는 플랫폼 의존적인 기능은 사용할 수 없다. 이와 같은 문제를 해결하기 위해서 가상기계 환경에서는 일반적으로 네이티브 인터페이스를 제공한다. 제공된 네이티브 인터페이스를 통해 구현된 네이티브 함수를 가상기계 환경에서 사용하기 위해서는 네이티브 함수를 위한 정보가 필요하다. 본 논문에서는 네이티브 함수를 위한 정보를 용이하게 생성하기 위해 네이티브 인터페이스 정의 언어와 언어로부터 네이티브 인터페이스 사용에 필요한 정보를 생성하는 컴파일러를 설계 및 구현한다. 구현된 컴파일러의 결과인 네이티브 함수를 위한 정보는 가상기계 환경의 내부 표현으로 생성되며, 생성된 정보는 임베디드 시스템을 위한 가상기계인 EVM에 적용하여 검증한다. 제안된 언어와 컴파일러를 통해 가상기계 개발자가 네이티브 함수를 위한 정보를 직접 작성하는 부담을 줄이고 편의성을 제공할 수 있다.

CAM(Copy-Add-Move)을 이용한 바이너리 패치 방법 [.PDF 343KB | .HWP 277KB]

• 저자: 이민재, 한경숙 (한국산업기술대학교); 우덕균 (한국전자통신연구원)
• 쪽: 23-37
• 요약:
  대개의 많은 소프트웨어는 프로그램의 안정성과 기능 향상을 위해서 소프트웨어 업데이트를 사용한다. 초기의 소프트웨어 업데이트는 변경된 파일을 교체하는 방법으로 이루어졌으나 최근에는 업데이트를 제공하는 서버의 네트워크 트래픽과 저장 공간의 부담을 줄이기 위해서 구 버전과 신 버전간의 차이점을 추출한 델타 패키지를 이용하는 방식을 사용한다. 본 논문은 파일의 바이너리를 일종의 문자열로 보고 문자열 매칭 알고리즘을 이용하여 차이점을 추출하는 바이너리 패치 도구를 제안한다. 가장 길고 최대한 근접한 매치를 찾기 위해 zdelta와 같이 윈도우에 존재하는 모든 바이너리 패턴을 인덱싱하는 방식을 이용하였다. vcdiff와 zdelta에서 사용한 복사 기반 방식을 확장하여 1:1 매치되는 구간에 있어서 Move의 개념을 추가한 CAM(Copy-Add-Move) 방식을 새로 도입하고, 기존의 vcdiff에서 사용한 1바이트 델타 명령 체계 세분화를 통해 델타 명령이 사용하는 인수를 줄임으로써 압축률을 향상시켰다. 델타 압축의 최악 경우(worst case)는 두 바이너리 버전 간의 차이가 큰 경우 발생한다는 것을 실험을 통해 밝히고 이와 같은 경우에는 오히려 델타 압축을 수행하는 것보다 데이터 압축을 수행하는 것이 더 좋은 압축률을 얻을 수 있다. 따라서 그 대안으로 wdiff는 RAR32를 이용하여 대상 파일을 데이터 압축하는 정책을 사용하였다.

웹 응용 프로그램의 보안 취약성 분석 [.PDF 414KB | .HWP 182KB]

• 저자: 김영민, 안준선 (한국항공대학교)
• 쪽: 39-48
• 요약:
  현재 대부분의 웹 사이트 구축은 웹 응용 프로그램(web application program)이 적절한 웹 페이지를 생성하여 전송하는 형태인 동적 웹페이지(dynamic web pages)를 사용하고 있다. 이러한 웹 환경에서 전통적인 웹 서버 자체에 대한 공격 외에도 웹 응용 프로그램이 가지고 있는 취약점을 대상으로 한 공격이 증가하고 있다. 본 논문에서는 웹 사이트에 대한 공격을 사전에 방지하기 위하여 웹 응용 프로그램에 존재하는 취약점을 미리 찾아내기 위하여 요약 해석에 기반 한 프로그램 내의 안전한 자료 흐름(secure information flow) 분석을 제시하였다. 개발한 요약 해석은 문자열 자료값들의 멱집합(powerset)을 근사하는 요약된 자료 공간 내에서 프로그램을 수행함으로써, PHP 프로그램의 특징인 복잡한 가변 변수(variable variables)와 문자열을 첨자(index)로 사용하는 배열 등을 적절히 처리할 수 있다. 주어진 분석을 통하여 프로그램 내의 민감한 부분에서 사용되는 값에 외부의 입력이 영향을 미칠 수 있는지 여부와 사용되는 문자열 값의 종류를 알아낼 수 있다.