안전한 정적 분석과 시대정신
들어가며
“시대정신”이라는 말이 있다. 특정한 시대에 큰 영향을 끼치는 중요한 가치를 일컫는다고 한다. 독일의 철학자 헤겔이 그 개념을 처음 고안한 이래 지금까지 이어져 매 선거철이면 우리 귀를 자주 간지럽힌다.
지난 4월 헤겔의 나라에서 이메일을 한 통 받았다. “현대 SW공학과 안전한 정적 프로그램 분석(Sound Static Program Analysis in Modern Software Engineering)”이라는 주제로 닥스툴 세미나(Dagstuhl Seminar)가 열리는데 참가하지 않겠느냐는 초청장이었다. 닥스툴 세미나는 독일의 작은 마을인 닥스툴의 닥스툴 성(Schloss Dagstuhl)에서 정기적으로 열리는 전산학 분야 전문가들의 모임이다. 일년 내내 각 분야별 다양한 주제로 세미나가 열리는데, 초청받은 연구자들이 모여 3-5일간 집중적으로 토론하고 교류하는 자리다. 닥스툴 세미나가 즐거운 자리라는 것을 익히 들은적 있는데다가, 특히 주제도 매우 마음에 들어서 단숨에 참가한다고 답장을 보냈다.
현대 SW 개발에서 정적분석은 빠질 수 없는 필수 요소가 된지 오래다. 특히, 안전성(soundness)이 보장되는 정적 분석기는 프로그램의 올바름을 증명할 때 필수이다. 정적 분석에서 안전성이란 프로그램의 실제 실행의미를 모두 포섭하도록 분석하는 성질을 뜻한다. 분석기가 실행의미를 모두 포섭하면서 샅샅이 훑어봤는데도 오류가 없는 것으로 밝혀지면 그 프로그램은 올바른 것이다. 가령, 어떤 변수 x의 값이 프로그램 실행 중에 항상 10 이상이라고 하자. 안전한 정적 분석기는 이러한 실제 값을 모두 포섭하면서 x의 값을 실행 전에 예측한다. 예를 들어, x의 값이 “양수”라고 예측한다면 이는 안전하게 실제를 모두 포섭한 것이다. 양수는 10 이상인 수를 모두 포함하므로. 이러한 예측 결과가 있으면, “1/x”이라는 식이 0으로 나누는 오류가 없음을 증명할 수 있다. 예측 결과 “x”는 양수이므로 0이 될 수 없기 때문이다. 실제를 포섭하는 예측 결과로도 오류 발생 가능성이 없다는 것을 보였으니, 실제 실행에서도 당연히 오류가 없을 것임이 자명하다. 증명 끝. 테스팅으로는 유한 시간안에 구석구석 숨어 있는 모든 오류를 찾아낼 수 없기 때문에, 크고 복잡한 시스템 개발에서 이러한 정적 분석은 아주 유용하다. 따라서 SW의 안전성이 매우 중요한 시스템(예: 항공기 제어, 운영체제, 의료기기 등)에서는 안전한 정적 분석기가 필수적이다.
하지만, 안전한 정적 분석이 안전필수 SW가 아닌 일반 응용SW 개발에서 얼마나 실용적인가에 대해서는 여러 의견이 많다. 실행의미를 모두 포섭하기는 하지만 실제가 아닌 상황까지 고려하는 경우도 있다는 문제 때문이다. 너무 보수적으로 프로그램을 분석하다보면 실제 오류가 아닌데도 오류라고 판단하는 경우가 생긴다. 가령, 어떤 변수 x의 값은 실제로 항상 양수만 가능한데도, 분석기가 보수적으로 “0보다 같거나 큰 수”라고 판단하는 경우도 있다는 뜻이다. 그렇다면 “1/x” 같은 식이 있을 때, 분석기는 x가 0이 될 가능성도 있다고 잘못 판단하여 “0으로 나누기 오류”를 보고할 것이다. 이른바 허위경보(false alarm)이다. 안전하지만 허위경보가 절대 없는 정적 분석기를 만드는 것은 이론적으로 불가능하다는 것이 이미 증명되어 있다. 그리하여 사람들은 허위 경보 비율을 줄이기 위해 종종 안전성을 포기하는 선택을 하곤 한다. 그러다보면 당연히 실제 오류를 놓치는 경우도 발생하기 마련이다. 따라서 허위경보와 놓치는 오류 사이에서 적절한 균형을 찾는 여러 기술을 많은 이들이 개발하고 있다.
이번 닥스툴 세미나의 주제는 이른바 “안전한 정적 분석의 시대정신”“을 논하자는 것으로 들렸다. 현대 소프트웨어 개발 현장에서 필요로 하는 정적 분석은 어떤 모습이어야 하는가? 지난 50년간 이 분야가 걸어온 길은 어떠하며, 앞으로는 어떤 방향으로 나아가야 하는가? 우리 연구실도 이에 관해 오랫동안 고민하던 차였다. 마침 최근 재미있는 성과도 나오고 있는 터라 우리 이야기를 들려주면 아주 딱이겠다 싶었다. 참가자들의 전문 분야도 다양해서 사람들이 어떤 반응을 보일지도 무척 궁금했다. 새로운 모험을 떠나는 기분으로 독일행 비행기에 올랐다.
닥스툴 가는 길
모험은 역시 멀고 험난한 법. 전에 닥스툴에 다녀온 분들과 이야기할 때면, 하나같이 빠지지 않는 말이 있었다. 바로 외진 시골 마을이라는 점. 교통이 불편하다고들 했다. 가기 전까지 그저 도시사람(서울사람)들의 엄살이라고 여겼다. 안내서를 보니 프랑크푸르트 공항에서 기차와 택시를 타고 한참 가야한다고 되어 있다. 시간이 좀 걸리기는 한데, 기차와 택시로 갈 수 있는데 웬 엄살인가?
막상 가보니 뒤통수가 얼얼했다. 택시를 타면 갈 수 있다고 했지, 택시를 항상 탈 수 있다고는 하지 않았다는 점을 놓쳤다. 한국에서 독일로 가는 비행기는 보통 독일 시간으로 저녁에 도착하고, 하필 내가 도착한 날은 일요일인 것이 문제였다. 안내서에 적힌 여러 경로 중, 나는 St. Wendel 역에서 택시를 타는 방법을 골랐다. 프랑크푸르트 공항에서 St. Wendel 역까지는 기차로 약 두 시간 걸리고 역 앞에는 정류장이 있으니 거기서 버스나 택시를 타면 된다고 했다. 구글 스트리트 뷰로 미리 역 주변을 살펴보니 정류장도 있고, 역 바로 앞에 건물도 보이는 흔한 마을이었다. 인터넷 검색을 해보니 내가 잘 아는 교수님들의 여행기가 몇 편 보였는데, 다들 St. Wendel 역에서 택시나 버스를 탔다고 하는 것도 안심이 되었다. 안내서에는 다른 역(Türkismühle)에 내리는 경로를 더 추천하긴 했지만, 그 쪽은 역 주변에 대중 교통이 없다며 미리 택시를 예약하라고 되어 있었다. 귀찮았다. 뭐 얼마나 대단한 오지라고? 기차가 다니는 마을인데? 그냥 St. Wendel으로 내질렀다.
St. Wendel 역에 가까워질수록 분위기가 심상치 않다. 창밖에는 아무것도 안보인다. 컴컴하다. 사람들은 거의 다 내렸다. 내리기만 한다. 기차 안에는 나밖에 없다. 밤 9시 반쯤 역에 내리니 작은 마을이 보이지만, 사람은 보이지 않는다. 정류소는 있지만, 버스도 택시도 없다. 역앞 도로가 마을에서 제일 큰 길로 보이지만 드문드문 차가 지나갈 뿐이다. 작은 별의 어린왕자가 이런 삶이겠구나 싶다.
기다려도 오지 않는 택시를 포기하고 방법을 찾아 나서야 했다. 지나가는 가족이 있어 붙잡고 도움을 청해보았다. 고마운 독일인들은 흔쾌히 길가에 서서 직접 택시 회사도 알아봐주고 전화도 해주었지만 어디도 전화를 받지 않았다. 밤은 점점 깊어가고, 어디 호텔이라도 잡아서 다음날 가는 수 밖에 없다고 생각하던 차에 문 닫을 준비를 하는 술집이 보였다. 마지막 희망을 걸고 들어가 사정을 이야기했다. 영업을 마무리하던 친절한 독일 청년은 어딘가에 전화를 걸어서 한참 통화를 했다. 2분 후에 택시가 온다는 반가운 소식. 곧 산신령같은 외모를 지닌 할아버지 택시기사가 도착했고, 칠흑같은 산골짜기를 지나 닥스툴 성에 도착했다. 도착해보니 밤 11시 무렵. 다들 저녁을 먹고 숙소로 들어간 듯했고, 남아서 맥주를 마시던 두세명이 반갑게 맞아주었다. 합류해서 맥주 한 잔을 들이켰다. 평화가 물밀듯 밀려왔다.
그 밤의 고생이 당황스럽긴 했지만, 처음 며칠간 사람들과 안면을 트는 데에 유용한 이야깃거리로 쓰였다. 이야기를 들은 사람들의 반응은 한결같았다. “아니 왜 택시 예약 안했어요?” 안내서에 예약 안하는 선택지도 있었으니까. 역시 선택지 많은게 항상 좋은 것은 아니다.
다음 번에 닥스툴로 가는 이들을 위해 명심 사항을 정리한다. 비슷한 고생이 없길 바란다.
- 독일 기차 앱을 미리 준비하여 예매. 프랑크푸르트 공항에서 기차표 파는 자판기만 있는데 찾기도 쓰기도 어려움.
- 프랑크푸르트에서는 광역이 아니라 지역 기차를 타야하는데 길 찾기가 어려움. 지하철 아닌가 싶은 플랫폼으로 내려가서 타야함.
- 택시는 미리 예약. 안내서에서 가장 추천하는 Türkismühle 역에서 내려서 예약한 택시를 타는 방법이 가장 안전.
- 현금 충분히 준비. 택시는 카드가 안됨.
- 세미나를 마치고 공항으로 돌아갈 때는 참가자들과 함께 갈 수 있도록 세미나 주최측에서 도와줌.
| 우여곡절 끝에 밤늦게 도착한 닥스툴 성 |
닥스툴 성
닥스툴 성은 1700년대에 지어진 오래된 성이다. 현재는 개조, 보수하여 전산학 세미나 센터로 사용되고 있다. 이 센터의 운영은 라이프니츠 정보과학 연구소(Leibniz Center for Informatics)에서 맡고 있다. 우리가 잘 아는 그 수학자 라이프니츠의 이름을 딴 기관이다. 이번에 가서 알았는데, 전산학자들의 많이 쓰는 서지 관리 시스템인 DBLP도 이 연구소에서 운영하고 있었다. 매 주 한두개 세미나가 일년 내내 열리는 듯 했다. 우리 세미나가 열린 주에도 다른 세미나가 동시에 진행되고 있었다.
독일 정부의 지원을 받아서 참가자들에게는 굉장히 저렴한 비용으로 숙식을 제공한다. 숙소는 대학 기숙사 같은 느낌인데, 소박했지만 불편함은 없었다. 식사도 성 안에 있는 식당에서 급식처럼 제공되었다. 독일의 가정식(혹은 독일 학생들의 급식)이 이런 것인가 싶은 느낌이었다. 그 이외에 물, 맥주, 와인, 과자 등은 언제든 각자 가져다 먹고 스스로 정산서에 기록한 후, 퇴실할 때 한꺼번에 계산하는 방식이었다.
닥스툴 성은 주변이 온통 숲과 산으로 둘러싸인 외진 곳에 위치해 있다. 주변 자연 경관이 좋을 것 같아서, 달리기를 해볼까 운동화를 챙겨갔지만 헛수고였다. 해가 너무 늦게 뜨고, 일찍 질 뿐더러, 건물 근처를 제외하고는 말그대로 칠흑같은 어둠이라서 나가 뛰어다닐 곳이 없었다. 봄이나 여름이었으면 어땠을지 궁금하다.
| 닥스툴 성 | 하리보의 나라에 온것을 환영하는 침대 |
| 독일 가정식 같았던 음식 | 무인매장식 운영 |
세미나 개요
우리 세미나는 월요일 아침부터 금요일 점심까지, 매일 오전 9시부터 오후 6시까지 밀도있게 진행되었다. 참가자들의 연령대도 다양했다. 70년대에 박사학위를 받은 분부터, 지금 박사과정에 있는 학생까지. 50년 세월이 모였다. 각 참가자들이 20-30분 정도로 각자 발표하는 것 이외에도, 여러 주제에 관해 토론하는 시간이 많았다. 무작위로 조를 짜서 특정 주제에 관해 토론하는 시간, 이론팀(theory)과 현실팀(practice)으로 나누어 상대팀 사람들과 한명당 10분씩 이야기하는 스피드 데이트 시간을 통해서 참가자들의 연구 방향과 서로 다른 시각을 엿볼 수 있었다. 또한, 매 식사 시간에는 각 식탁에 참가자들이 무작위로 배치되기 때문에 자연스럽게 여러 사람들과 교류할 수 있었다. 매일 저녁에는 맥주와 치즈가 제공되었고, 탁구, 당구, 다트, 보드게임 등으로 즐거운 시간을 보냈다.
| 참가자들이 선정한 토론 주제 후보. 정적 분석 분야의 오랜 문제와 새로운 문제가 모두 모였다. |
지향성 프로그램 분석: 의심에서 확신으로(Directed Program Analysis: from Suspicion to Witness)
초대장에 적힌 세미나 취지를 읽고는 반가웠다. 같은 고민을 하던 우리 연구실의 연구 방향과도 결이 맞았다. 우리가 하고 있는 일을 소개할 좋은 발표 제목을 생각하다가 위와 같은 제목을 골랐다. 기존 정적 분석이 오류 의심에서 멈추었다면, 우리는 의심을 뛰어넘어 확신에 이르는 결론을 내놓겠다는 포부였다. 긴 여정의 마지막날 마지막 발표 순서인 것이 아쉬웠지만, 그래도 많은 사람들이 관심을 가졌고 여러 질문이 이어졌다. 발표 슬라이드는 여기에서 볼 수 있다.
앞서 언급한 허위 경보 문제는 정적 분석이 안고 있는 근본적인 숙제이다. 오랜 시간 동안 수많은 연구자들이 여러 접근법을 시도해왔다. 크게 세 가지 방향으로 나누어 볼 수 있다.
- 안전성을 유지한 채 더욱 정교한 분석을 설계하여 허위 경보를 줄이려는 방향. 정교한 분석을 현실적인 비용으로 실현하는 것이 관건.
- 안전성을 포기하고 허위 경보를 줄이려는 방향. 안전성을 포기하면서도 놓치는 오류가 적은 분석을 설계하는 것이 관건.
- 안전성을 유지하되, 사용자를 위해 분석 결과를 후처리하는 방향. 후처리의 정교함과 효율성, 설명가능성이 관건.
세 가지 방향 모두가 현실에서 매우 중요하다. 나같은 경우, 박사 과정 중에는 1번과 2번 방향을 주로 연구했고, 졸업후 지금까지는 3번 방향을 주로 연구하고 있다. 발표 주제도 그래서 3번 방향에 초점을 맞추었다. 마침 조별 토론의 주제 중에도 이 방향과 밀접한 “정적 분석 결과의 설명가능성(사용자 편의성)”이 있었다. 토론보다 내 발표가 먼저 있었으면 좋았겠지만, 발표 홍보 기회로 삼기로 했다. 토론 과정에 나온 내용에 맞게 발표 내용을 일부 보완하기도 했다.
조별 토론의 초점은 어떻게 하면 일반 개발자(정적분석 비전문가)에게 정적 분석 결과를 잘 설명할 수 있겠냐는 것이었다. 정적 분석기의 동작이 프로그램의 실행 과정과 다른 경우가 많기 때문에, 일반 개발자들이 결과를 이해하기 어려워하는 경우가 많다. 또한, 반대로 개발자들이 분석결과를 검토하면서 내린 결론(예: 오류 진위 여부)을 다시 분석기가 이해하도록 만드는 것도 중요하다. 이 문제를 해결하기 위해서, 우리 연구실에서는 개발자와 분석기가 손쉽게 상호작용하는 알람 랭킹 시스템을 연구한 적이 있다. 이 시스템은 정적 분석 결과로 나온 오류 후보 지점을 의심도 순으로 정렬하여 개발자에게 편의를 제공하고, 개발자가 검토한 결과를 다시 분석기에 반영할 수 있게 한다. 분석 결과에 관한 자세한 설명은 없지만, 적어도 의심도 순으로 정렬된 목록을 제공한다는 점에서 유용하다. 이를 이용하면 여러 오류 의심 지점이 존재할 때, 고효율 저비용으로 주어진 시간안에 많은 오류를 찾아낼 수 있다. 하지만, 여전히 개별 오류 의심 지점에 대한 설명가능성 문제는 남아 있었다.
반면, 이 발표에서는 어떻게하면 설명을 잘할 것인지가 아니라, 어떻게하면 설명을 안해도 되는지를 이야기하고 싶었다. 의심스러운 오류 후보 지점을 개발자에게 그냥 전달하는 대신, 실제 오류를 증명하는 증거(즉, 오류 유발 입력)를 잘 찾는 방법을 소개하고자 했다. 개발자에게 오류 유발 입력보다 더 좋은 설명은 없기 때문이다. 이를 실현하고자 하는 것이 이른바 지향성 프로그램 분석(Directed Program Analysis)이다. 정적 분석기가 오류 의심 지점을 찾아내면, 각 오류 의심 지점 별로, 해당 지점에서 발생하는 실제 오류 유발 입력을 효과적으로 찾는 기술이다. 이러한 입력을 효과적으로 찾으려면, 정적 분석기가 오류 의심 지점을 찾을 때 사용한 내부 정보를 잘 활용해야 한다. 하지만 이러한 과정은 개발자에게 직접 드러나지는 않고, 오직 마지막에 도출된 오류 유발 입력만이 개발자에게 전달된다. “확실하지 않으면 승부를 걸지 말라”는 영화 <타짜>의 격언과 맞닿아 있다.타짜>
발표에서는 이러한 지향성 프로그램 분석의 개념과 연구실에서 개발한 세 가지 적용 사례를 소개했다. 아이디어도 재미있어 했지만, 현실 세계에서 널리 쓰이는 SW에 있는 실제 오류를 찾아냈다는 점에서 관심을 많이 받았다. 연구실 학생들이 이루어낸 성과가 자랑스러웠다. 발표에서 소개한 각 사례는 다음과 같고, 구체적인 이야기는 해당 링크에서 살펴볼 수 있다.
| 마지막 날 마지막 발표 중 |
기록정신
닥스툴 세미나의 운영에서 매우 인상적이었던 점은 기록정신이었다. 세미나 기간 동안 모든 발표와 토론 내용은 함께 기록했다. 각 발표자는 발표 전후로 요약문을 공책에 직접 기록했고, 세미나 후에는 웹 시스템에 올려서 공유했다. 토론시에도 각 조별로 중요한 논의 내용을 기록하여 전체와 공유했다. 이러한 내용은 세미나가 끝난후 정식으로 웹에 출판되어 누구나 열람할 수 있다. 역대 모든 세미나의 자료는 여기에서 볼 수 있다. 좋은 말씀은 누구나 쉽게 접할 수 있도록 널리 퍼트리자는 정신. 역시 구텐베르크의 나라답다. 이 글을 쓰는 시점에는 아직 우리 세미나의 자료가 올라오지 않았지만, 최근에 참가자들의 메일링 리스트를 통해 최종본의 의견을 수렴하는 절차가 진행 중인 것으로 보아 머지 않아 올라올 것으로 보인다.
이 외에도, 여러 방면으로 참가자들의 흔적을 오래된 성에 새겨넣었다. 모든 참가자들은 방명록에 자필로 서명을 남겼다. 또한 도서관에는 각 참가자들이 직접 집필한 책을 비치해놓고 저자에게 직접 한마디씩 남기도록 했다. 우리 세미나 참가자들이 쓴 책도 도서관 입구의 작은 책장에 비치되어 있었다. 물어보니 지난 번에 참석했을 때 남겨놓았다는 사람들이 있었다. 도서관에는 제법 책이 많았는데, 그 작은 입구 책장에 우리 세미나 참석자의 책이 여러권 꽂혀 있는 것으로 보아, 아마 각 세미나 때마다 참가자들의 저작을 입구에 비치해놓는 것 같다.
이러한 기록정신은 참석자들의 가슴에 은은한 모닥불을 지피는 듯 했다. 우리가 나눈 이야기가 이 성처럼 오래도록 남을 것이라는 생각. 우리의 토론과 참여가 존중받고 지원받는다는 느낌. 그런 이유로 여기에 있는 일주일을 더 알차게 보내야겠다는 책임감. 마지막 날 밤 이야기를 나누어보니 나만 든 생각은 아니었다.
| 모든 발표자들은 발표 요약이 담긴 책 | 내 발표 요약문 | 참석자들의 저작물 |
마무리
잊고 있던 구석의 감각이 근질근질해지는 일주일이었다. 학생때부터 논문으로 만나던 선배 연구자들 그리고 오랜만에 만난 또래 친구들. 이해하고자 곱씹기를 반복했던 그 때 그 아이디어, 예제, 수식. 기억 저편에 있던 논문 제목. 대학생 시절 처음 홀로 떠난 여행지였던 독일. 내재된 많은 기억이 하나둘 떠오르며 귀국 길, 다시 흥겨운 먼 길을 재촉했다. 중세 판타지 영화 세트장 같은 세미나 장소도 묘한 분위기를 더했다. 그 분위기가 익숙할 유럽인들에게는 어떤 느낌일지 모르겠지만. 칼과 마법으로 용을 잡으러 떠나던 그 세계 사람들과, 과학을 연구하는 우리는 닮은 점이 많지 않은가. 여태껏 알지 못했던 세상의 비밀을 캐낸다는 것, 감당하기 어려운 거대한 것에 맞선다는 것, 같은 뜻을 품은 동료들과 힘을 합친다는 것.
| 유구한 역사와 전통을 지닌 닥스툴 세미나의 단체사진 |