모델기반의커널테스팅프레임워크 523 모델기반의커널테스팅프레임워크 (MOdel-based KERnel Testing (MOKERT) Framework) 김문주 홍신 (Moonzoo Kim) (Shin Hong) 요약최근내장형시스템이점점많은분야에사용되며, 시스템에특화된운영체제커널에대한필요성이커지고있다. 하지만, 커널개발은코드의복잡성등의이유로말미암아테스팅에큰비용이소요됨에도불구하고, 높은신뢰성을달성하기가어려운실정이다. 이러한커널개발및테스팅의어려움을극복하기위해, 운영체제커널의동시성오류검출을지원하는모델기반의커널테스팅 (MOKERT) 프레임워크를제안한다. MOKERT 프레임워크는주어진 C 프로그램을 Promela 정형명세모델로변환하고나서 Spin 모델검증기를사용하여검증하고, 검증반례가생성된경우, 이검증반례를실제커널코드에서실행을시켜서진위를확인한다. 본연구에서는 MOKERT 프레임워크를리눅스 proc 파일시스템에적용하여, ChangeLog 에보고된오류가실제로자원경쟁문제를일으킴을확인하였을뿐만아니라, 커널패닉을일으키는새로운오류도발견하였다. 키워드 : 모델검증기법, 테스팅, 검증반례분석, 모델추출 Abstract 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. Key words :model checking, testing, counter example analysis, model extraction 본연구는 2008년교육과학기술부의재원으로한국학술진흥재단의지원을받아수행된연구이며 (KRF-2008), 교육과학기술부 / 한국과학재단우수연구센터육성사업의지원 (R11-2008-007-03002-0) 과지식경제부및정보통신연구진흥원의대학 IT연구센터지원사업 (IITA-2009-(C1090-0902- 0032)) 의연구결과로수행되었습니다. 이논문은 2009 한국소프트웨어공학학술대회에서 검증반례재연을통한모델기반커널테스팅 의제목으로발표된논문을확장한것이며, 추가성과는 Model-Based Testing 2009에발표하였음 종신회원 : KAIST 전산학과교수 moonzoo@cs.kaist.ac.kr 학생회원 : KAIST 전산학과 hongshin@gmail.com 논문접수 : 2009년 3월 16일심사완료 : 2009년 5월 15일 CopyrightC2009 한국정보과학회ː개인목적이나교육목적인경우, 이저작물의전체또는일부에대한복사본혹은디지털사본의제작을허가합니다. 이때, 사본은상업적수단으로사용할수없으며첫페이지에본문구와출처를반드시명시해야합니다. 이외의목적으로복제, 배포, 출판, 전송등모든유형의사용행위를하는경우에대하여는사전에허가를얻고비용을지불해야합니다. 정보과학회논문지 : 소프트웨어및응용제36권제7호 (2009.7) 1. 서론소프트웨어테스팅은일반적으로소프트웨어의총개발기간및가용자원의 50% 이상을차지한다. 여러소프트웨어시스템가운데운영체제커널은다음과같은원인으로, 개발및분석이어려운소프트웨어중하나로알려졌다. - 코드의복잡함운영체제커널은다양한하드웨어구성요소 (CPU, 메모리, 컴퓨터주변장치 ) 와소프트웨어구성요소 ( 장치드라이버모듈, 시스템콜라이브러리 ) 를관리하기위해서많은수의서비스루틴을가지고있다. 그뿐만아니라, 커널은성능향상을위해복잡한형태의최적화된알고리즘을사용한다. - 동시성으로말미암은동작경우의수증가커널은다중스레드프로그램이므로동시성오류 (con-
524 정보과학회논문지 : 소프트웨어및응용제 36 권제 7 호 (2009.7) currency bug) 를일으킬수있으며, 특정한동시성오류는특정스케줄링시나리오에의해서만발생한다. 동시에수행되는스레드의개수에따라서실행가능한스케줄링시나리오의수는지수적으로증가하며, 대부분의커널에서사용자는프로세스스케줄러를정교하게제어할수가없다. 이러한이유로커널의동시성오류를발견하고수정하는것은어렵다. - 유닛테스팅의어려움대부분의커널은성능의향상을위해단일 (monolithic) 커널구조를사용한다. 그러므로커널의유닛을독립적으로테스팅하기위해서는, 커널전체의구현에대한이해를요구하여, 많은비용이소요된다. 예를들어, proc 파일시스템을테스트하려면가상파일시스템, 메모리관리, 스케줄러등에관한실행환경을테스팅에적합하게구성하는과정이필요하다. 그이유는앞서언급한부분들이 proc 파일시스템의수행에밀접한관계가있기때문이다. 위와같이, 커널의특정부분을유닛테스팅하려면실행환경을상세하고적합하게구성해야하며, 이는때때로유닛테스팅그자체보다더큰노력을요구한다. - 적합한도구의부재커널테스팅을지원하는도구들이적은이유는, 테스팅툴에의해발생하는부작용으로커널이멈추거나, 예상치못한작동을일으킬가능성이있기때문이다. 또한, 일반적인테스팅도구는커널환경에서는사용할수없는라이브러리에의존하는경우가많아서, 커널테스팅에적합하지않다. 이러한이유로커널개발자들은커널을분석할때 printk() 나커널로그에의존하는경우가대부분이다. 커널의복잡성과크기를고려할때, 커널을구성요소단위로분석하는것이필요하다. 하지만, 위에서언급한이유로말미암아구성요소단위로커널을테스팅하는것은실질적으로어렵다. 결과적으로전통적인테스팅방법은커널을개발및분석하는데있어큰도움을주지못하며, 이로인해커널은특정개발자들만이개발할수있는영역으로남아있다. 하지만, 내장형시스템이일상생활모든영역에널리사용되면서특정목적을위한운영체제 ( 휴대폰또는센서네트워크를위한운영체제 ) 개발의필요성이점차증가하고있다. 그러므로커널의구성요소단위분석을지원하는프레임워크를개발하는것이중요하다. 본연구는모델추출 [1] 과모델검증기법 [2] 을이용해커널상의동시성오류를검출하는모델기반의테스팅프레임워크를개발하는것을목적으로한다. 앞서언급한이유로말미암아전통적인방식의테스팅으로커널을검증하는것은현실적으로어려움이많기에, 모델검 증기법이커널을분석하는데대안이될수있다. 그이유는, 모델검증기법은분석하고자하는커널의구성요소와그와관련된환경을추상화를통하여모델링하므로, 복잡한커널을구성요소단위로독립적으로분석하는것이가능하다. 게다가모델검증기법은모든가능한실행시나리오를분석하고, 구체적인검증반례 (counter example) 를제시해주기때문에, 커널을분석하는데유용하다. 하지만, 추상모델과실제프로그램간의차이로말미암아모델검증기법이제시한검증반례가실제프로그램상의에러인지, 아니면오경보 (false alarm) 인지의여부를개발자들이판단하기는어려우므로, 순수한모델검증기법만으로는커널을검증하는데문제가있을수있다. 본논문에서제시하는모델기반의커널테스팅프레임워크는모델검증과정에서발견한검증반례를모델이아닌, 실제운영체제커널코드의실행에서재연하는기능을제공한다. 이기능을통해모델기반의커널테스팅프레임워크는커널개발자들에게모델검증기법과테스팅의장점을동시에제공할수있다. 이기능은모델검증에서발견된오류의원인분석, 결함패치 (bug patch) 의적합성확인, 추상화모델의정밀화등의작업을가능하게한다. 따라서모델기반의커널테스팅프레임워크의사용은, 비록추상화모델과검증반례를재연하기위한실행환경을구성하기위한작업이필요하지만, 커널의분석에서전통적인테스팅기법의어려움을극복할수있다. 2. 관련연구커널과같은동시성을갖는프로그램의신뢰성을향상하려는방법중, 동시성프로그램테스팅의경우, 가능한많은프로그램수행경우를테스트하려고노력하고있다. [3] 에서는문맥전환 (context switching) 이일어나는시점마다무작위적으로실행될스레드를고르는알고리즘을제안하고, 실험을통하여이알고리즘을이용한테스팅이운영체제스케줄링에의존한테스팅기법보다더많은서로다른수행시나리오를검사하기때문에, 프로그램의동시성오류를찾을확률을높일수있음을보이고있다. 하지만, 동시성프로그램테스팅의경우오류의검출이확률적이라는근본적인단점이있다. 본연구에서제안하는모델기반의커널테스팅 (MOdel-based KERrnel Testing(MOKERT)) 프레임워크는, 모델검증도구를사용하여모든수행가능시나리오가요구사항을만족하는지를검사하기때문에, 확률적테스팅기법보다높은신뢰성을제공할수있다. [4] 에서는메시지전달이나세마포어등의명백한동기화 (synchronization) 메커니즘을사용하는경우, 하나의
모델기반의커널테스팅프레임워크 525 그림 1 모델검증도구 SPIN 이생성하는반례의예 수행시나리오를기반으로, 자원경쟁 (data race) 을일으킬수있는여러수행시나리오를변형하여생성하여테스트하는 RichTest라는툴을구현하고있으나, 실제동시성프로그램에서는공유변수를통한간접적인동기화사용이빈번하므로실제적인효용성이크지않다. 또한, 다중스레드프로그램의효과적인분석과디버깅을위하여, 실제프로그램의실행을기록하고, 이를재연하는연구가진행되고있다. [5] 에서는자바프로그램의실행을기록하고다시재연하는가상기계를구현하였다. 가상기계상에서다중스레드자바프로그램을테스트하고, 오류실행이발견되는경우, 오류실행을재연함으로써결함을분석하고디버깅할수있도록하였다. [6] 과 [7] 에서는프로그램의오류가일어나기전시점까지의프로그램의실행을기록하고, 이를재연하여프로그램오류의원인을분석할수있도록지원하는효과적인알고리즘을제시하고있다. 이와같은연구들에서는테스트중에관찰이가능한오류에대해서만재연기능을제시할뿐이므로, 만일테스팅과정중오류가발견되지않는경우, 프로그램에오류가없음을확신하지못한다. 하지만, 본연구에서제안하는 MOKERT 프레임워크는모델검증을통해모든수행가능한시나리오를분석하여, 모든오류를검출및재연할수있으므로위의연구들과는차별성을갖는다. 위에언급한연구들의약점인, 효과적인테스트케이스생성의어려움을극복하고자제안된일반적인모델기반테스팅기법은, 프로그램의특성을표현한모델을근간으로테스트케이스들을생성하는기술이다. [8] 에서는 Java PathFinder 모델검증도구를이용하여테스트케이스를생성하고있다. [9] 는비행안내시스템에관한사례연구를각각기호적 (symbolic), 한정적 (bounded), 명시적 (explicit) 모델검증도구에적용해테스트케이스를생성하고, 각모델검증도구가테스트케이스를생성하는시간및자원정도를비교하고있다. [10] 에서는추상상태기계 (abstract state machine) 기반의명세를 Promela 모델로자동변환하여, Spin 모델검증도구가생성하는검증반례를테스트케이스로이용한다. 위와같은기법의경우, 모델검증도구가생성하는검증반례를이용해테스트케이스를생성하지만, 본연구에서제안하는 MOKERT프레임워크와는달리, 검증반례를재연하는기능은없다. 본연구와밀접한관련이있는소프트웨어검증도구중 CHESS[11] 는무상태검색 (stateless search) 기법을사용하여동시성프로그램의많은스케쥴링시나리오를체계적으로테스트하며, 검출된오류시나리오를재연하는기능을제공한다. 하지만, 이기법은검증대상및환경이완전히구현된상태에서만적용가능하며, 기반플랫폼 (WIN32API 등 ) 에크게의존하기때문에, 하드웨어바로위에서동작하는커널을직접적으로테스트할수는없다. 다른소프트웨어모델검증도구들 [12,13] 은술어추상기법이나 SAT 인코딩을통해검증대상 C 프로그램으로부터정형모델을자동으로추출하여모델검증을수행하나, 상태폭발문제등의문제점들로말미암아그적용범위가크게제한되어있다. MOKERT는검증대상프로그램의완전자동화된분석을목적으로하고있지는않으며, 그대신전문가의지식을활용하여어플리케이션에대한추상화모델과환경을생성함으로써커널에존재하는동시성오류의실제적인검출을목표로한다 ([14] 참조 ). 3. 모델검증도구 SPIN과모델추출도구 Modex 3.1 모델검증도구 SPIN 모델검증도구 SPIN[2] 은모델명세언어로 Promela 를사용한다. C 언어와 Promela 언어의공통적인특성들로말미암아, C 프로그램으로작성된검증대상프로그램은이에대응되는 Promela 모델로변환할수있다. 예를들어, C언어에서의스레드는 Promela 모델에서프로세스로표현할수있으며, C에서사용되는모든제어구문들 (if, goto, while 등 ) 은 Promela의제어구문으로자동으로변환할수있다. 또한, Promela는 typedef와배열등을사용하여복잡한자료구조를표현할수있다. 1) 또한, Promela는 C 언어의함수호출에대응할수있는 inline 함수를제공한다. 이에더하여, SPIN 4.0 이상의버전에서는 Promela언어에 C 구문을내장하여사용할수있다. 이기능을통하여, C언어로작성된프로그램에서 Promela 모델로의자동변환의가용성이증가하였다. 1) 하지만, 포인터변수의직접적인표현은불가능하며, 배열등을통하여간접적으로표현해야한다.
526 정보과학회논문지 : 소프트웨어및응용제 36 권제 7 호 (2009.7) 모델검증도구 SPIN이생성하는검증반례에는다음과같은정보들이포함되어있다. - 단계번호 (step number) - 현재프로세스의고유번호 (process ID) - 현재프로세스가수행하는 proctype 이름 - 현재수행중인 Promela 모델의행번호 l -Promela 모델의 l 번째행구문예를들어, 그림 1에검증반례의 45번째단계는프로세스 1번이 proc_readdir이라는 proctype의 125번째행을실행한것이고, 그구문은 proc_subdir==1 이라는것을표현하고있다. 그리고 45번째단계에서 46번째단계로넘어가면서프로세스 1번에서프로세스 2번으로스케줄이바뀌고, 프로세스 2번이 remove_proc_entry라는 proctype의 156번째행을실행함을보이고있다. 3.2 모델추출도구 Modex Modex[1] 는 C 프로그램과변환스크립트를입력으로받아, C 프로그램을 Promela 언어로자동변환하는모델추출도구이다. Modex는 C 프로그램에서 if, while, goto와같은제어구문을그에상응하는 Promela 제어구조로자동변환한다. 그결과 Modex가생성한 Promela 모델은검증대상 C 프로그램과동일한제어구조를가지게된다. 제어구조를제외한다른 C 구문들은 Promela 모델의내장형C 구문으로표현된다. C 프로그램에서수식들은 c_expr{ } 키워드로시작하는내장형 C 수식으로표현되며, 변수대입이나함수호출등은 c_code{ } 키워드로시작하는내장형 C 구문으로표현된다. Promela명세의내장형구문들은 SPIN 모델검증도구가생성하는검증프로그램의코드에그대로복사되어사용되게된다. 사용자는변환스크립트를사용하여변환과정을조절 할수있다. Modex에서사용하는변환스크립트는변환표 (translation table) 로표현된다. 하나의변환표에는변환대상 C 프로그램의각함수에대한변환규칙 (translation rule) 이기술되어있다. 하나의변환규칙은특정문자패턴으로시작하는검증대상 C프로그램의구문이, 어떻게 Promela 구문으로변환되어야함을명세하고있다. 4. 모델기반커널테스팅프레임워크 4.1 개요모델기반커널테스팅 (MOdel-based KERnel Testing(MOKERT)) 프레임워크는모델검증기법의결과인검증반례를실제검증대상프로그램에적용함으로써, 커널코드에서의동시성오류테스팅의어려움을극복하는것을목표로한다. 모델검증단계에서의반례를실제검증대상프로그램에서재연하는것은소프트웨어산업현장에모델검증기술을적극적으로도입하는데중요한요소임에도, 대부분의모델검증프레임워크는이문제에대해적합하게논의하고있지않다. 전통적인모델기반테스팅방식은그림 2(a) 에표현된것과같이, 정형모델을사용자가수작업으로생성하고, 반례의분석도사용자가수작업으로수행한다. 이러한과정은많은시간과노력이소모된다. MOKERT 프레임워크에서의모델기반테스팅방식은그림 2(b) 에표현되어있다. MOKERT 프레임워크에서는 Modex를사용하여검증대상 C 프로그램으로부터 ( 반 ) 자동으로정형모델을추출한다. 이추출과정에서는변환스크립트 T가사용된다. 변환스크립트 T에는변환대상 C 프로그램의특정구문이 Promela의어떠한구문으로변환되어야하는지명세되어있다. 이러한 T의역인 T -1 은변환된 Promela모델의특정구문이변환대상 C 프로그램의어 (a) 사용자가제공하는모델을이용하는전통적인모델기반테스팅방법 그림 2 모델기반테스팅 (b) 모델추출도구를이용하는 ( 반 ) 자동모델기반테스팅방법
모델기반의커널테스팅프레임워크 527 떠한구문을변환한것인지에대한정보를나타내며, 따라서 T -1 을이용하면주어진반례가 C프로그램에서어떠한구문의실행을표현하는것인지이해할수있다. 그리고이정보를바탕으로, 검증대상프로그램이반례에서보이는것과같은형태의실행을하도록대상프로그램을수정 (instrumentation) 한다. 이렇게수정된프로그램을실행함으로써, 실제커널프로그램에서반례의재연 (replay) 이가능하다. MOKERT는반례의재연에초점을맞춘만큼, liveness property를제외한일반적인 safety property를요구명세대상으로한다. MOKERT 프레임워크가제공하는반례재연기능은다음과같은장점이있다. 그림 3 MOKERT프레임워크의구조 - 결함의원인분석용이 MOKERT는모델검증단계에서발견한반례를단계별로실행할수있는기능을제공한다. 그러므로사용자는커널코드상의오류를발생시키는결함의원인을보다편리하게분석할수있다. 이는동시성오류를찾는데장점이될수있는데, 그이유는결함의재연을위해사용자가직접스레드스케줄링을조작해야하는불편함을해결할수있기때문이다. - 모델개선 (model refinement) 모델검증과정중, 초기에생성된모델은과도하게추상화되어있을가능성이크다. 올바른검증결과를위해서는모델을점차세밀하게만드는과정을반복해서적용할필요가있다. MOKERT에서는정형모델에서반례가발견되는경우, 그반례가올바른것인지아니면과도한추상화로생긴오경보 (false alarm) 인지의여부를자동으로확인할수있는기능을제공한다. 반례가오경보인경우, 정형모델을개선하여야한다. 이러한개선과정은술어추상화 (predicate abstraction) 기술에서사용하는반례기반추상화개선기술 (counter example guided abstraction refinement: CEGAR)[15] 과 개념적으로유사하나, 추상모델의개선을수동으로수행한다는점에서차이가있다. - 결함패치검증 (validation of bug patch) 커널에서의오류는대부분프로그램코드를사람이눈으로검사하거나 (code inspection) 나토의, 혹은가상시나리오를바탕으로보고되며, 커널영역에대한테스팅의어려움으로인해, 테스팅으로실제적인오류를발견하는경우는비교적적다. 따라서리눅스의 Change- Log는실제로는불필요하거나올바르게결함을해결하지못한패치를포함하고있으며, MOKERT 프레임워크를사용함으로써결함패치가올바른지에대한여부를검증할수있다 (5.2절참조 ). 4.2 MOKERT 프레임워크의구조 MOKERT의전반적인구조는그림 3에서표현된형태와같다. MOKERT프레임워크는정적단계와동적단계로구성된다. MOKERT프레임워크의정적단계는다음과같은세부과정들로구성된다. (1) 검증대상 C 프로그램을변환스크립트를기반으로 Modex를통하여 Promela 모델로변환한다. 생성된 Promela 모델은프로세스, 환경모델, 검증요구사항명세등으로구성된다. 이과정에서, Modex의중간결과물로 Promela 모델의행번호와검증대상 C 프로그램의행번호사이의대응정보가생성된다. (2) 모델검증도구 SPIN은이전단계에서생성된 Promela 모델이검증요구사항명세를만족하는지를검사한다. 만약모델이검증요구사항명세를만족한다면모델검증도구 SPIN은검증결과를사용자에게보고하고, 그렇지않았으면반례를생성한다. (3) 검증대상 C 프로그램은 (1) 단계에서생성된 Promela 모델의행번호와검증대상 C 프로그램의행번호사이의대응정보와 (2) 단계에서생성된반례를기반으로하여검증대상프로그램이반례를재연할수있도록대상프로그램을수정 (instrumentation) 한다. 수정된검증대상 C 프로그램은, 반례의문맥전환이일어나는부분에대응하는검증대상 C 프로그램의부분에 probe가삽입된형태이다. 또한, 수정된프로그램에는 MOKERT의동적단계를지원하기위해제어스레드 (controller thread) 와모니터스레드 (monitor thread) 가포함되며, 이밖에모델검증에서의환경모델과동일한테스팅환경을구성하기위한테스트드라이버가포함된다. 수정된대상 C 프로그램은컴파일러를이용하여실행가능한형태의프로그램으로만들어진다. 동적단계에서는검증대상프로그램으로부터생성된스레드들이제어스레드, 모니터스레드와함께실행된다. 제어스레드는반례의재연을위해검증대상스레
528 정보과학회논문지 : 소프트웨어및응용제 36 권제 7 호 (2009.7) 드들의 probe와통신을하며그들의스케줄을조정한다. 모니터스레드는검증대상스레드들과제어스레드의상태를관찰하고반례가올바르게재연되고있는지확인하는기능을제공한다. MOKERT 프레임워크에서는, 검증반례가생성되면사용자가직접테스트드라이버를구축해야한다. 하지만, 이작업은일반적인테스트를위한테스트드라이버를구축하는작업보다간단하며, 그이유는다음과같다. 첫째, 사용자는테스트드라이버를구축할때에모델검증단계에서사용했던추상환경모델을참고할수있다 [16]. 둘째, MOKERT 프레임워크에필요한테스트드라이버는, 하나의검증반례가나타내는특정시나리오만을지원하면되므로, 범용적인테스트베드를구축하는데에필요한노력에비해적은양의노력만이요구된다. 4.3 동적 (run-time) 단계동적단계에서모니터스레드는검증대상스레드들과제어스레드의상태를관찰함으로써반례의재연이올바르게이루어지고있는지를관찰한다. 모니터스레드는검증대상프로그램의실행이반례의마지막에도달하게되면, 사용자에게재연이성공적으로이루어졌다고알린다. 이와동시에테스트드라이버는테스트결과를통해, 재연에의한실행이요구사항을만족하는지를알려주게된다. 다음은반례재연의가능한결과를나타낸다. (i) 반례의마지막에도달하면서요구사항을만족하지않는경우 (ii) 반례의마지막에도달하였지만요구사항을만족하는경우 (iii) 반례의마지막에절대도달하지않는경우첫번째경우는사용자가반례의재연을통해기대하는결과이다. 두번째와세번째는반례의재연에실패한경우를가리킨다. 만약일정시간내에반례의마지막에도달하지못하는경우, 모니터스레드는사용자에게현재검증대상스레드들의상태와함수호출스택의상태등의로그정보와함께반례재연에실패함을알린다. 반례재연의실패는다음과같은이유에기인한다. (i) 정확하지않은모델링검증대상프로그램에대한모델이과도하게추상화된경우, 실제프로그램에서반례를재연할수없다. 즉, 모델에서반영하지못한커널전체의환경설정으로반례의실행이실패할수있다. 예를들어, 커널전체적으로인터럽트가제한되어있거나, 우선순위스케줄링이진행중인경우, 제어스레드가검증대상스레드의스케줄을조절하는것은불가능하므로반례를재연할수없다. (ii) 정확하지않은테스트드라이버구축테스트드라이버가잘못작성되어검증환경을올바르게구성하지못하는경우, 반례의재연에실패하게된다. 그림 4 proc_readdir() 함수와 remove_proc_entry() 함수간의자원경쟁 5. 사례연구 : Proc 파일시스템의 proc_readdir () 와 remove_proc_entry() 간의자원경쟁오류본절에서기술하는사례연구는, 실제커널의동시성오류검출에 MOKERT 프레임워크가어떻게사용되는가를구체적으로기술함으로써, 본프레임워크의유효성을실험적으로보이고자한다. 5.1 오류설명 Proc 파일시스템은 UNIX 계열의운영체제에서사용되는가상파일시스템중하나이다. Proc 파일시스템을통하여사용자는특정프로세스의정보를열람하거나커널모듈과의통신을수행할수있다. 리눅스 Changelog 2.6.22에는리눅스커널 2.6.21에서발견된 proc_readdir() 함수와 remove_proc_entry() 함수사이의자원경쟁오류를보고하고있으며, 이를해결하기위한결함패치를소개하고있다. 이결함에의하여발생가능한자원경쟁상태는그림 4에설명되어있다. remove_proc_entry() 함수의 24번째행에서 de(proc파일시스템에서하나의디렉토리항목을나타내는개체 ) 를제거하기전, 23번째행에서 de의 count값을읽음으로써현재항목에대한동시사용자가없는지를확인한다. 하지만, proc_readdir() 함수에서는, de 값을읽기전에 de의 count 값을증가시키지않고있다. 따라서 remove_proc_entry() 함수에서는 proc_readdir() 함수가 de를읽으려고하는지파악하지못한채 de를제거하게되고, 결과적으로 proc_readdir() 함수의 70번째행에서는 remove_ proc_entry() 함수의수행으로이미제거작업이수행된 de 개체의내용을읽는명령을수행하게된다. 5.2 오류재연 MOKERT 프레임워크를통해 proc_readdir() ( 총 67행 ), remove_proc_entry() ( 총 35행 ) 그리고동기화관련함수등위두함수와관련된함수들이 Modex를통하여 Promela 모델로변환되었다. proc_ readdir() 함수에관한 Promela 프로세스는총 68행이고, remove_proc_entry() 함수에관한 Promela
모델기반의커널테스팅프레임워크 529 프로세스는총 36행이었다. 이에더하여, 검증환경 ( 총 76행 ) 은 Jan, Feb, Mar, Apr 로명명된 4개의항목을가지는하나의 proc 파일시스템디렉토리로설정하였다. 이러한환경설정은그림 5와같다. 검증환경은 proc_readdir() 함수와 remove_proc_entry() 함수에관한두프로세스를생성하며, remove_proc_ entry() 함수가 Feb 항목을지우는것과동시에 proc_readdir() 함수가같은디렉토리에존재하는모든항목을읽는작업을수행하도록설정하였다. 요구사항으로는 proc_readdir() 함수의 70번째행에서접근하는디렉토리항목은이전에제거되지않은것이어야한다는조건으로표현하였다. 이요구사항을검증하기위해각디렉토리항목에 removed라는표식을추가하였으며, 이는디렉토리항목이제거되었을때 true의값을가지게된다. 모델검증도구 SPIN은이모델로부터 59단계로이루어진반례를생성하였다. 그림 5 디렉토리항목구조의예실제운영체제커널을대상으로반례를재연하기위하여, 테스트드라이버 ( 총 98행 ) 는모델에서의환경과동일한형태의환경을생성하도록작성되었다. 커널에서반례를재연한결과, remove_proc_entry() 함수로제거한디렉토리항목은 proc_readdir() 함수의결과로출력되는반면, 제거하지않은항목들이출력되지않는증상을확인할수있었다. 다시말하여, proc_readdir() 함수는그실행결과로 Jan, Feb 만을출력하였고, Mar, Apr 은출력하지않았다. 이는그림 4에서설명하는 proc_readdir() 함수와 remove_proc_entry() 함수간의자원경쟁상태로말미암은잘못된출력결과이다. 이러한결함은리눅스 2.6.22 에서 proc_readdir() 함수의 68번째행에 atomic_inc(&de->count) 구문을추가함으로써해결되었다. Promela 모델에리눅스 2.6.22에서추가된구문을반영하였을때, 더이상오류가발생하지않았으며, 따라서리눅스 2.6.22의패치가올바름을확인할수있었다. 본사례연구는 2명의대학원생이 3일에걸쳐서수행하였으며, 그중 2일은 proc 파일시스템 C 코드를이해하기위해소요되었다. 5.3 새로운자원경쟁오류검출리눅스커널 2.6.21 proc 파일시스템을검증한연구를, 본논문을작성할시점에서가장최근리눅스커널인 2.6.28.2로확장적용한결과, 새로운자원경쟁문제 로인하여커널패닉이발생되는새로운오류를발견하였으며, 관련리눅스커널코드를관리하는담당자에게보고하였다. 새로이발견된오류는, 스레드 T1이 remove_proc_entry() 를통해하나의디렉토리 d1 를삭제하려할때, 동시에다른스레드 T2가 remove_proc_entry() 를사용해하위디렉토리인 d1/d2 를삭제하면서 d1/d2 를가르키는포인터의값을 null로바꾼경우, T1이이러한변화를파악하지못하고 null 포인터를참조하기때문에커널패닉을발생시킨다. 본사례연구는리눅스의버전이높아지면서 remove_ proc_entry() 의길이가 35행에서 70행으로증가하면서, 추가적인모델링및환경을구성했어야함에도불구하고대학원생 1명이하루만에검증을완료할수있었다. 이는기존의리눅스 2.6.21 proc 파일시스템을위해구성한모델및재연테스트베드를재활용할수있었기때문이다. 본사례연구를통하여, MOKERT가기존에보고된오류의진위를판별할수있을뿐아니라, 새로운동시성오류를검출하는용도에효과적으로사용될수있다는것을보일수있었다. 6. 결론 본연구는운영체제커널의동시성오류를효과적으로검출하기위한 MOKERT 프레임워크를제안하고있다. MOKERT는사용자가추상화모델링작업을통해서운영체제커널의각구성요소를독립적으로분석한결과를, 검증반례재연기능을통하여실제커널코드에적용하여확증하는것을지원한다. 따라서, MOKERT 프레임워크는동시성을가지는커널의동작을모델검증을통해면밀히검사함으로써커널코드분석의신뢰성을향상시키는데에쓰일수있다. 본연구에서는리눅스커널의 proc 파일시스템을대상으로하는사례연구를통하여, 이프레임워크의실효성을확인하였다. 사례연구를통해서, 모델검증을기반으로하는테스팅기술의발전을위하여모델추출기술의추가적인개발및발전되어야함을알수있었다. Modex를포함하는현재의모델추출기술은아직사용자의높은숙련도를요구하고있기때문이다. 저자들은이번연구에서개발된 MOKERT 프레임워크를이용하여, 더많은리눅스파일시스템의컴포넌트들을분석하여신뢰성을향상시키는연구를진행하는한편, 공개 real-time OS 등의분야로적용대상을확장할예정이다. 참고문헌 [1] G. J. Holzmann and R. Joshi, "Model-driven software verification," Spin Workshop, April 2004.
530 정보과학회논문지 : 소프트웨어및응용제 36 권제 7 호 (2009.7) [2] G. J. Holzmann, "The Spin Model Checker," Wiley, New York, 2003. [3] K. Sen, "Effective random testing of concurrent programs," Proceedings of the twenty-second IEEE/ ACM International Conference on Automated software engineering, 2007. [4] R. H. Carver and Y. Lei, "A General Model for Reachability Testing of Concurrent Programs," IEEE International Conference on Formal Engineering Methods, 2004. [5] M. Christiens, J. D. Choi, M. Ronsse and K. Bosschere, "Record/Replay in the Presence of Benign Data Races," In International Conference on Parallel and Distributed Processing Techniques and Applications, 2002. [6] S. Artzi, S. H. Kim, and M. D. Ernst, "ReCrash: Making Software Failures Reproducible by Preserving Object States," European Conference on Object-Oriented Programming, 2008. [7] S. Narayanasamy, G. Pokam, and B. Calder, "Bug- Net: Recording application-level execution for deterministic replay debugging," IEEE Micro, 26(1): 100-109, 2006. [8] W. Visser, C. S. Pasareanu and S. Khurshid, "Test input generation with Java PathFinder," International Symposium on Software Testing and Analysis, 2004. [9] M. P. E. Heimdahl, S. Rayadurgam, W. Visser, G. Devaraj and J. Gao, "Auto-generating Test Sequences Using Model Checker: A Case Study," Formal Approaches to Software Testing, 2004. [10] A. Gargantini, E. Riccobene and S. Rinzivillo, "Using Spin to Generate Tests from ASM Specifications," Abstract State Machines, 2003. [11] M. Musuvathi, S. Qadeer and T. Ball, "Chess: A systematic testing tool for concurrent software," Microsoft Research Technical Report MSR-TR- 2007-149, 2007. [12] D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, "The software model checker BLAST: Applications to software engineering," International Journal on Software Tools for Technology Transfer, 2007. [13] E. Clarke, D. Kroening, and F. Lerda, "A tool for checking ANSI-C programs," Tools And Algorithms for Construction and Analysis of Systems, 2004. [14] P. Camara, M. Gallardo and P. Merino, "Model extraction for ARINC 653 based avionics software," Spin workshop, 2007. [15] E. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith, "Counterexample-guided abstraction refinement," Computer Aided Verification, July 2000. [16] M. Kim, Y. Kim, Y. Choi and H. Kim, "Pre-testing flash device driver through model checking techniques," IEEE International Conference on Software Testing, Verification and Validation, April 2008. 프트웨어 김문주 1995 년 KAIST 전산학과학사. 2001 년 Univ. of Pennsylvania 박사. 2002 년 ~ 2004 년 SECUi.COM 차장. 2004 년 ~ 2006 년 POSTECH 연구원. 2006 년 ~ 현재 KAIST 전산학과조교수. 관심분야는정형검증, 소프트웨어테스팅, 내장형소 홍신 2007년 KAIST 전산학전공 ( 학사 ). 2007 년~현재 KAIST 대학원전산학전공석사과정. 관심분야는소프트웨어검증, 모델체킹, 프로그램분석