모델기반의 커널 테스팅 프레임워크

김문주(Moonzoo Kim),홍신(Shin Hong) 한국정보과학회 2009 정보과학회논문지 : 소프트웨어 및 응용 Vol.36 No.7

Despite the growing need for customized operating system kernels for embedded devices, kernel development continues to suffer from insufficient reliability and high testing cost for several reasons such as the high complexity of the kernel code. To alleviate these difficulties, this study proposes the MOdel-based KERnel Testing (MOKERT) framework for detection of concurrency bugs in the kernel. MOKERT translates a given C program into a corresponding Promela model, and then tries to find a counter example with regard to a given requirement property. If found, MOKERT executes that counter example on the real kernel code to check whether the counter example is a false alarm or not. The MOKERT framework was applied to the Linux proc file system and confirmed that the bug reported in a ChangeLog actually caused a data race problem. In addition, a new data race bug in the Linux proc file system was found, which causes kernel panic. 최근 내장형 시스템이 점점 많은 분야에 사용되며, 시스템에 특화된 운영체제 커널에 대한 필요성이 커지고 있다. 하지만, 커널 개발은 코드의 복잡성 등의 이유로 말미암아 테스팅에 큰 비용이 소요됨에도 불구하고, 높은 신뢰성을 달성하기가 어려운 실정이다. 이러한 커널 개발 및 테스팅의 어려움을 극복하기 위해, 운영체제 커널의 동시성 오류 검출을 지원하는 모델 기반의 커널 테스팅 (MOKERT) 프레임워크를 제안한다. MOKERT 프레임워크는 주어진 C 프로그램을 Promela 정형 명세 모델로 변환하고 나서 Spin 모델검증기를 사용하여 검증하고, 검증반례가 생성된 경우, 이 검증반례를 실제 커널 코드에서 실행을 시켜서 진위를 확인한다. 본 연구에서는 MOKERT 프레임워크를 리눅스 proc파일시스템에 적용하여, ChangeLog에 보고된 오류가 실제로 자원경쟁문제를 일으킴을 확인하였을 뿐만 아니라, 커널 패닉을 일으키는 새로운 오류도 발견하였다.

동적 심볼릭 테스팅(Concolic 테스팅)

김문주(Moonzoo Kim),김윤호(Yunho Kim),홍신(Shin Hong) 한국정보과학회 2019 정보과학회지 Vol.37 No.4

Concolic 테스팅 도구 CROWN의 적용 가능성 및 사용성 개선 연구

김현우(Hyunwoo Kim),김윤호(Yunho Kim),김문주(Moonzoo Kim) 한국정보과학회 2018 정보과학회논문지 Vol.45 No.10

본 연구에서는 Concolic 테스팅 기법의 적용 가능성 및 사용성을 개선하기 위한 CROWN(Concolic testing for Real-wOrld software aNalysis) 도구 확장에 대해 소개한다. 기존 CROWN 도구는 적용 대상 개발 환경이 Linux 환경으로 제한되어 있고 Concolic 테스팅 실행 결과를 쉽게 확인하기 어려워 사용자가 테스트 결과를 분석하기 어려웠다. 본 연구에서는 먼저 Concolic 테스팅의 적용 플랫폼을 넓히기 위해 CROWN 도구를 Windows 개발 환경에서 사용할 수 있게 확장하고 Concolic 테스팅 결과를 사용자가 쉽게 분석할 수 있도록 사용자 인터페이스를 개선하였다. The paper presents an extension of the Concolic testing tool CROWN(Concolic testing for Real-wOrld softWare aNalysis) for improving the applicability and usability of Concolic testing. The existing CROWN tool is limited to Linux platforms and the Concolic testing results generated from CROWN are hard for users to understand. We extend CROWN to run on Windows OS to increase the running platforms and improve user interface with CROWN and its applicability to help users analyze Concolic testing results in an easier way.

Concolic Testing 도구 KLEE의 다양한 탐색 방법 비교

김영주(YoungJoo Kim),김문주(Moonzoo Kim),김윤호(Yunho Kim),정의준(Uijune Jung) 한국정보과학회 2012 정보과학회 컴퓨팅의 실제 논문지 Vol.18 No.4

테스트 케이스 자동생성기법인 Concolic (concrete+symbolic) 테스팅 기법을 사용하는 테스팅 도구인 KLEE의 심볼릭 state를 스케줄링하는 탐색 방법(search strategy)들의 분기 커버리지 성능을 비교 분석했다. 또한 분기 커버리지를 보다 빠르게 높일 수 있는 breadth first search (BFS)를 새롭게 구현해 기존 방법들과 비교했다. 본 실험에서는 GNU Coreutils 버전 8.9를 대상으로, 주어진 시간에 각 탐색 방법들이 달성하는 분기 커버리지(branch coverage)를 비교하고 결과를 분석했다. Concolic (Concrete+symbolic) testing is an automated test case generation technique that works on target source code. This paper analyzes the branch coverage performances of the search strategies of a Concolic testing tool KLEE. In addition, we implemented the breadth first search (BFS) strategy to get higher branch coverage in KLEE. To compare the effectiveness of the search strategies, we applied KLEE to GNU Coreutils version 8.9 and compared the branch coverage of these search strategies and analyze their results.

효과적인 내장형 소프트웨어의 정수 확장 (Integer Promotion) 버그 검출 기법

김윤호(Yunho Kim),김태진(Taejin Kim),김문주(Moonzoo Kim),이호정(Ho-jung Lee),장훈(Hoon Jang),박민규(Mingyu Park) 한국정보과학회 2016 정보과학회논문지 Vol.43 No.6

세탁기, 냉장고 등의 가전제품에 탑재되는 8-bit MCU용 C 컴파일러는 소프트웨어 실행 속도를 높이기 위해 표준 C 언어 규칙을 따르지 않고 컴파일을 수행할 수 있다. 개발자가 일반 C 컴파일러와 8-bit MCU용 C 컴파일러의 차이를 정확하게 이해하지 못할 경우 표준 C 언어 환경에서는 발생하지 않으나 8-bit MCU를 사용하는 내장형 시스템에서는 발생하는 버그를 야기할 수 있으며 이런 버그는 표준 C언어 환경을 가정하는 버그 검출 도구로는 찾기 어렵다. 본 논문에서는 표준 C 정수 확장 규칙을 따르지 않는 8-bit MCU용 컴파일러를 사용할 때 발생하는 정수 확장 버그를 소개하고 정수 확장 버그를 탐지하기 위한 다섯 종류의 버그 패턴을 제안한다. 정수 확장 버그 패턴 검출 도구를 개발하여 LG전자 세탁기 소프트웨어를 분석한 결과 컴파일러 옵션을 잘못 선택한 경우 발생하는 27개의 정수 확장 버그를 발견하였다. C compilers for 8-bit MCUs used in washing machines and refrigerators often do not follow the C standard to improve runtime performance. Developers who are unaware of the difference between C compilers following the C standard and the C compilers for 8-bit MCU can cause bugs that do not appear in the standard C environment but appear in the embedded systems using 8-bit MCUs. It is difficult for bug detectors that assume the standard C environment to detect such bugs. In this paper, we introduce integer promotion bugs caused by the different integer promotion rules of the C compilers for 8-bit MCU from the C standard and propose 5 bug patterns where the integer promotion bugs occur. We have developed an integer promotion bug detection tool and applied it to the washing machine control software developed by the LG electronics. The integer promotion bug detection tool successfully detected 27 integer promotion bugs in the washing machine control software.

효과적인 변이 분석을 위한 C 프로그램 변이 도구 비교

김윤호(Yunho Kim),김현우(Hyunwoo Kim),양웅규(Woonggyu Yang),김문주(Moonzoo Kim) 한국정보과학회 2016 한국정보과학회 학술발표논문집 Vol.2016 No.12

CREST-BV: 임베디드 소프트웨어를 위한 Bitwise 연산을 지원하는 Concolic 테스팅 기법

김윤호(Yunho Kim),김문주(Moonzoo Kim),장윤규(Yoonkyu Jang) 한국정보과학회 2013 정보과학회논문지 : 소프트웨어 및 응용 Vol.40 No.2

기존 소프트웨어 테스팅 기법은 개발자가 수동으로 테스트 케이스를 작성해야 하는 비효율성으로 인해 임베디드 소프트웨어의 안정성 확보에 어려움이 있다. Concolic 테스팅 기법은 자동으로 소프트웨어 테스트 케이스를 생성함으로써 기존 소프트웨어 테스팅 기법의 문제를 해결했지만, 임베디드 소프트웨어 테스트에 필수적인 bitwise 연산을 지원하지 않는 문제가 있었다. 본 논문에서는 임베디드 소프트웨어를 위해 bitwise 연산을 지원하는 Concolic 테스팅 개선 방법을 연구하고 오픈 소스 임베디드 소프트웨어 Busybox에 적용하여 기존 연구와 분기 커버리지 및 실행 속도를 비교하였다. Busybox의 10개 유틸리티에 적용한 결과 기존 연구 결과 대비 평균 33%의 분기 커버리지 향상이 있었다. 또한, CREST-BV의 성능 저하 원인을 분석하였다. Conventional testing methods often fail to assure reliability of embedded software due to inefficiency and ineffectiveness of manual test case generation. Concolic testing can address this by automatically generating test cases but has a limitation that does not support bitwise operations critical to embedded software. To address this limitation, we have developed an improved concolic testing technique with bitwise operations support for embedded software. We applied the improved technique to 10 utilities of open-source embedded software Busybox and achieved 33% more branch coverage on average. In addition, we analyzed the performance bottleneck of the improved technique.

사례연구를 통한 정적 프로그램 분석 기법을 사용하는 도구의 비교

김윤호(Yunho Kim),박용배(Yongbae Park),김문주(Moonzoo Kim) 한국정보과학회 2013 정보과학회 컴퓨팅의 실제 논문지 Vol.19 No.8

프로그램 신뢰성 향상을 위해서 정적 프로그램 분석 도구가 많이 사용되고 있다. 하지만, 정적 분석 결과에서 거짓 경보를 걸러내기 위한 추가적인 분석이 필요하고 실제 오류를 찾지 못할 수 있는 문제점이 있다. 본 논문에서는 상용 정적 프로그램 분석 도구인 Coverity와 Sparrow 및 오픈 소스 도구인 Clang analyzer를 buffer overflow 벤치마크와 libexif 0.6.20 소스코드에 적용하여 실험 대상 도구가 오류를 찾아내는데 얼마나 효과적인지 사례 연구를 수행하였다. 실험 결과 buffer overflow 벤치마크에서는 Coverity, Sparrow, Clang analyzer 각각 6.02%, 3.61%, 0%의 버그탐지율과 2.41%, 1.20%, 0%의 오탐율을 보였다. libexif 0.6.20 적용에서 Coverity, Sparrow, Clang analyzer는 총745개의 오류를 찾아내었으나 알려진 7개의 오류 중 6개를 찾아내지 못하였다. 이와 같이 정적 분석 도구가 놓칠 수 있는 오류가 많으므로 높은 소프트웨어 신뢰성 보장을 위해 다른 기법과 병행하여 적용하는 것이 필요하다. Static analysis tools have been widely used to improve software reliability. However, static analysis tools have limitations that can generate false alarms and can miss real bugs. This paper presents a comparative study of three static analysis tools, Coverity, Sparrow, and Clang analyzer, through a case study on a set of buffer overflow benchmark programs and libexif 0.6.20 to evaluate the effectiveness of the three static analysis tools in terms of a bug finding capability. Experiment results on buffer overflow benchmark show that bug detection capabilities of Coverity, Sparrow, and Clang analyzer are 6.02%, 3.61%, and 0%, respectively and false alarm ratios of Coverity, Sparrow, and Clang analyzer are 2.41%, 1.20% and 0%, respectively. Experiment results on libexif 0.6.20 show that Coverity, Sparrow, and Clang analyzer detect 745 bugs and miss 6 out of 7 real bugs. Thus, it is necessary to use other bug finding techniques with static analysis techniques for achieving high software reliability, because static analysis tools can miss real bugs in target programs.

안드로이드 커널 모듈 취약점 탐지를 위한 자동화된 유닛 테스트 생성 기법

김윤호(Yunho Kim),김문주(Moonzoo Kim) 한국정보과학회 2017 정보과학회논문지 Vol.44 No.2

본 논문에서는 안드로이드 커널 모듈의 취약점을 탐지하기 위한 자동 유닛 테스트 생성 기법을 제안한다. 안드로이드 커널 모듈의 각 함수를 대상으로 테스트 드라이버/스텁 함수를 자동 생성하고 동적 기호 실행 기법을 사용하여 테스트 입력 값을 자동으로 생성한다. 또한 안드로이드 커널 모듈의 함수 포인터와 함수 선행 조건을 고려하지 않은 테스트 생성으로 인한 거짓 경보를 줄이기 위해 정적 분석을 통한 함수 포인터 매칭 기법과 def-use 분석을 사용한 함수 선행 조건 생성 기법을 개발하였다. 자동 유닛 테스트 생성 기법을 안드로이드 커널 3.4 버전의 세 모듈에 적용한 결과 기존에 존재하던 취약점을 모두 탐지할 수 있었으며 제안한 거짓 경보 감소 기법으로 평균 44.9%의 거짓 경보를 제거할 수 있었다. In this study, we propose an automated unit test generation technique for detecting vulnerabilities of Android kernel modules. The technique automatically generates unit test drivers/stubs and unit test inputs for each function of Android kernel modules by utilizing dynamic symbolic execution. To reduce false alarms caused by function pointers and missing pre-conditions of automated unit test generation technique, we develop false alarm reduction techniques that match function pointers by utilizing static analysis and generate pre-conditions by utilizing def-use analysis. We showed that the proposed technique could detect all existing vulnerabilities in the three modules of Android kernel 3.4. Also, the false alarm reduction techniques removed 44.9% of false alarms on average.

안드로이드 커널 모듈 취약점 탐지를 위한 자동화된 유닛 테스트 생성 기법

김윤호(Yunho Kim),김문주(Moonzoo Kim) 한국정보과학회 2016 한국정보과학회 학술발표논문집 Vol.2016 No.6