이광근
아이락은 C 프로그램 실행 중에 발생할 수 있는 버퍼오버런 에러를 프로그램 실행 전에 자동으로 빠짐없이 찾아 주는 프로그램 분석기이다. 이 분석기는 요약 해석의 틀 속에서 설계됐으며, 리눅스 커널, GNU 프로그램, 상용 임베디드 소프트웨어에 적용되어 실제 버그를 찾아냈다. 또한 아이락은 정적 프로그램 분석으로부터 기인하는 허위 경보에 유연하게 대처할 수 있는 기능을 제공한다.
프로그램이 버그 없이 안전하게 실행되는지를 100% 보장할 수 없을까? 우리는 많은 컴퓨터 프로그램들이 아무런 문제없이 안전하게 돌아간다는 보장도 없이 그 프로그램에 의존해 살아가고 있다. 일례로, 서울 시내버스 교통카드 시스템의 마비라든지, 휴대폰의 버그 등 소프트웨어 장애는 이미 우리 일상에 악영향을 미치고 있다. 지구상 곳곳에 존재하는 컴퓨터에서 돌아가는 프로그램들에 우글거리는 버그들이 한꺼번에 나타난다고 상상해보라. 이 얼마나 끔찍한 일이 되겠는가? 하지만 다행히도 컴퓨터의 발달과 함께 오랜 시간에 걸쳐 프로그램의 버그를 줄일 수 있는 많은 기술들이 개발되어 왔다.
1970년대 제일 처음 모습을 드러낸 버그 잡는 기술은 바로 프로그램이 제대로 생겼는지를 검증해 내는 구문 검증 기술(parsing)이다. 이 기술은 이미 우리가 너무나 익숙하게 사용하고 있기에 지금은 거의 관심을 두지 않고 있다. 하지만 이 기술 덕분에 더 이상 우리가 짠 프로그램에서 저지른 문법 실수를 일일이 눈으로 확인해서 찾지 않아도 된다. 가령, C 프로그램에서 세미콜론(;)을 빠뜨렸을 때 이를 찾기 위해 고생하는 프로그래머는 없는 것처럼 말이다. 그러나 제대로 생긴 프로그램이라고 모두 문제없이 돌아가는 것은 아니다. 예를 들어 x = “버그” + 10 같은 프로그램은 생긴 것은 멀쩡하지만 하는 일은 전혀 그렇지 않다.
이런 프로그램들을 안전하게 걸러내기 위해 1990년대에 활성화된 기술이 바로 타입 검증(type checking)이다. 타입에 맞지 않는 프로그램들은 실행 중에 계산할 수 없게 되어 예측할 수 없는 방향으로 프로그램이 실행되거나 혹은 원인도 모르게 비정상 종료된다. 따라서 프로그램의 모든 연산에서 다루는 값들은 항상 정의된 타입에 맞는 값들이어야 한다. 어떤 프로그램이 항상 그러한 성질을 만족하면서 실행될 것인지를 자동으로 검증해 주는 것이 바로 타입 검증 기술이다.
한편, 타입이 맞는 프로그램이라고 해도 모두 제대로 실행된다고 할 수는 없다. 타입보다 더욱 정교한 성질에 대한 보장이 필요한 것이다. 물을 만들기 위해서는 수소와 산소가 있어야지 수소랑 질소가 만나서는 안 된다는 사실을 검증하는 것은 타입 검증과 비슷하다. 하지만 물 100g 이상을 만들기 위해서는 적어도 수소 몇 g과 산소 몇 g이 필요하다는 사실까지의 검증은 더 정교한 기술을 필요로 한다.
자동 증명 기술(theorem proving)과 정적 분석 기술(static analy sis)이 바로 그러한 정교한 프로그램의 버그 잡는 기술의 예이다. 이러한 기술들은 우리가 분석하고자 하는 프로그램의 성질을 정교한 논리식으로 정의하고 그 식을 만족하는 지를 온갖 방법을 동원해 찾아낸다. 대게 이러한 정교한 분석들은 많은 시간과 자원을 필요로 하기 때문에 아직은 컴파일러에 장착될 정도는 되지 못한다. 모든 사람들이 이 기술을 아무렇지도 않게 사용할 날이 아직은 멀어 보이지만, 지금 이 순간에도 전 세계의 수많은 사람들이 이 기술을 더 쓸 만하게 만들어나가고 있다.
정적 프로그램 분석
정적 프로그램 분석(static program analysis)은 프로그램의 성질을 실행 전에 자동으로 안전하게 빠짐없이 예측하는 기술이다. 사실 프로그램의 성질(버그)을 실행 전에 정확히 알아내기란 불가능하다. 하지만 프로그램 분석 분야에서는 오랜 기간 동안 사람들이 이 한계에 도전해 왔고, 프로그램의 성질을 실행 전에 미리 알아내는 것이 어느 정도 가능하게 되었다.
예를 들어 다음 날의 날씨를 예측하는 기계가 있다고 치자. 그런데 다음 날 비가 올 지를 정확하게 예측하는 것은 잘 알고 있듯이 불가능한 일이다. 우리는 다음 날 비가 온다면 반드시 이 기계가 비가 온다고 미리 말해주기를 원한다. 사실, 이러한 조건을 만족하는 기계를 만드는 것은 아주 쉽다. 항상 비가 온다고 말하는 기계를 만들어 버리면 되는 것이다. 그런데 이런 기계는 아무런 정보도 주지 못하므로 쓸모가 없다. 쓸모 있는 기계를 만들기 위해 우리가 할 수 있는 최선은 다음날 비가 오지 않는 것이 확실한 경우에는 기계가 비가 온다는 말을 하지 않게 하는 것이다. 여기서 말하고자 하는 프로그램 분석 기술도 이와 비슷하다.
안전하고 정확한 분석기란 버그가 있을 수 있는 곳에서는 항상 경고를 해주면서 실제로 문제가 없는 것이 명백한 곳은 많이 피해가는 것이다. 버그가 있을 만한 곳은 모두 찾아주기 때문에 ‘빠짐없는, 안전한’ 분석기이다. 어떤 방법이 이러한 기술을 가능하게 하는 지 살펴보자. 알고 보면 정말 간단하다. 프로그램이 실행 중에 일어날 수 있는 모든 일을 실행 전에 예측할 수 있으면 된다. 프로그램의 모든 부분에서 일어날 수 있는 모든 실행 상태들을 계산해 내면 되는 일이다. 다음의 간단한 코드를 보자.
int main( )
{
int x, idx;
x = 0;
while (x<100) {
idx = rand()%10;
x = x + 1;
}
return 0;
}
우리가 알고 싶은 프로그램의 성질이 만약 이 프로그램이 끝나기 전에 메모리에 있는 변수들이 가지고 있는 값들이라고 생각해보자. 그럼 실제로 실행해보면 어떻게 될까? 변수 x에 저장된 값은 루프(loop)을 돌고 난 후의 값이니 100이 되어 있을 테고, 변수 idx에 저장된 값은 0부터 9 사이의 임의의 값을 하나 갖게 될 것이다. 그렇다면 정적 프로그램 분석의 결과는 무엇이 되어야 안전하겠는가?
변수 i의 값은 100이고 변수 idx의 값은 0에서부터 9사이의 모든 값이라고 하면 안전한 분석이다. 실제 실행 중에 일어날 수 있는 모든 것을 포섭하고 있기 때문이다. 물론 더 많은 것을 이야기해도 안전하다. 예를 들면 변수 i의 값은 100 이상이고 idx는 모든 값이 될 수 있다고 이야기하는 것이 되겠다. 하지만 이것은 첫 번째 분석 결과보다 더 많은 집합을 이야기하고 있으므로 부정확하다. 분석 결과로 정확히 알고 싶은 것이 2라는 값이었다면 정수, 짝수, 0보다 큰 짝수, 0하고 10 사이의 짝수라고 이야기하는 것들은 안전하지만 부정확한 분석 결과이다.
테스트를 통한 디버깅의 한계
정적 프로그램 분석이 프로그램을 실제로 돌려가며 테스트를 통해 디버깅하는 것과 다른 점은 무엇일까? 가장 중요한 차이는 정적 프로그램 분석은 실행 중에 일어날 수 있는 모든 것을 포섭하지만 테스트는 그렇지 못하다는 것이다. 앞의 코드만 보더라도 실제로 수백 번의 테스트를 하더라도 변수 idx가 가지는 값들을 전부 찾아낸다는 보장을 할 수 없다. 이와 같이 간단한 코드에서조차도 힘들진대 실제 현장에서 개발하고 있는 커다란 프로그램에 대해서는 어떻겠는가? 또, 한 번 실행을 하는데 오랜 시간이 걸리거나 프로그램의 입력으로 될 수 있는 값들의 개수가 무한하거나 혹은 끝나지 않는 프로그램들을 테스트를 통해서 검증해내기란 정말 어려운 일이다. 그런 면에서 테스트를 통한 검증은 근본적으로 한계를 지니며, 프로그램에 버그가 없다는 사실이 아니라 단지 버그가 있는 지만 확인할 수 있다.
정적 프로그램 분석 기술의 적용
실제로 프로그램 분석 기술을 사용하여 유용한 일을 해낸 외국의 사례들을 살펴보자. 윈도우 98을 사용하던 대부분의 많은 사람들은 이유도 모른 채 발생하는 블루스크린에 짜증이 난 경험이 있을 것이다. 윈도우 XP에서는 블루스크린을 거의 볼 수 없게 되었는데 그 이면에는 마이크로소프트(이하 MS) 내부에서 버그 잡는 기술에 대한 투자가 있었다.
그 한 예가 바로 슬램(SLAM) 프로젝트이다. SLAM은 MS 연구소에서 프로그램이 원하는 속성을 만족하는지 검증하고 버그를 발견해 주어 신뢰성 높은 소프트웨어를 제작토록 도와주기 위한 프로젝트이다. MS는 SLAM 프로젝트의 결과물을 이용하여 윈도우 XP가 사용하는 디바이스 드라이버(device driver)의 버그들을 찾아내고 있다. 윈도우의 많은 버그들 중에는 드라이버에서 발생하는 버그들이 특히 많은데, 왜냐하면 이런 드라이버들은 새로운 기기가 추가될 때마다 새로이 작성되고 개발자들이 보통의 운영체제를 개발한 쪽과 다르기 때문이다. SLAM의 결과물로 현재 100여 개의 드라이버에 대해 20여 개의 속성을 검증하여 20개 이상의 버그를 찾아냈다고 한다.
Bandera는 자바로 작성된 프로그램이 올바르게 작동하는지를 검증해주는 프로그래밍 도구이다. 특히 여러 쓰레드(thread)가 동시에 (concurrent) 수행되는 경우에 발생 가능한 오류를 찾아준다. 예를 들어, 모든 쓰레드가 서로를 기다리기만 하는 교착 상태(dead lock)에 빠지지 않는지, 또는 무한정 어떤 조건이 만족되기를 기다리기만 하는 쓰레드가 없는지 검사해 준다. Bandera는 캔사스 주립 대학에서 1998년부터 개발해왔고 실제 현장에 적용되고 있다. NASA와 하니웰 테크놀로지 센터(Honeywell technology center)에서 Ban dera를 사용하여 개발하는 소프트웨어를 검증하고 있다. 특히 하니웰 테크놀로지 센터는 Bandera를 이용하여 항공 운항을 위한 실시간 운영체제인 DEOS(Digital Engine Operating System)에서 오류를 찾아냈고 수정할 수 있었다.
또 다른 예로 AirBus의 컨트롤러 소프트웨어 모듈 검증이 프로그램 분석 기술을 통해 성공적으로 이뤄졌다. 기존에 의존하던 다른 검증 기술(verification by theorem proving)보다 그 비용과 효과가 뛰어났기 때문에 AirBus에서는 비행기 내장 소프트웨어 개발에 프로그램 분석 기술을 통한 검증 단계가 반드시 들어가도록 표준 개발 과정을 개편하고 있다.
요약 해석
초등학교 교실의 산수 시간. 선생님이 정수식 계산 문제 하나를 학생들에게 내준다.
문제 : 128 쪱 22 + (1920 쪱 (-10)) + 4 = ?
0.1 초 후에 철호가 정수라는 답을 제시하는 것을 시작으로 시간이 흐름에 따라 영호, 진호, 명호, 상호가 점점 더 정확한 답을 얘기한다.
철호: 정수
영호: 짝수
진호: 음수
명호: -100000보다 크고 10000보다 작은 정수
상호: -16380
철호, 영호, 진호, 명호, 상호 등의 답은 모두 옳다고 할 수 있다. 다만 정확도에는 차이가 난다. 모두 옳다는 얘기는 각각이 제시한 답 속에 정확한 답 -16380이 포함되기 때문이다. 정확도의 차이는 각 답들이 제시하는 집합의 크기에서 기인한다. 마지막 상호의 답이 가장 정확한데 상호의 답은 하나의 원소만 가지고 있기 때문이다. 짝수라는 답을 얘기한 영호의 머리 속을 잠시 들여다보자. 영호는 모든 정수는 홀수와 짝수 집합의 한 원소에 대응시킬 수 있다는 사실을 알고 있었을 것이다. 그리고 짝수와 짝수의 합은 짝수, 짝수와 짝수의 곱은 짝수, 홀수와 짝수의 합은 홀수가 된다는 식의 홀수, 짝수 계산법을 알고 있었을 것이다. 영호의 머리 속에서 주어진 문제는 “짝수 × 짝수 + 짝수 × 짝수 + 짝수”라는 문제로 바뀐 후, 알고 있는 홀수, 짝수 계산법이 적용되어 최종적으로 짝수라는 답에 이르게 되었을 것이다.
요약 해석(abstract interpretation)이라는 것은 영호가 했던 일을 컴퓨터 프로그램에 적용하는 것이라고 볼 수 있다. 주어진 프로그램이 어떻게 실행될 지를 정의해 주는 것을 프로그램의 의미(seman tics)라 한다. 프로그램의 실행을 정의하는 방법은 다양하지만 어떤 방법이든지 프로그램의 실행을 정의하는 데 필요한 값들이 돌아다니는 공간(이하 도메인)을 명확히 할 필요가 있다. 예를 들면, 계산식을 위해서는 정수 도메인이 필요하고, 포인터를 다루기 위해서는 메모리 주소를 원소로 가지는 도메인이 필요할 것이다. 또 대입문(assign ment statement)을 위해서는 주소에 값을 대응시키는 함수들의 집합인 메모리라는 도메인이 있어야 할 것이다.
요약 해석은 주어진 프로그램을 프로그램의 실제 실행을 정의하는 도메인 대신에 요약된 도메인(예를 들어 정수의 요약 도메인으로서의 홀수, 짝수 집합)에서 실행하면서 실제 프로그램이 실행 중에 가질 수 있는 값들을 모두 포섭하는 결과 값을 계산해내는 분석이라고 할 수 있다. 만일 요약 해석(abstract interpretation)이 요약 도메인 상에서의 프로그램 실행에만 관한 내용이라면 요약 해석은 하나의 아이디어에 지나지 않을 것이다. 요약 해석이 훌륭한 이유는 요약된 도메인에서 얻은 프로그램 실행의 결과가 실제 프로그램 실행의 결과를 온전하게 포섭하는 것이 보장되는 올바른 분석을 디자인할 수 있는 틀(framework)을 제공해주기 때문이다. 영호가 주어진 정수식의 답으로 짝수를 제시했는데, 이것이 옳다는 것(직관적으로는 옳지만)은 어떻게 증명할 수 있을까? 모든 정수식에 대해서 영호식의 계산법으로 얻은 답이 실제 계산식의 계산 결과를 포섭함을 증명하는 것은 답이 뻔히 보이는 간단한 문제는 아니다.
아이락 설계
아이락(Airac, Array Index Range Analyzer for C)은 이러한 요약 해석의 틀 속에서 설계하고 구현했다. 요약 해석의 틀 속에서 아이락이 프로그램의 실제 실행을 어떻게 요약하는 지 예를 통해 살펴보자. 아이락은 주어진 프로그램이 잘못된 배열 참조를 하는 경우가 있는 지 없는 지를 분석하는 것을 목표로 하고 있다. 그러므로 아이락이 사용하는 요약 도메인은 영호의 것처럼 홀수, 짝수만으로 이뤄져있어서는 제대로 된 분석 결과를 내놓지 못할 것이다. 아이락의 분석 목표에 맞는 수준의 요약 도메인이 필요한 것이다.
아이락은 프로그램에 있는 수식 값들의 요약 도메인으로 구간(interval)이라는 도메인을 이용한다. [a,b]로 표시되는 구간 도메인의 원소는 a보다는 크거나 같고, b보다는 작거나 같은 수들의 집합을 의미한다. 또 특별히 ∞ 기호를 이용해서 크기가 무한한 집합을 의미하는 구간을 나타낼 수도 있다. 즉 [ -∞, +∞ ]은 모든 수 전체를 의미하는 구간이 된다. 구간 도메인의 원소 간에는 순서(order)도 정의할 수 있다. 구간 a, b 간의 순서 ⊆는 구간 a가 구간 b에 포함되는 경우 a ⊆ b로 나타낸다. 그리고 모든 구간보다 작은 구간을 특별히 기호 ⊥로 나타낸다.
배열은 배열의 요약된 시작 주소, 배열의 크기 구간, 그리고 현재 포인터가 가리키고 있는 배열의 오프셋(offset) 구간을 가지는 값으로 요약된다. 메모리는 메모리가 할당된 프로그램 상의 위치로 요약된다. 이를 위해 아이락은 프로그램의 모든 식, 명령문, 선언 등에 고유한 레이블을 할당한다. 다음의 프로그램을 생각해보자.
int a[10], *p;
p = a + 3;
아이락의 요약 도메인에서 이 프로그램을 실행하고 나면 a는 쨦l0, [10, 10], [0, 0]쨧을, p는 쨦l0, [10, 10], [3, 3]쨧을 가지게 된다. 여기서 l0는 배열 선언 a[10]에 할당된 레이블이다. 아이락은 프로그램의 모든 배열의 크기와 그 배열 접근에 이용되는 인덱스의 값을 구간으로 요약한 후, 인덱스 구간이 크기 구간 외의 값을 가질 가능성이 있을 때 버퍼 오버플로우가 날 수 있다는 알람을 발생시킨다.
앞에서 예로 든 프로그램의 일부를 담고 있는 다음의 프로그램을 통해 아이락이 프로그램을 구간으로 요약하는 과정을 알아보자.
x = 0; ?
while(x<10) {
? x = x+1; ?
} ?
이 프로그램의 실행으로 프로그램의 각 지점(프로그램 포인트)에서 변수 x가 가질 수 있는 값(구간)은 무엇이 될까? 상식적으로 접근해보자. 우선 프로그램 포인트 ?에서 x는 x = 0;의 실행 결과로 0을 값으로 가질 것이다. 프로그램 포인트 ?에서는 프로그램 포인트 ?과 같은 값을 가질 것이고, 프로그램 포인트 ?에서는 x = x+1;의 실행 결과로 프로그램 포인트 ?보다 1 큰 값을 가질 것이다. 프로그램 실행 흐름은 여기까지 이른 후에 다시 프로그램 포인트 ?로 돌아가므로 프로그램 포인트 ?에서 x는 이제 0 또는 1의 값(구간으로 표현하면 [0,1])을 가진다고 할 수 있다. 이런 식으로 생각을 해보면 x는 프로그램 포인트 ?에서는 [0,10], 프로그램 포인트 ?에서는 [0,9], 프로그램 포인트 ?에서는 [1,10] 마지막으로 프로그램 포인트 ?에서는 [10,10]의 값을 가진다고 할 수 있을 것이다.
이 과정을 구현한 프로그램 분석기는 어떻게 만들 수 있을까? 이렇게 접근해보자. 우선 우리가 알고 싶은 것, 즉 각 프로그램 포인트에서 변수 x가 가질 수 있는 값을 미지수로 가지는 방정식을 세우자. 그리고 구간 도메인 상에서 이 방정식을 풀자. 그러면 그 방정식의 해가 바로 우리가 원하는 분석 결과가 될 것이다. 각 프로그램 포인트 ?에서 x가 가지는 값을 Xi라는 미지수로 표현하자. 프로그램의 실행 의미를 생각하면 다음과 같은 방정식을 만들어 갈 수 있을 것이다. 우선 자연어로 방정식을 표현해보자.
X1=[0,0] 또는 X3
X2=X1이면서 x<10을 만족 = X1에 포함되고 [-∞, 9]에도 포함됨
X3=X2에 [1,1]을 더함
X4=X1이면서 x>=10을 만족 = X1에 포함되고 [10, +∞]에도 포함됨
우리가 원하는 분석은 프로그램의 실제 실행을 포섭하는 것이어야 한다는 점과 분석 결과가 실제를 포섭하면서도 결과가 나타내는 집합의 크기가 작을수록 분석의 정확도가 높다는 점을 상기하자. “X1 = [0, 0] 또는 X3”에서 좌변을 [-∞, +∞]로 바꿔도 틀리지는 않다. 하지만 정확도는 가장 낮다고 할 수 있다. [-∞, +∞]은 모든 수의 집합을 의미하기 때문이다. 그러면 “[0, 0] 또는 X3”을 포섭하면서 가장 작은 값은 어떻게 나타내면 좋을까? 수학시간에 배운 합집합이 바로 우리가 원하는 답이다. 두 집합의 합집합은 둘을 포함하는 최소 집합이므로. 집합세계의 합집합을 구간으로 확장해서 ∪이라는 기호로 쓰자.
예를 들어 [1, 2] ∪ [2, 3]의 결과는 이다. “X1에 포함되고 [-∞, 9]에도 포함됨”은 집합세계의 교집합을 이용해서 나타낼 수 있을 것이다. 기호로는 ∩을 사용하자. 예를 들어 [1, 2] ∩ [2, 3]의 결과는 [2, 2]가 될 것이다. 구간 간의 덧셈은 ?로 쓰고, [a, b] ? [c, d] = [a+c, b+d]로 정의하자. 이 정의는 각 구간에 포함되는 모든 수들 사이의 덧셈 결과를 포함하는 최소 구간을 의미한다. 이제 자연어로 썼던 방정식은 다음과 같은 모양이 된다.
X1 = [0, 0] ∪ X3
X2 = X1 ∩ [-∞, 9]
X3 = X2 ? [1, 1]
X4 = X1 ∩ [10, +∞]
자, 이제 어떻게 풀어야 할지는 모르겠지만, 모양은 그럴 듯한 방정식을 얻었다. 이제 우리의 목표는 이 방정식의 해 중에서 구간 도메인의 순서 기준으로 가급적 작은 해를 구하는 것이다. 우리의 방정식을 조금 다르게 표현해보자.
(X1, X2, X3, X4) = F (X1, X2, X3, X4)
F (X1, X2, X3, X4) = ([0, 0] ∪ X3, X1 ∩ [-∞, 9], X2 ? [1, 1], X1 ∩ [10, +∞]
방정식을 이와 같이 바꿔 쓰면 우리가 원하는 해는 함수 F의 고정점(fixpoint)이라고 할 수 있다. 함수의 고정점이란 함수의 입력과 출력이 같게 되는 값을 의미한다. 즉, 함수 f에 대해 f(x) = x를 만족하는 x가 함수 f의 고정점이다. 만일 이런 가 둘 이상 있고 그들 간에 순서가 있다면 그 중에서 가장 작은 값을 최소 고정점(least fixpoint)이라고 한다. 특정 조건을 만족하는 경우 함수의 고정점을 구하는 기계적인 방법이 존재한다. 그 방법은 함수가 정의된 도메인의 최소 원소에 함수 적용 값이 변하지 않을 때까지 함수를 계속 적용하는 것이다. 함수 F의 k번 적용을 의미하는 Fk를 다음과 같이 정의하자.
F0(⊥, ⊥, ⊥, ⊥) = (⊥, ⊥ ⊥, ⊥)
Fn+1 (⊥, ⊥, ⊥, ⊥) = F(Fn(⊥, ⊥ ⊥, ⊥)) (n 쨧 0)
우리의 경우 Fk+1 (⊥, ⊥, ⊥, ⊥) = Fk(⊥, ⊥ ⊥, ⊥)이 될 때까지 k + 1번 함수 F를 적용하면 된다. <표 1>은 함수 F를 적용해 가는 과정을 보여주고 있다. k가 14인 경우 13일 때와 다른 값을 가지는 Xi의 값이 없음을 보여준다. 즉 함수 를 13번 적용해서 고정점에 도달했으며 이를 14번째 적용에서 확인한 것이다. 최종 결과가 앞서의 상식적인 접근으로 얻은 결과와 일치함을 확인하자. 이제 루프의 조건이 외부 입력으로 결정되도록 분석 대상 프로그램을 조금 바꿔 보자.
n = readint()
x = 0; ?
while(x
? x = x+1; ?
} ?
변수 n의 값은 외부 입력으로 결정되므로 어떤 값이든지 될 수 있다. 구간으로는 [-∞, +∞]에 해당한다. 이 프로그램에 대한 방정식은 다음과 같다.
X1 = [0, 0] ∪ X3
X2 = X1 ∩ [-∞, +∞] = X1
X3 = X2 ? [1, 1]
X4 = X1 ∩ [-∞, +∞] = X1
이 방정식의 답을 구하는 계산은 끝이 나지 않는다. 함수를 k(>1)번 반복 적용한 후의 X0은 [0, k-2]가 된다. 보통의 방법으로는 고정점에 도달하지 못하는 것이다. 어떻게 하면 될까? 우리의 목표가 실제 일어날 수 있는 상황과 정확히 일치하는 분석 결과를 얻는 것이 아니라 실제 상황을 포섭하는 분석 결과를 얻는 것이라는 점을 생각하면 해결책을 구할 수 있다. 해결책은 방적식의 답을 포섭하면서 구간이 커질 수 있는 횟수를 제한하는 것이다. 이를 넓히기(widening)라고 한다.
X1에 대해 [0, 0] ∪ [1, 1]의 값으로 [0, 1] 대신에 [0, +∞]을 취한다면 다음번 함수 적용에서도 [0, +∞]이 되므로 함수 적용을 멈출 수 있게 된다. 이런 넓히기를 적절히 이용하면 어떤 프로그램이 주어지더라도 항상 유한한 시간 내에 분석을 완료할 수 있게 된다. 하지만 넓히기를 불필요하게 많이 사용하면 분석의 정확도는 떨어지게 된다. 이를 방지하기 위해서는 넓히기를 적용하는 경우를 최소화하는 방법과 넓히기로 인해 떨어진 정확도를 보정할 방법이 필요하다. 넓히기는 while 등의 반복문, 재귀 함수 등으로 생기는 루프의 시작점에서만 적용하면 된다. 사실 루프의 반복 횟수가 유한하다면 굳이 넓히기를 사용하지 않아도 유한한 시간 내에 분석을 끝낼 수가 있다.
그러나 루프의 반복 횟수가 유한할 지의 여부를 결정할 일반적인 방법은 없기 때문에, 모든 루프에 대해 넓히기를 적용해야만 항상 유한한 시간 내에 분석이 끝남을 보장할 수 있다. 그리고 여기서는 소개하지 않겠지만, 넓히기 후에 좁히기(narrowing)를 적용하면 넓히기로 떨어진 정확도를 상당 부분 보정할 수 있다. 아이락은 프로그램의 요약 도메인 설계, 프로그램으로부터 방정식을 도출하는 방법과 방정식의 해를 구하는 방법 등을 요약 해석이 제시하는 프레임워크 내에서 설계하고 구현하였다. 따라서 아이락은 ‘프로그램의 분석 결과가 프로그램의 실제 실행에서 일어날 모든 상황을 포섭함’을 보장받게 된다.
아이락 분석 예
이제, 아이락이 실제 소프트웨어에서 찾아내는 오류들을 살펴보자
리눅스 커널 2.6.4 장치 드라이버
리눅스 커널 2.6.4의 USB 모뎀 드라이버와 관련된 /drivers/usb/ class/cdc-acm.c 파일의 일부분이 다음과 같다.
static struct acm *acm_table[ACM_TTY_MINORS];
...
static int acm_probe (struct usb_interface *intf,
const struct usb_device_id *id)
{
...
for (minor = 0; minor < ACM_TTY_MINORS && acm_table[minor]; minor++);
if (acm_table[minor]) {
err(“no more free acm devices”);
return -ENODEV;
}
...
acm_table[minor] = acm;
...
}
acm_table이라는 배열이 ACM_TTY_MINORS의 크기로 선언되어 있다. acm_probe라는 함수의 한 부분에서 for를 돌면서 acm_table에서 0인 곳을 찾는다. 그리고 그 뒤에 이 칸을 채우는 일을 하는데, for 바로 다음부터 프로그래머가 실수를 한 것으로 보인다. for를 돌면서 minor 변수는 0부터 ACM_TTY_MINORS-1까지의 값을 가질 수 있다. 이 구간에 속한 minor 값으로 ACM_TTY_ MINORS 크기의 acm_table 배열을 접근하는 것은 올바른 코드이므로 아이락은 for의 조건에 대해서는 경보를 내지 않는다. 그러나 for가 끝난 뒤부터는 minor가 ACM_TTY_MINORS의 값을 갖거나 mi nor가 [0, ACM_TTY_MINORS]의 값을 갖고 acm_table [minor]가 0을 갖는다.
아마도 이 부분을 짠 프로그래머는 for가 끝난 뒤에도 acm_ table[minor] 칸이 0이 아니라면 원하는 minor 값을 찾지 못한 것이므로 오류 값을 돌려주려는 의도였을 것이다. 하지만 acm_table에서 값이 0인 칸을 찾지 못한다면 minor는 무조건 ACM_TTY_MINORS라는 값을 가지며 이러한 인덱스로 acm_table을 참조하면 안 된다는 사실을 간과한 모양이다. 아이락은 [0, ACM_TTY_MINORS]의 값을 갖는 minor로 크기가 ACM_TTY_MINORS인 acm_table 배열을 접근할 수 있다고 for 다음에 나온 모든 관련 코드에 대해서 경보를 낸다.
GNU tar의 rmt.c
앞서 설명한 리눅스 커널의 예와 비슷한 경우다. GNU tar 1.13의 src/rmt.c의 125번째 줄에 다음과 같은 get_string 함수가 있다.
main (int argc, char *const *argv)
{
...
char device_string[STRING_SIZE];
get_string (device_string);
...
}
static void
get_string (char *string)
{
int counter;
for (counter = 0; counter < STRING_SIZE; counter++)
{
if (safe_read (STDIN_FILENO, string + counter, 1) != 1)
exit (EXIT_SUCCESS);
빠뜨린 예외 처리
다음은 실제로 제품에 사용됐던 어떤 임베디드 소프트웨어의 일부분이다.
static EVENTQUEUE *_inputQueue[MAX_NUM_QUEUE];
...
int ew_Os_CheckInputEvent (ULONG qid, EVENT *pEvent) {
int curQ = ew_GetQueue( qid );
if( curQ < 0 )
return ERR_FATAL;
if( _inputQueue[curQ]->getPos >= DF_MAX_EVENT_ITEM )
return ERR_FATAL;
...
}
int ew_Os_UpdatePos (ULONG qid, int type, int x, int y) {
int curQ;
curQ = ew_GetQueue( qid );
if((_inputQueue[curQ]->eventItem[_inputQueue[curQ]->getPos]).type != type)
return ERR_FATAL;
...
}
int ew_GetQueue( unsigned long qID ) {
int i = qID - QID_SEED;
if( _inputQueue[i] == NULL_Q ) return -1;
if( i >= MAX_NUM_QUEUE || i < 0 ) return -1;
return i;
}
ew_GetQueue는 배열의 인덱스를 돌려주는 함수인데, 어떤 상황에는 예외를 의미하는 -1을 돌려주기도 한다. ew_GetQueue를 사용할 때에는 프로그래머가 예외의 경우인지 먼저 검사한 뒤에 정상적인 경우에만 배열 참조에 그 결과를 사용해야 하는데, 이를 실수로 빠뜨리고 프로그램을 짜는 경우가 생긴다.
아이락은 앞의 ew_GetQueue라는 함수가 [-1, MAX_NUM_ QUEUE-1]의 값을 돌려준다는 것과 _inputQueue 배열의 크기가 MAX_NUM_QUEUE라는 사실을 분석해낸다. ew_Os_CheckInput Event 함수 안에서 ew_GetQueue의 결과를 담은 curQ가 0보다 작은 경우에는 함수를 끝내므로 그 아래를 진행할 때에는 curQ가 [0, MAX_NUM_QUEUE-1]의 값을 가진다는 사실을 안다. 따라서 curQ를 _inputQueue의 인덱스로 사용하는 것에는 아무런 문제가 없으므로 아이락은 여기서 경보를 내지 않는다. 그러나 ew_Os_ UpdatePos 함수에서는 ew_GetQueue가 돌려준 [-1, MAX_NUM_ QUEUE-1]의 값 그대로 _inputQueue를 참조할 수 있기 때문에 아이락이 오류가 발생할 수 있다고 경보를 내며 배열의 크기와 인덱스 값을 알려준다. 아이락은 이렇게 프로그래머가 실수로 예외처리를 빠뜨린 경우를 정확히 찾아준다.
앞에서 소스코드와 함께 소개한 분석 결과를 살펴보면 프로그래머가 만들어내는 오류들은 그 형태가 의외로 간단하다. 그러나 이렇게 간단한 구조의 오류들이라도 전체 프로그램 코드가 매우 큰 경우에는 사람의 손으로 찾아내기가 결코 쉽지 않다. 프로그래밍이란 아주 작은 실수에도 깨질 수 있는 매우 섬세한 조각들을 서로 정교하게 이어 붙여서 원하는 일을 하는 구조물을 만드는 작업이다.
어느 한 부분이 살짝이라도 어긋나 있다면 구조물 전체를 와르르 무너뜨리는 것이 바로 프로그램의 버그다. 해야 할 일이 명확하며 이를 비교적 체계적으로 구현한 프로그램에서 어긋난 부분들이란 앞서 살펴본 예들과 같이, 보통 사소한 실수에서 비롯되기 마련이다. 사소한 실수들이지만 커다란 프로그램의 구석구석에 숨어있다면, 이를 찾아내는 데에는 그 구조물을 만들어내는 것보다도 더 큰 노력이 필요할 수 있다. 아이락은 이렇듯 사소한 실수로부터 비롯되는 치명적인 문제들을 자동으로, 빠뜨림 없이, 그리고 실행 전에 찾아준다.
아이락의 분석 속도와 정확도
GNU 프로그램, 리눅스 커널과 상용 임베디드 소프트웨어를 대상으로 한 아이락의 분석 결과는 <표 2>와 같다. 펜티엄 4 3.2GHz CPU와 4GB 메모리를 가진 시스템에서 아이락을 돌린 시간이다. 줄 수는 전처리하기 전 C 프로그램의 줄 수이다. 경보 수에서 배열은 경보를 낸 대상 메모리 영역 또는 배열의 수이며, 접근은 그 대상들을 잘못된 인덱스로 참조한 위치의 모두 센 것이다.
이 결과에서 분석 속도는 초당 평균 10줄 정도로 컴파일 시간 등과 비교해볼 때 별로 빠르지 못하다. 그러나 6000줄짜리가 1초도 안 되서 끝나는가 하면, 1200줄짜리가 45초가 넘게 걸리는 등 프로그램이 하는 일에 따라 분석 속도의 편차가 심하다. 물론 개선의 여지는 항상 남아있지만, 아이락이 모든 경우를 다 포함하는 결과를 만들어준다는 사실을 생각해보면 테스트를 통한 검증과는 비교가 안될 만큼 빠른 속도라고 생각할 수도 있겠다.
분석 정확도는 찾아낸 총 1199개의 접근 오류 중에서 199개가 실제 오류로 16.6%이다. 경보가 나오면 이들이 실제 오류인지 아닌지는 사람이 직접 그 진위 여부를 확인해야 한다. 가령, Es* 소프트웨어의 경우를 보자. 162개의 경보 중에서 겨우 6개의 실제 오류를 발견하기 위해 나머지 156군데를 살펴봐야하는 헛수고를 해야만 한다고 생각할 수 있다. 그러나 23만 줄의 프로그램 코드 전체를 살펴보는 대신에 아이락이 짚어준 162 군데만 살펴보면 된다. 실제로 발생할 수 있는 모든 잘못된 배열 참조 문제를 이 162군데만 확인함으로써 찾아낼 수 있다는 것이다. 정확도를 단순히 실제 오류와 경보 수의 비로만 생각할 것이 아니라, 분석한 프로그램의 크기까지도 고려하여 그 효용성을 판단해야 할 것이다.
아이락의 한계
아이락 같은 안전한 프로그램 분석기에서는 분석 속도와 정확도 간의 균형이 상당히 중요하다. 대다수의 경우에 정확도를 높이려다 보면 분석 시간이 늘어나고 분석 속도를 높이려다 보면 정확도가 떨어진다. 아이락의 경우 <표 2>를 보면 알 수 있듯이 사용자가 프로그램을 분석하여 바로바로 분석 결과를 확인하고 이를 바탕으로 디버깅을 할 수 있는 수준의 분석 속도를 갖고 있지는 못하다. 하지만 테스팅을 통해 디버깅하는 과정과 비교해 생각해보면 이 정도의 시간 안에 모든 버그를 빠뜨림 없이 찾아낸다는 것은 유용할 수 있다. 안전한 프로그램 분석기의 분석 결과에는 허위 경보(false alarm)가 들어가지 않을 수가 없다. 허위 경보는 실제로 버그가 아닌 곳을 버그라고 하는 것이다. 안전하게 모든 것을 포섭해서 분석을 하려다 보면 요약하는 과정을 피할 수 없고, 그런 요약은 분석의 정확도를 떨어뜨릴 수밖에 없다. 다음의 코드를 보자.
s=0;
for(i=0;i
s += i;
}
이렇게 간단한 프로그램을 분석한다고 했을 때 변수 i가 변수 bound가 가지는 값이라는 사실은 정확히 분석할 수 있지만, 변수 s가 0부터(변수 bound가 가지는 값) - 1까지의 합이라는 것을 정확히 분석하기란 매우 힘들다. 요약 해석의 결과로는 s가 0이상의 수라는 사실 밖에는 알아내지 못한다. 물론 더 구체적인 수를 알아내기 위해서는 더 많은 분석 시간을 사용하면 된다. 하지만 만약 bound가 프로그램의 외부 입력과 같이 모르는 값이라면 어떻게 해야 할까? 안전한 분석을 위해서는 그 모르는 값이 모든 정수라는 가정 하에 분석해야 한다. 모든 정수를 실제 정수들로 표현하면 무한하기 때문에 요약 없이는 분석이 유한한 시간에 끝날 수 없다. 요약은 이렇게 필수적이고 그래서 허위 경보들이 나오는 것이다. 그런데 너무 많은 허위 경보는 분석기의 사용자를 지치게 한다. 경보가 난 몇 군데를 계속 살펴봤는데 모두 실제로는 버그가 아니었다고 판단이 든다면 사용자는 분석기를 믿지 못하게 된다.
이런 허위 경보를 줄일 수 있는 하나의 방법으로 우리는 스팸메일을 걸러내는 방법과 유사한 베이지안 통계 분석(Bayesian statistical analysis)을 사용했다. 실제 스팸메일인 경우들을 어느 정도 알고 있는 상태에서 메일을 받았을 때 그것이 가지고 있는 여러 가지의 증상(symptom)들을 보고 실제로 스팸메일일 확률을 계산하여 분류할 수 있다. 우리도 실제 버그인 곳들을 알고 있는 상태에서 어떤 경보가 나왔을 때 그곳이 가지고 있는 여러 가지의 증상들을 보고 실제 버그일 확률들을 통계적으로 계산해 낼 수 있다. 여기서 증상이라는 것은 경보가 나온 곳이 가지고 있는 문법 구조, 실행 흐름, 분석 중에 나타나는 성질 등 이외에도 특성으로 삼을 수 있는 모든 것들이 될 수 있다.
이 방법의 장점은 분석 결과로 나오는 경보들을 실제 버그들과 허위 경보들로 분류한 정보를 많이 제공하면 할수록 다음 예측이 정확해진다는 점이다. <그림 1>의 그래프는 이 방법을 통해 아이락의 분석결과들이 실제 버그일 확률에 따라 실제 버그들과 허위 경보들의 개수를 그린 것이다.
허위 경보의 분포만을 보면 비교적 바람직한(실제 버그일 확률이 낮을수록 많아지는) 모습을 보여준다. 실제 버그의 경우에는 안타깝게도 확률에 따라 분포하는 모습을 보이지 못하는데, 이는 실제 버그에 대한 정보가 적고 허위경보에 대한 정보만 많기 때문일 거라고 추측하고 있다. 사실 실제 프로그램들에서 실제 버그들을 많이 찾아내기란 쉬운 일이 아니다. 모두들 버그 없는 프로그램들을 짜려고 노력하고, 또 오픈소스들에서는 아직 개발 중인 소스보다 버그가 더욱 드물게 발견된다. 이렇게 실제 버그일 확률을 계산함으로써 우리는 사용자에게 어떤 버그들을 먼저 보여줄 지를 랭킹을 정할 수 있다. 실제 버그일 확률이 높은 경보들을 우선적으로 보여줌으로써 사용자들이 허위 경보에 지치는 것을 최대한 막을 수 있다.
앞으로의 방향
일반적으로 프로그램 분석기란 프로그램이 가질 수 있는 성질을 알아내는 프로그램이다. 그 프로그램 성질 중에 아이락이 관심 있는 성질은 ‘C 프로그램에서 스택이나 힙에 할당될 수 있는 메모리가 항상 처음에 할당되었던 크기 안에서만 사용되는가’이다. 명확히 정의될 수 있는 프로그램의 성질은 모두 분석기의 분석 대상이다. 예를 들어 ‘이 프로그램은 항상 끝나는가’, ‘동적으로 할당되었던 메모리들은 프로그램이 끝나기 전에 모두 해제(free)되는가’, ‘이 프로그램이 실행 중에 사용하는 메모리의 최대 크기는 어느 정도인가’ 등이 프로그램의 성질이 될 수 있다. 따라서 이런 프로그램 성질을 알아내는 분석기는 아이락에서와 마찬가지로 요약 해석 방법을 통해 모두 구현 가능하다.
모든 프로그래밍 언어는 그 언어로 짜여진 모든 프로그램의 의미를 정확히 정의할 수 있기 때문에 모두 분석 대상 언어가 될 수 있다. 즉 앞에서 소개된
C 언어로 변환하는 과정만 구현한다면 C가 아닌 다른 그 어떤 언어도 아이락의 분석 대상 언어가 될 수 있다. 정확도와 분석 속도도 여러 가지 기술들을 이용하여 개선이 가능하다. 앞으로 다양한 프로그램 성질들을 알아낼 수 있는 분석기를 만들려고 하고 있으며, 이와 동시에 분석 대상이 되는 언어도 확장하고, 분석 속도와 정확도를 높이는 방법들에 대한 연구도 진행하고 있다.
분석기 구현은 올바름을 확인하는 작업
실제로 아이락을 구현하면서 처음에 겁도 없이 확인하지도 않고 계단을 밟아 올라가다가 결국 허공을 딛고 굴러 떨어져 처음부터 다시 분석을 디자인하는 허무함을 맛보았었다. 분석기를 만드는 사람은 항상 자신이 하고 있는 작업이 올바른 것인지 끊임없이 확인해야 한다. 그렇지 않으면 자신이 구현한 분석기가 옳다는 것을 증명하지 못할뿐더러 잘못된 결과를 내는 분석기를 만들어 낼 수 있다. 분석기의 정확도, 분석 속도의 향상은 분석기가 올바르다는 전제하에서만 의미가 있다. 올바름을 확인하는 작업은 자신이 무엇을 하고 있는 지 수학적으로 명확히 기술해보는 것에서부터 출발한다.
수안이의 컴퓨터 연구실
Leave your greetings.