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

편집사: [.PDF 91KB]

연구논문

• 문장 결합을 통한 소프트웨어 테스트 데이터 생성
  곽동규, 조용운, 김영철, 유재우
• 컴퓨터 보안정책을 위한 객체-기반 시각 명세 언어 설계 및 구현
  강철범, 김성욱
• Petri Net을 사용한 임베디드 시스템의 스케줄링
  이태용
• 고급언어 기반의 대규모 네트워크 보안 관리 시스템 개발
  김장하, 이강희, 김상욱
• 술어 추상화 기반의 자바 프로그램 모델 체킹
  이태훈, 권기현
• 동적 바인딩을 이용한 공유 데이터 구조
  배경호, 김태완, 장천현

본문

문장 결합을 통한 소프트웨어 테스트 데이터 생성 [.PDF 142KB]

• 저자: 곽동규, 조용운, 김영철, 유재우
• 요약:
  테스트 데이터 생성 단계는 소프트웨어 테스팅 과정에 있어 매우 중요하며 많은 노력을 요구한다. 본 논문에서는 pascal이나 C와 같은 절차적 프로그래밍 언어에 있어서 실행의 단위가 되는 문장들간의 결합구조 정보를 통해 테스트 데이터를 자동 생성하는 방법을 제안한다. 이를 위해 본 논문에서는 프로그램의 문장을 집합으로 정의하고 집합의 원소간에 연산을 통해 프로그램 코드의 구조 정보를 추상 구문 트리(Abstract Syntax Tree)로 표현한다. 또한, 본 논문은 생성된 추상 구문 트리의 구조 정보에 따라 사용자가 입력한 실행 경로를 XML 파일로 표현하여 실행 경로에 영향을 주는 조건식을 추출하고 연산하기 위한 알고리즘을 제안한다. 따라서 제안하는 테스트 데이터 자동 생성 방법은 기존의 테스팅 적합성 기준을 판별하는 과정을 필요로 하지 않는다. 또한, 실행 경로 정보에 대한 XML 파일을 통해 조건식의 추출과 연산과정을 자동화 할 수 있는 가능성을 제시하여 소프트웨어 테스트 데이터 생성에 관련된 자동화 도구 개발에 기여할 수 있을 것으로 기대된다.

컴퓨터 보안정책을 위한 객체-기반 시각 명세 언어 설계 및 구현 [.PDF 186KB]

• 저자: 강철범, 김성욱
• 요약:
  컴퓨터 시스템 및 네트워크를 보호하기 위하여 다양한 보안정책 언어들이 개발되었다. 이런 보안정책들은 동일한 의미를 가지더라도 적용 도메인과 추상화 정도에 따라 표현 방법이 다르며 통합 관리하기 어렵다. 기존의 보안정책 명세 언어는 호스트 혹은 네트워크 환경 도메인에 종속적이며 인가, 의무, 제한, 위임, 복합과 같은 보안정책의 기본 유형들을 모두 표현하기 어렵고 여러 객체 간 또는 객체 내부에서 발생하는 상황을 표현하는데 한계가 있다. 보안정책 명세 언어를 실제 시스템에 적용하는 기법에서도 복잡하고, 관리하기 힘들다. 다양한 도메인에 적용되는 보안정책을 효율적으로 정의하고 관리하기 위하여 이를 독립적으로 표현하는 일반적인 기술 언어에 대한 정의가 필요하며, 보안정책을 명세 언어의 형태로 표현함으로써 적용되는 도메인이나 침입의 형태에 상관없이 일관적인 방법으로 보안정책을 기술해야 한다. 또한 보안정책의 재사용, 일괄적인 관리가 가능하고 명확한 의미전달 및 정형성이 보장되어야 하며 보안정책을 실제 시스템에 적용하기 위한 보안정책 적용 시스템이 필요하다.
  본 논문에서는 객체 기반의 보안정책 명세 언어를 제시한다. 보안정책의 조건과 행위를 객체의 상태, 객체간의 관계로 표현하므로 다양하고 광범위한 보안정책의 표현이 가능하다. 그래픽 기반의 표현 기법을 사용함으로써 표현이 간단하고 이해하기 쉬운 특징을 가진다. 객체-기반 시각 보안정책 명세 언어는 적용하려는 시스템이 객체-지향 방법으로 모델링 된 것을 전제로 하므로 시스템 객체 에이전트와 실제 적용 시스템을 설계 및 구현하였다.

Petri Net을 사용한 임베디드 시스템의 스케줄링 [.PDF 123KB]

• 저자: 이태용
• 요약:
  Embedded systems specification usually has both data computation and control structures. Control structure can be two types. One is data dependent control and the other is real time control. The first one can be easily solved because it is involved with only one task and its behavior is very obvious. The problem is the second case. We must use some sophisticated techniques to resolve concurrent behavior of tasks.
  To solve the second problem, these tasks require to be scheduled on a shared resource such as processor and memory. This scheduling is mainly based on the system specification. To simulate dynamic behaviors of system, it is very difficult to predict these behaviors because these behaviors have to be determined at compile time and decisions have to be made at run time. In other words, scheduling must be efficiently made while pleasing real time constraints and using the processor and memory resources as efficiently as possible. Therefore, Quasi-static scheduling algorithm is used to solve these problems.

고급언어 기반의 대규모 네트워크 보안 관리 시스템 개발 [.PDF 373KB]

• 저자: 김장하, 이강희, 김상욱
• 요약:
  대규모 네트워크에서는 보안 관리를 위한 여러 가지 기법이 적용되고 있다. 네트워크를 통해 전파되는 바이러스와 인터넷 윔의 경우 자동화된 공격 기법을 포함하여 단시간에 수많은 호스트를 감염시킨다. 네트워크의 링크 계층을 지원하기 위한 여러 가지 장비는 이러한 문제점을 해결하기 위한 보안 관리 기능을 제공하고 있다. 그러나 최근 사용되는 대부분의 네트워크 장비가 접근 제어와 같은 보안 기능을 포함하고 있지만 위급한 상황에 이러한 기능을 적절히 활용하는 것은 쉽지 않다. 2002년 초에 발생한 Slammer웜은 대규모 네트워크를 통해 빠르게 전파되었지만 관리자의 보안 기능 활성화 이전에 전체 네트워크로 확산된 대표적인 예이다. 네트워크를 구성하고 있는 장비들이 다양하고 그것들의 보안 설정이 서로 상이하기 때문에 긴급 상황에서 일괄적인 관리가 어렵다는 단점 때문이다.
  이러한 문제점을 해결하기 위해 본 논문에서는 대규모 네트워크를 구성하는 다양한 하부 노드들의 보안 설정을 위한 공통적인 속성을 분석하고 이러한 정보를 추상적으로 기술할 수 있는 고급언어를 제안한다. 그리고 중간단계의 자료구조를 설계하여 고급 언어와 실제 하부 노드에 적용될 명령어의 변환을 돕는다. 전체 관리 시스템은 고급언어 컴파일러가 포함된 관리자 인터페이스, 네트워크 도메인을 관리하기 위한 도메인 관리 서버와 하부 노드 인터프리터 에이전트로 구성된다. 관리자가 고급언어로 기술한 보안 정책은 컴파일러에 의해 중간단계의 자료구조로 변환되고 도메인 관리 서버에서 연산되고 인터프리터에 의해 하부 노드에 최종 적용된다. 기존의 네트워크 보안 관리를 위해 서로 다른 하부 노드를 순차적으로 설정하였던 것에 비해 본 논문에서 제안하는 보안 관리 시스템은 고급 언어로 기술된 하나의 정책으로 전체 시스템의 관리를 받고 있는 하부노드들의 보안 설정을 일괄적으로 제어할 수 있다.

술어 추상화 기반의 자바 프로그램 모델 체킹 [.PDF 179KB]

• 저자: 이태훈, 권기현
• 요약:
  모델 체킹은 오류를 찾아내기 위한 검증 기술중의 하나로서 하드웨어 검증, 소프트웨어 검증, 프로토콜 검증등에 적용되어 왔다. 현재 많은 연구 그룹들이 모델 체킹을 이용해서 프로그램 소스 코드를 직접 검증하려는 시도를 진행중이다. 유한 상태만을 다루는 현재의 모델 체킹 기술로는 프로그램 소스 코드를 직접 검증하기 힘들다. 왜냐하면 프로그램은 무한 상태를 갖고 있기 때문이다. 이를 해결하기 위한 기술 중에 하나가 술어 추상화이다. 술어 추상화를 통해서 무한 상태 공간을 유한 상태 공간으로 축소할 수 있다. 현재까지 개발된 술어 추상화 기반의 모델 체킹 도구로는 SLAM, BLAST, MAGIC 등이 있다. 이들 도구는 C 언어와 같은 절차적 프로그램의 검증만을 지원하는 반면에, 자바 언어와 같은 객체지향 프로그램의 검증은 지원하지 않는다. 본 논문에서는 술어 추상화를 자바 프로그램에 적용하여 추상화된 이진 프로그램을 구한 후, SMV를 이용해서 이진 프로그램을 검증하는 방법을 제안한다.

동적 바인딩을 이용한 공유 데이터 구조 [.PDF 187KB]

• 저자: 배경호, 김태완, 장천현
• 요약:
  일반적으로 정적 바인딩에 의해 데이터형이 결정되는 소프트웨어는 프로그램을 작성 시에 데이터의 형식을 정의해 컴파일 하는 과정에 데이터의 형식을 분석한다. 이와 같은 경우 실행 시간에 데이터의 형식 및 구조가 변경되어야 한다면 실행을 멈추고 해당 소프트웨어의 원시프로그램을 수정해야 한다. 그리고 다수의 소프트웨어들이 데이터 구조 및 값을 공유해야 한다면 소프트웨어간의 통신 기법을 이용해서 데이터를 주고 받아야 한다. 그러나 이 방법에도 데이터 구조 및 내용 변경 시에는 원시 프로그램을 수정해야 하는 문제점을 가지고 있다.
  이에 본 논문에서는 운영체제에서 지원하는 공유 메모리를 이용하여, 공유 데이터 구조를 탑재하고 동적 바인딩 기술을 이용하여 문제점을 해결하였다. 데이터의 형식, 변수명이나 값을 공유메모리에 저장하고 시스템 내의 모든 응용 소프트웨어들이 공유할 수 있도록 한 기법이다. 응용 소프트웨어는 실행 중에 필요한 데이터의 값이나 형식을 공유 메모리로부터 읽어온다. 그리고 시스템에서 사용하는 데이터 형식이 변경되더라도 공유 메모리내의 해당 데이터의 형식만 변경하면 되므로 응용 소프트웨어의 실행을 멈추지 않아도 된다. 또한 시스템 내에서 사용하는 모든 데이터를 응용 소프트웨어들이 공유함으로써 응용 소프트웨어간의 데이터를 동기화하기 위하여 통신을 하지 않아도 되어서 응용 소프트웨어 개발자의 개발 작업은 더욱 쉬워진다.