프로그래밍언어논문지 제19권 제2호 (2005년 11월)

편집사: [.HWP 16KB] 연구논문 C 프로그램을 위한 효율적인 버퍼 오버런 분석기의 개발 김유일, 전진성, 한환수 (KAIST) 요약해석기 AiracV 신재호, 김재황, 오학주, 정영범, 이광근 (서울대학교) SMT 멀티 프로세서 시스템을 위한 적응형 실행 기법 정창희 (한국전자통신연구원); 이재진 (서울대학교) 자바프로그램의 보안 정보 흐름 분석 박숙영, 이상규 (숙명여자대학교) 간단한 자바프로그램을 위한 CTL 모델 체킹 이정림, 이태훈, 권기현 (경기대학교) fFSM 모델의 정형 분석 박사천, 권기현 (경기대학교) 시스템 종속 그래프에 기반한 프로그램 자르개의 구현 노상훈, 신승철 (동양대학교)

본문

C 프로그램을 위한 효율적인 버퍼 오버런 분석기의 개발 [.PDF 347KB]

• 저자: 김유일, 전진성, 한환수 (KAIST)
• 쪽: 1-9
• 요약:
  C 언어로 작성된 소스 코드를 분석하여 버퍼 오버런 취약점을 실행 전에 발견하는 효율적인 정적 분석 도구를 개발하는 과정에서, 속도와 정확도라는 두 가지 상충하는 요구 사항을 모두 만족시키기 위한 분석기의 구조를 제안하고, 현재까지의 실험 결과를 소개한다. 제안하는 분석기의 구조는 포인터 분석과 값 분석을 별도의 단계로 구분하여 정확도를 다르게 설정할 수 있는 구조로, 리눅스 커널 소스에 대해서는 부정확한 포인터 분석과 정확한 값 분석의 조합이 정확한 포인터 분석과 정확한 값 분석의 조합에 비해 빠른 속도로 수행되면서도 정확도 면에서 비슷하다는 실험 결과를 통해 이러한 구조의 가능성을 보인다.

요약해석기 AiracV [.PDF 344KB]

• 저자: 신재호, 김재황, 오학주, 정영범, 이광근 (서울대학교)
• 쪽: 11-17
• 요약:
  AiracV는 요약해석틀에 기반하여 C 프로그램의 버퍼 오버런을 안전하게 찾는 정적 프로그램 분석기이다. 우리가 Airac으로부터 얻은 경험을 바탕으로 AiracV는 한층 개선된 설계를 바탕으로 구현하고 있다. AiracV가 기존의 Airac에 비해서 달라진 점을 살펴 보고, 현재 우리가 설계의 일부를 구현한 AiracV의 첫 판의 성능을 Airac과 비교하여 본다.

SMT 멀티 프로세서 시스템을 위한 적응형 실행 기법 [.HWP 598KB]

• 저자: 정창희 (한국전자통신연구원); 이재진 (서울대학교)
• 쪽: 19-35
• 요약:
  Simultaneous multithreading(SMT) 멀티 프로세서에서 루프를 병렬 수행하기 위해서 사용 가능한 모든 쓰레드들을 사용하는 것이 항상 좋은 성능을 가져오는 것은 아니다. 이는 쓰레드들 사이의 간섭(interference)과 병렬 수행의 오버헤드가 존재하기 때문이며, SMT 멀티 프로세서의 성능을 극대화하기 위해서는 최적의 쓰레드 개수를 찾는 것이 매우 중요하다. 본 논문은 SMT 멀티 프로세서를 위한 최적의 수행 모드를 찾아내는 적응형 실행 기법을 제시한다. 컴파일러 전처리기(pre프로세서)는 수행 중에 루프를 실행하는 최적의 쓰레드 개수를 자동으로 결정하는 코드를 생성하며, 이러한 결정은 실행 중에 얻어지는 피드백에 근거한다. 실험을 위해 8개의 논리적인 프로세서를 지원하는 4개의 Intel Hyper-Threading Xeon 프로세서들로 구성된 SMP 시스템을 사용했으며, 본 논문이 제시하는 방법을 10개의 대표적인 과학 수치계산 병렬 벤치마크 프로그램에 적용한 결과, 생성된 코드는 4, 8 개의 논리적인 프로세서에서 수행되는 원래의 코드보다 각각 평균적으로 2배, 18배 빠른 성능을 보였다.

자바프로그램의 보안 정보 흐름 분석 [.HWP 664KB]

• 저자: 박숙영, 이상규 (숙명여자대학교)
• 쪽: 37-45
• 요약:
  자바 언어의 사용에 있어서 안전한 데이터의 관리는 중요한 요소가 된다. 자바 바이트코드 검증기(Java bytecode Verifier)나 클래스 로더(class loader), 보안관리자(Security Manager)를 통한 자바언어 자체의 보안장치로서는 플랫폼 독립을 지원하는 자바언어의 특성을 살리면서 동시에 민감한 정보의 유출을 방지하는 역할을 수행하기에는 부족한 점이 있다. 이러한 점을 고려하여 안전한 정보 흐름에 관한 연구들이 수행되어 왔다. 그중 자바 가상 기계의 바이트코드 검증기의 타입 검사기능을 이용한 방법이 연구되어 왔는데 본 논문에서는 구문분석정보를 그래프로 나타내어 보다 효율적인 방법으로 안전한 정보 흐름을 분석하고 그 결과를 시각화 하여 시스템 관리자가 보다 편리하게 사용할 수 있는 안전한 정보 흐름 분석기를 구현하였다.

간단한 자바프로그램을 위한 CTL 모델 체킹 [.HWP 560KB]

• 저자: 이정림, 이태훈, 권기현 (경기대학교)
• 쪽: 47-66
• 요약:
  소프트웨어의 안전성과 신뢰성을 높이기 위해서는 소프트웨어에 대한 철저한 검증이 요구된다. 더군다나 임베디드 소프트웨어에서는 검증이 더욱 요구된다. 왜냐하면 임베디드 소프트웨어는 복잡한 기능을 만족해야 하며, 시간 제약 및 운용 제약과 같은 성능 조건을 만족할 뿐만 아니라 크기와 속도 면에서 최적화되어야 하기 때문이다. 본 논문에서는 간단한 자바 언어로 작성된 임베디드 소프트웨어의 기능을 검증하는 모델 체커를 구현하였다. 모델 체커는 크게 추상화 모듈과 검증 모듈로 구성된다. 추상화 모듈은 상태 폭발을 방지하기 위해서 자바 프로그램을 이진 프로그램으로 변환한다. 검증 모듈은 이진 프로그램의 제어 흐름을 분석해서 CTL(Computation Tree Logic) 모델 체킹을 수행한다. SLAM, BLAST와 같은 기존 소프트웨어 모델 체커가 API(Application Programming Interface) 이용 규칙에 대한 안전성 속성만을 검사하는데 비해서, 본 논문에서 구현된 모델 체커는 안전성 속성과 궁극성 속성 모두를 검사하는데 초점을 맞추고 있다. 또한 추상화 작업 동안에 정리 증명기 호출 횟수를 감소시킴으로서 모델 체커의 성능을 개선하였다.

fFSM 모델의 정형 분석 [.HWP 868KB]

• 저자: 박사천, 권기현 (경기대학교)
• 쪽: 67-80
• 요약:
  하드웨어와 소프트웨어를 통합 설계하는 프레임워크인 PeaCE(Ptolemy extension as a Codesign Environment)가 개발되었다. PeaCE에서 fFSM(flexible Finite State Machine)은 제어흐름을 명세하도록 풍부한 구문을 제공하는 모델이지만, 정형 의미의 부재로 인해서 명세를 정형 분석하기가 어려웠다. 본 논문에서는 fFSM에 대한 정형 의미를 정의했고, 이를 통해서 정형 분석을 수행하는 프레임워크를 개발했다. 본 논문에서 개발된 프레임워크를 통해서 데드락, 레이스 조건(race condition), 애매한 전이(ambiguous transition), 순환 전이(circular transition)등과 같이 임베디드 소프트웨어에서 발생할 수 있는 중요한 버그들을 정형적으로 분석하는 방법을 보인다.

시스템 종속 그래프에 기반한 프로그램 자르개의 구현 [.HWP 220KB]

• 저자: 노상훈, 신승철 (동양대학교)
• 쪽: 81-88
• 요약:
  프로그램 자르기(Program Slicing)는 프로그램의 이해와 디버깅 등을 돕는 매우 유용한 도구로 알려져 있고 프로그램 분석에도 이를 도입하여 효과를 배가하는 시스템이 연구되어 왔다. 우리는 시스템 종속 그래프를 이용하는 프로그램 자르개를 구현하였는데 본 논문에서는 그래프의 적절한 표현방법과 잘라낸 정보(slice info)를 취급할 때 발생한 문제를 해결하는 방법을 설명한다. 또한 구현된 자르개가 소프트웨어 보안 문제의 하나인 정보흐름 보안성 검증에서 어떻게 응용될 수 있는지를 설명한다.