프로그래밍언어논문지 제17권 제3호 (2003년)

논문

• 속성 분할을 이요한 릴레이 모델 체킹
  이태훈, 권기현
• 비트 연산을 이용한 향상된 연산 난독화 기법
  박희완, 최석우, 한태숙
• Topology String을 이용한 단백질 구조 비교 방법
  김진홍, 안건태, 이수현, 이명준
• 다중 메모리 구조를 위한 효울적인 자료 할당 기법
  조정훈, 백윤흥, 최준식
• 센서 네트워크 어플리케이션 개발을 위한 NesC
  이민구, 강정훈, 유준재
• 마크업 문서의 대수적 분석에 의한 분할과 변환
  곽동규, 최종명, 유재우
• 집합 제한식을 이용한 프로시저-내 정보흐름 안전성 분석
  임흥태, 신승철, 도경구
• 정보 흐름에 대한 SSA기반 분석
  최성권, 신승철, 도경구

본문

속성 분할을 이요한 릴레이 모델 체킹 [.PDF 883KB]

• 저자: 이태훈, 권기현
• 요약:
  모델 체킹은 유한 상태 모델과 시제 논리식을 받아서 모델과 논리식과의 만족성 관계를 결정한다. 만족성 관계를 판정하기 위해서 모델이 갖는 상태 공간을 모두 검사하기 때문에, 모델의 크기가 커질수록 고려해야 하는 상태의 수도 지수적으로 증가한다. 이를 상태 폭발 문제라고 한다. 이를 해결하기 위한 방법으로 추상화, 반순서 등의 여러 가지 방법이 제안되었다. 대부분의 방법들은 모델의 구조를 이용하여 상태 공간을 축소하고 있다. 이와는 달리, 본 논문에서는 속성 분할을 이용한 릴레이 모델 체킹을 제안하고, 이를 통해서 상태 폭발 문제를 해결한다. 제안된 릴레이 모델 체킹의 유용성을 확인하기 위해서 푸쉬 푸쉬 및 소코반 게임 풀이에 적용해 본 결과, 추상화 기법으로 풀지 못했던 푸쉬 푸쉬 50판과 A* 알고리즘으로 풀지 못했던 소코반 51판등을 제안된 릴레이 모델 체킹으로 풀 수 있었다

비트 연산을 이용한 향상된 연산 난독화 기법 [.PDF 917KB]

• 저자: 박희완, 최석우, 한태숙
• 요약:
  자바 프로그램은 클래스 파일에 소스 코드의 심볼릭 정보를 그대로 유지하고 있어서 클래스 파일로부터 원본과 거의 동일한 소스 코드를 얻어낼 수 있다. 이 문제에 대처하기 위해서 프로그램의 기능을 그대로 유지하고, 소스 코드를 해석하기 어려운 형태로 변환하는 난독화 방법이 제안되었다. 지금까지 연구된 난독화 기법들은 레이아웃을 위주로 변환하기 때문에 프로그램에 포함된 알고리즘 구조 자체를 변경시키지는 못한다. 따라서 중요한 데이터나 알고리즘을 보호하려고 할 때 난독화 도구를 적용하는 것은 무의미했다. 본 논문에서는 관련연구로서 선형함수를 사용하여 데이터와 그 연산을 보호하는 난독화 기법을 소개하고, 선형 함수 난독화 기법의 단점인 실행 속도 저하와 클래스 크기 증가에 대한 단점을 보완한 비트 연산자를 사용한 연산 난독화 기법을 새롭게 제안했다. 비트 연산자를 이용해서 연산을 난독화하면 프로그램의 실행 성능을 유지하면서 데이터와 연산들에 대해서 복잡한 난독화를 수행할 수 있다. 또한 후처리 과정으로서 연산의 최적화 과정을 제안하여 클래스 크기 증가와 프로그램 실행 속도 저하의 단점을 보완할 수 있게 하였다.

Topology String을 이용한 단백질 구조 비교 방법 [.PDF 666KB]

• 저자: 김진홍, 안건태, 이수현, 이명준
• 요약:
  단백질 구조 비교 방법은 단백질 구조의 유사성을 측정하는 과정에서 많은 시간을 요구할 뿐만 아니라 PDB 데이터베이스에 저장된 데이터가 증가함에 따라 보다 많은 단백질과 비교가 요구된다. 따라서 대용량의 단백질 구조 데이터베이스를 대상으로 효율적으로 단백질의 유사 부분구조를 찾을 수 있는 방법이 필요하다. 본 논문에서는 단백질 구조 비교를 보다 빠르고 효과적으로 수행하기 위하여 단백질 이차구조가 가지는 공간상의 정보를 내포한 Topology String을 생성하고 이를 이용하여 대용량의 단백질 구조 데이터베이스에서 유사성이 높은 단백질 구조를 필터링하는 방법에 대하여 기술한다. Topology String은 단백질 이차구조를 하나의 문자로 기술하여 아미노산 순서와 위상학적인(공간적인) 정보를 바탕으로 단백질 구조를 표현하여, 단백질 이차구조를 이용하여 구조 비교를 수행하기 이전에 유사성이 높은 단백질 구조를 신속하게 찾아내는데 효과적으로 적용될 수 있다.

다중 메모리 구조를 위한 효울적인 자료 할당 기법 [.PDF 1337KB]

• 저자: 조정훈, 백윤흥, 최준식
• 요약:
  현존하는 대부분의 DSP들은 다중 메모리 뱅크를 지원하는 하버드 구조를 가진다. 따라서 하나의 명령어를 사용하여 메모리에서 여러 개의 데이터 워드를 동시에 읽어 들이는 것이 가능하다. 뿐만 아니라, 이러한 DSP들은 여러 개의 레지스터 파일이 각 기능(functional) 유닛에 분산되어 있는 비정규적인 구조로 되어 있다. 이러한 다중 메모리 뱅크 구조를 효율적으로 사용하기 위해 각 메모리 뱅크에 데이터를 효율적으로 할당하려는 노력이 여럿 선행되었지만, 대부분이 정규적인 구조를 가정한 연구였으며, 그 결과, 비정규적인 구조를 가지는 DSP에 대해서는 최적의 코드를 생성하지 못하는 경우가 종종 발생하였다. 본 논문에서는 다중 메모리 뱅크 구조에서 각 메모리 뱅크에 데이터를 효율적으로 할당하는 새로운 알고리듬을 설명한다. 기존의 연구는 메모리 뱅크 할당을 다른 코드 생성 알고리듬과 통합하여(tightly coupled) 수행하였으나, 우리의 메모리 뱅크 할당 알고리듬은 독립된 컴파일 단계에서 동작하도록 설계되었다(Decoupled). 실험 결과, 우리의 독립된(decoupled) 메모리 할당 알고리듬은 기존의 알고리듬과 비슷한 품질의 코드를 생성하면서도 컴파일 시간을 극적으로 향상시킨 것을 알 수 있었다.

센서 네트워크 어플리케이션 개발을 위한 NesC [.PDF 501KB]

• 저자: 이민구, 강정훈, 유준재
• 요약:
  최근 유비쿼터스(Ubiquitous)라는 단어가 다양한 과학 기술 분야에서 많이 사용되어지고 있다. 그리고 조만간 도래하게 될 유비쿼터스 컴퓨팅 & 네트워킹 시대의 핵심 기술로 떠오르고 있는 센서 네트워크 분야에서 TinyOS가 현재 적합한 OS로 촉망 받고 있으며, 전 세계 100여개 이상의 센서 네트워크 연구 그룹들에 의해서 채택되어 이용되고 있다. 이러한 TinyOS에서 구현하고자 하는 개념들을 지원하기 위해 고안되어진 NesC 프로그래밍 언어의 전반적인 특성에 대한 소개를 본 논문을 통해서 제공하고자한다. 본 논문은 이를 위해 Mote, TinyOS, NesC에 대한 각각의 기본적인 개념들에 대한 접근을 하였고, 예제로서 사람의 위치를 Tracking 할 수 있는 어플리케이션을 NesC를 이용해 직접 구현하였으며, Mote의 정상적인 추적이 가능함을 실험적으로 살펴보았다. 또한 앞으로 더욱 규모가 큰 시스템들에 적용하여 적합하도록 만들기 위해 NesC가 나아가야 할 발전 방향에 대해서 제시하였다.

마크업 문서의 대수적 분석에 의한 분할과 변환 [.PDF 644KB]

• 저자: 곽동규, 최종명, 유재우
• 요약:
  현재 많은 응용프로그램들이 XML로 표현된 정보를 이용하여 서비스하고 있다. 특정 응용프로그램을 위해 작성된 XML 문서를 다른 응용프로그램에서 사용하기 위해서는 적절한 변환이 필요하다. 본 논문은 대수학적 방법을 이용해서 XML 문서를 분할하고, 변환하는 방법을 소개한다. 이 방법을 사용하기 위해서 논문에서는 XML 문서의 태그간의 관계를 연산으로 정의하고, 연산의 특성을 이용해서 문서의 경계를 구분하는 방법과 경계가 구분된 문서를 분할하는 방법을 제시한다. 또한, 분할된 문서의 태그들을 그룹핑해서 m:n으로 변환이 가능한 단위를 정의하고, 이 단위를 이용해서 XML 문서를 변환하는 방법을 소개한다. 대수학적 방법을 이용한 문서의 변환은 일반적인 XML 문서에 적용할 수 있고, 경계를 구분하여 정보의 이해가 용이한 문서를 생성하는 장점을 가지고 있다. 논문에서는 문서 변환의 예로 HTML 문서를 VoiceXML로 변환하는 HTMLtoVoiceXML을 소개한다.

집합 제한식을 이용한 프로시저-내 정보흐름 안전성 분석 [.PDF 646KB]

• 저자: 임흥태, 신승철, 도경구
• 요약:
  이 논문은 명령형 프로그램의 프로시저 내부에 대한 정보흐름의 안전성을 집합 제한식 분석법을 사용하여 예측하는 방법을 제시한다. 지금까지 제안된 분석 기법은 정보흐름이 안전한 프로그램을 안전하지 않다고 보수적으로 판정한다는 점에서 정밀도가 떨어지는 경우가 많이 있다. 본 논문에서는 이전의 타입시스템을 이용한 접근 방법보다는 분석 결과가 더 정밀한 새로운 분석법을 제안한다

정보 흐름에 대한 SSA기반 분석 [.PDF 586KB]

• 저자: 최성권, 신승철, 도경구
• 요약:
  정보 흐름 분석은 주어진 프로그램에서 보안등급이 서로 다른 변수들 사이의 정보 흐름이 안전한가를 정적으로 검사한다. 부분타입을 포함하는 타입시스템을 이용하여 프로그램의 정보 흐름을 분석하면 정보 누출을 손쉽게 발견할 수 있지만 정보 누출이 전후 방향으로 복구되는 상황을 인지하지 못하기 때문에 너무 많은 안전한 프로그램을 거절하는 단점이 있다. 이것은 타입 추론의 결과가 프로그램의 흐름에 민감하지 않기 때문인데, 본 논문에서는 주어진 프로그램을 SSA 형태(static single assignment form)로 변환한 후에 타입시스템을 적용함으로써 이 문제를 해결하는 방법을 설명한다. 본 논문의 방법은 정보 누출의 복구되는 경우에도 정확하게 분석하기 때문에 요약 해석법과 같은 정도의 정밀도를 갖는다.