[연재] 완벽한 백신SW 불가능한 이유, 튜링은 알고 있다
(2) 소프트웨어가 도무지 해결하지 못하는 세 가지:
첫 번째 '종료 문제'
지난해 과학계를 뜨겁게 달군 과학 뉴스 중 하나는 바로 중성미자 입자의 속력이 빛보다 더 빠르다는 어느 관측실험 결과였습니다. 이에 많은 사람들이 놀라움과 의구심을 나타낸 이유는 이 관측 결과가 100여 년이 넘도록 반박되지 않았던 아인슈타인의 특수 상대성이론을 뒤집는 것이었기 때문입니다. 그런데 소프트웨어공학에도 ‘빛의 속도’와 같은 불가침(?)의 영역이 있습니다. 수학자 앨런 튜링(Alan Turing,1912-1954)이 연구한 ‘홀팅(종료)문제’입니다.
컴퓨터를 사용하다가 “프로그램이 응답하지 않습니다”라는 경고 메시지를 본 적이 있을 겁니다. 정상적으로 종료했어야 하는 소프트웨어가 오류로 인해 실행을 무한히 계속하고 있을 때 등장하는 경고문입니다. ‘종료 문제’는 바로 임의의 소프트웨어가 언제나 정상적으로 종료하는지 아닌지를 결정하는 문제입니다. 종료 문제를 해결할 수 있다면, 프로그램이 응답을 하지 않는다는 경고문을 영영 보지 않아도 됩니다. 오류로 실행을 무한히 계속하는 프로그램을 미리 걸러낼 수 있다면 소프트웨어를 사용하는 모든 시스템의 안정성이 비약적으로 향상될 것이기 때문입니다. 일상의 모든 면면에 소프트웨어가 연관되어 있는 21세기의 삶을 생각해보면, 종료 문제의 해결은 이루 말할 수 없는 가치를 지닌다 하겠습니다. 그렇다면 이 중요한 문제는 해결됐을까요?
불행히도 앨런 튜링이 남긴 가장 큰 업적 중 하나는 ‘종료 문제를 완벽하게 해결하는 것이 불가능하다’는 수학적 증명입니다. 튜링은 ‘튜링 기계(Turing Machine)’라는 계산 모형을 이용해 종료 문제의 결정 불가능성을 증명했는데, 오늘날 우리가 사용하는 컴퓨터는 모두 본질적으로 고도로 발달한 튜링 기계입니다. 따라서 우리가 사용하는 모든 소프트웨어가 안전하게 종료한다는 완벽한 증명은 불가능한 셈입니다.
그런데 빛보다 빠르다는 중성미자의 속력 관측에 오류가 있었던 것으로 밝혀진 것과는 정반대로, 오늘날의 소프트웨어공학은 수학적으로 해결 불가능이 증명된 종료 문제에 여전히 도전하고 있을 뿐 아니라 가시적인 성과도 내고있습니다. 그럼 튜링이 틀린 것일까요? 아닙니다. 종료 문제의 결정 불가능성을 증명한 튜링도 옳고, 종료 문제를 해결하기 위해 연구에 몰두하는 소프트웨어공학자들도 옳다는, 황희 정승 뺨치는 상황을 이해하기 위해서는 종료 문제가 정확히 무엇인지를 조금 더 깊숙히 들여다볼 필요가 있습니다.
근본적으로 해결이 불가능한 문제
조금 딱딱한 이야기를 하기 전에, 일상에서 일어날 법한 예를 하나 들어 보겠습니다. 어느 날 친구가 요즘 인터넷에서 대단한 인기를 끌고 있는 무료 게임이라며 어떤 프로그램을 메일로 보내주었습니다. 출처를 모르는 프로그램을 실행하는 것을 피하라는 컴퓨터 보안전문가의 신문 컬럼이 생각나 잠깐 머뭇거렸지만 친구가 보내주었으니 괜찮겠지 싶어서 프로그램을 실행했습니다. 아뿔싸, 그럴 듯한 시작화면이 나타난 다음 컴퓨터가 아무런 반응을 하지 않습니다!
다양한 키조합을 눌러 보아도 반응이 없는 걸로 보아 아무래도 만능 해결책인 ‘껐다 켜기’를 시도해야 할 것 같지만, 그 사이에 컴퓨터에 무슨 피해라도 없었는지 걱정이 되기 시작합니다. 친구가 보내준 게임을 실행하기 전에 초강력 백신 프로그램 C3+를 이용해 이런 일이 벌어질지 아닐지 미리 알아낼 수 있는 방법은 없었을까요? 결론부터 말하자면 그렇게 강력한 백신 프로그램은 존재할 수 없습니다. 바로 종료 문제가 결정 불가능이기 때문입니다.
앨런 튜링은 ‘현대 컴퓨터과학의 아버지’라고 불리우는 영국 출신의 수학자입니다 .[1] 수학자로서 튜링의 업적은 그 범위가 무척 넓어서 컴퓨터과학은 물론이고 생물학에도 공헌했지만, 컴퓨터과학에서 튜링의 이름과 직결되는 가장 유명한 업적 중 하나가 바로 종료 문제입니다. 종료문제를 조금 딱딱한 수학적인 언어로 적으면 다음과 같습니다.
“임의의 프로그램 A가 주어졌을 때, A가 정상적으로 종료하는지 무한히 계속하는지를 결정하라.”
이것을 조금 더 일상적인 언어로 옮기면 다음과 같이 말할 수 있습니다.
“친구가 처음 보는 게임프로그램 A를 메일로 보냈다. A를 실행하면 정상적으로 종료하는지 아니면 컴퓨터가 ‘얼어버릴지’ (다시 말해 ‘프로그램이 응답을 하지 않습니다’라는 경고를 보게 될지)를 결정하라.”
“대체 그게 왜 어려운가?”라고 생각하시는 분들을 위해 이야기를 얼른 이어가자면, 튜링의 업적은 “임의의” 프로그램 A에 대해 종료 문제의 답을 “자동으로 계산해 결정하는 프로그램”을 작성하는 것이 불가능하다고 증명한 것입니다(결정 불가능). 다시 말해 ”실행해보니 정상적으로 종료하더라“라던지, 특정한 몇 개의 프로그램을 사람이 검토한 뒤 ”모두 분명히 정상적으로 종료한다“라고 말하는 것만 가지고는 종료 문제를 해결했다고 할 수 없다는 뜻입니다.
이 증명의 위대한 점 중 하나는 튜링이 결과를 발표한 시점이 프로그램은커녕 컴퓨터라는 것이 실제로 존재하지 않았던 1936년이라는 사실입니다. “프로그램”이 무엇인지를 수학적으로 논증하기 위해 튜링이 고안한 계산 모형이 이른바 튜링 기계로, 오늘날 우리가 사용하는 컴퓨터와 스마트폰은 모두 본질적으로 고도로 발달한 튜링기계일 뿐입니다. 자신이 증명하고자 하는 대상의 수학적 정의에서 시작해야 했던 튜링과 달리, 소프트웨어와 프로그램이라는 개념이 더 이상 낯설지 않은 오늘날의 우리는 큰 어려움 없이 종료 문제에 대한 증명을 스케치할 수 있습니다.
’귀류법’ 논리로 튜링 증명 맛보기
» 제2차 세계대전 당시에 영국 정보부가 비밀리에 암호 해독 작업을 수행했던 곳인 블레칠리 파크(Bletchley Park)에 세워진 앨런 튜링의 동상. 독일군이 사용한 암호기계 '이니그마(Enigma)'를 들여다보고 있다. 사진/ 유신논리와 관련된 수수께끼를 즐기시는 분들께는 아래의 증명이 좋은 두뇌 운동이 될 것입니다. 증명은 ‘귀류법’을 이용합니다. 귀류법(또는 반증법)은 어떤 주장에 대해 그 함의하는 내용을 따라가다보면 이치에 닿지 않는 내용 또는 결론에 이르게 됨을 보여서 애초의 주장이 잘못되었음을 보이는 증명 방법을 말하는데, 지금의 논리 문제를 푸는 데 유용하기에 여기에서 주로 사용하겠습니다. 우선, 만약에 종료 문제를 해결할 수 있다고, 다시 말해 친구가 보낸 게임 A가 정상적으로 종료하는지 아니면 무한히 계속하는지 결정할 수 있다고 가정해 봅시다. 그렇다면 종료 문제의 해답을 이용해서 다음과 같은 프로그램 H를 작성할 수 있습니다.
프로그램 H는 다른 프로그램 A를 입력으로 받아서:
(1) A가 정상적으로 종료하는 프로그램이면, 프로그램 H는 무한히 실행을 계속한다 (즉,“응답을 하지 않”는다)
(2) A가 정상적으로 종료하는 프로그램이 아니면, 프로그램 H는 정상 종료한다
H는 일부러 응답을 하지 않는 기능을 갖춘, 도무지 아무런 쓸모가 없어 보이는 프로그램이지만, 우리의 증명 과정에서는 결정적인 역할을 하게 됩니다. 여기서 핵심은 친구가 무슨 게임, 무슨 프로그램을 보내더라도(다시말해 ‘가능한 모든’ 프로그램에 대해서도) 프로그램 H는 친구가 준 프로그램의 정상 종료 여부를 결정할 수 있어야 한다는 것입니다. 문제는 ‘가능한 모든’ 프로그램에는 H 자신도 포함된다는 것입니다. H에 H 자신을 입력으로 넣으면 어떻게 될까요?
H가 정상 종료하려면 입력으로 받은 프로그램이 무한히 계속하는 프로그램이어야 하는데(위에서 (2)의 경우), 그렇다면 결국에는 H 자신도 무한히 계속해야 한다는 뜻이 되어 모순입니다. 반대로 H가 무한히 계속한다면 입력으로 받은 프로그램은 정상 종료해야 하고(위에서 (1)의 경우), 입력 프로그램에는 H 자신도 포함되어 H 자신이 정상 종료해야만 한다는 뜻이 되니, 역시 모순입니다. 결국 귀류법에 따라, 종료 문제가 결정 가능하다는 전제조건은 틀렸음이 입증됩니다.[2]
“임의의 프로그램에 대해 종료 문제를 결정할 수 없다”는 튜링의 증명은 절대 명제입니다. 빛보다 빠른 중성미자가 관측되었다는 첫 소식을 들었을 때에 많은 물리학자들이 특수상대성이론이 잘못됐을 리 없다며 관측 사실에 의구심을 표했던 것처럼, 소프트웨어에 대한 새로운 가설이 종료 문제의 해결 방법로 귀결될 경우 튜링의 증명이 틀릴 수 없기 때문에 새 주장이 오류라고 판단합니다.
완벽한 백신 프로그램이 불가능한 이유도
그러면 이제 글 첫머리에 얘기했던 예로 다시 돌아가볼까요? 지금부터 친구가 보낸 게임 A가 나쁜 짓 X를 할지 안 할지를 미리 규명하는 완벽한 백신 프로그램 C3+가 불가능한 이유를 알아보겠습니다. 먼저 완벽한 백신 프로그램 C3+가 존재한다고 가정해 봅시다. 그렇게 가정한 전제에서는 다음과 같은 편법(?)을 써서 종료 문제를 해결하는 프로그램 H를 작성할 수 있을 것입니다.
프로그램 H는 다른 프로그램 A를 입력으로 받는다:
(1) A의 마지막에 나쁜짓 X를 추가한 A‘를 만든다.
(2) C3+를 이용해 A’가 나쁜짓 X를 할 수 있는지 결정한다.
다음의 두 가지 결론은 모두 다 종료 문제의 결정 불가능성과 모순이 됩니다.
(1) C3+가 A‘는 안전하다고 결정한다: A’가 안전한 유일한 경우는 A의 실행이 무한히 계속되어 X에 영영 도달하지 않는 경우이다. 다시 말해 A가 정상적으로 종료하지 않는다는 뜻이다.
(2) C3+가 A‘는 위험하다고 결정한다: A’가 위험한 유일한 경우는 A의 실행이 정상적으로 종료되어 X에 도달하는 경우이다. 다시 말해 A가 정상적으로 종료한다는 뜻이다.
어느 쪽이든 C3+가 A에 대한 종료 문제를 해결하는 것이 됩니다. 물론 그럴 리가 없기 때문에, 역시 귀류법에 따라 C3+와 같은 완벽한 백신이 존재할 수 있다는 전제는 틀린 것이 되고 완벽한 백신은 존재하지 않는다는 결론에 도달합니다.[3]
틈새 파고들어 개선책을 찾는 소프트웨어공학
잠깐, 이렇게 종료 문제가 근본적으로 해결할 수 없는 문제라면, 그렇다면 현재 종료 문제를 한창 연구하는 소프트웨어 공학자들은 대체 뭘 하고 있는 걸까요? 지금 사용하는 백신 프로그램에 의혹의 눈초리를 보내기 전에 이전에도 문제(?)가 되었던 “임의의”라는 표현에 주목하세요. 종료 문제가 결정 불가능인 이유는 임의의 프로그램, 즉 상상 가능한 모든 프로그램에 대해 정상 종료 여부를 결정해야 하기 때문입니다. 상상 가능한 모든 프로그램의 갯수는 무한할 뿐더러, 아마도 무한한 갯수의 아무 쓸모 없는 프로그램을 포함할것입니다. 아무 쓸모 없는 프로그램이 종료하는지 아닌지는 우리의 관심사가 아닙니다.
종료 문제를 연구하는 소프트웨어공학자들은 가능한 모든 프로그램이 아닌 우리에게 가치가 있는 프로그램으로 문제의 범위를 제한한 뒤에 종료 문제에 대한 부분적인 해답을 얻는 것을 목표로 합니다. 임의의 모든 프로그램에 대해 종료 문제를 해결하는 것은 불가능하지만, 그럼에도 불구하고 상당수의 프로그램에 대해서는 해결이 가능하다는 뜻입니다 (마찬가지로, 완벽한 백신은 이론적으로 불가능하지만 매우 믿을 만한 백신은 충분히 가능하다는 희소식이기도 합니다). 이들이 연구하는 기술을 자동종료 증명(Automated Termination Proof)이라고합니다. 주어진 소프트웨어가 언제나 정상적으로 종료하는지를 자동으로 증명하는 도구를 만드는 것입니다.
물론 분석 대상을 특정한 맥락의 프로그램으로 제한한다 하더라도 종료 문제를 결정하는 것은 결코 쉽지 않은 일이며, 소프트웨어를 이용한 자동종료 증명은 단순한 수학적인 이론을 넘어 고도의 공학적 완성도를 요하는 계산작업입니다. 컴퓨터과학에서 가장 유명한 결정 불가능 문제임에도 불구하고 종료 증명을 향한 사람들의 노력은 멈추지 않았고, 그 과실 중 일부는 생각보다 가까운 곳에 있습니다.
마이크로소프트사의 연구조직인 마이크로소프트 리서치(Microsoft Research)가 자랑하는 여러 업적 중 하나가 바로 자동종료 증명을 목표로 하는 터미네이터(Terminator), 즉 ‘종결자’ 프로젝트입니다. 터미네이터 프로젝트는 윈도 운영체제가 사용하는 장치 드라이버 프로그램을 대상으로 약 3만5천 줄 크기의 프로그램 코드에 대한 자동종료 증명을 완수했습니다. 그 결과는 정상 종료가 보장되는 장치 드라이버 프로그램, 다시 말해서 갑자기 컴퓨터가 아무런 반응을 하지 않거나 프로그램이 응답을 하지 않는 일이 크게 줄어든다는 뜻입니다. 윈도 운영체제가 버전이 올라갈수록 더 안정적이 된 데에는 자동종료 증명 기술을 발전시킨 연구결과도 한몫을 했습니다. 물론 마이크로소프트 리서치 이외에도 많은 연구자들이 다양한 접근방법을 이용한 자동종료 증명 연구결과를 내놓은 바 있습니다.
종료 문제, 그리고 자동종료 증명을 항한 사람들의 노력은 여러 모로 소프트웨어를 둘러싸고 과학(수학)과 공학이 어디에서 만나고 있는지를 잘 보여줍니다. 한편으로는 극히 추상적인 수학 문제로 보이는 종료 문제가 바이러스 백신 프로그램과 같은 일상적인 소프트웨어의 한계를 규정합니다. 그 반대편에는 이론적으로 계산 불가능한 문제에 대한 답을 조금이라도 더 얻어내려는 컴퓨터과학의 노력과 이 복잡한 계산이 실제로 가능하도록 뒷받침하는 공학적 뒷받침이 있습니다.
종료 문제는 해결이 불가능하다는 것이 이론적으로 증명된 문제입니다. 다음 회에서는 불가능한 것은 아니지만 답을 계산하려면 시간이 너무 오래 걸려서 사실상 불가능에 가까운 문제들을 알아보겠습니다.
[주]
[1] 컴퓨터과학 바깥에 튜링의 이름을 가장 널리 알린 업적은 2차 세계대전 중 독일군이 사용한 암호 이니그마(Enigma)를 해독하는 데 공을 세운 점입니다. 역사학자들은 앨런 튜링을 위시한 수학자들이 이끈 암호 해독팀이 이니그마를 해독한 덕분에 2차 대전의 종전이 2년 정도 앞당겨졌다고 평가합니다. 튜링이 비밀리에 암호 해독 작업을 수행했던 장소인 블레칠리 파크(Bletchley Park)는 그 역할이 일반에 잘 알려지지 않은 덕분에 관리가 매우 소홀했으나, 최근 구글의 대규모 기부를 비롯한 블레칠리파크 구명 운동 덕분에 암호 해독 팀이 사용한 초기 컴퓨터를 보관하는 박물관으로 거듭날 수 있게 됐습니다.
[2] 여기서 거짓말쟁이의 역설, 혹은 러셀의 역설을 생각하신 분들은 종료 문제 증명의 핵심을 꿰뚫어본 것입니다 :)
[3] 사실 튜링이 실제로 증명한 것은 “주어진 프로그램 A가 유한(finite)한 행동 X를 하는지를 결정하는 프로그램 H를 작성하는 것은 불가능하다”는 것이며, 종료 문제는 유한한 행동 X가 홀팅, 즉 종료 기능을 포함하는 특수한 경우입니다. 어떤 의미에서 튜링의 결정 불가능성 증명은 바로 완벽한 백신의 존재가 불가능하다는 증명에 매우 가깝습니다 :)
'Travia' 카테고리의 다른 글
| 불완전성 정리_쿠르트 괴델 (0) | 2014.03.16 |
|---|---|
| 불확정성 원리_하이젠베르크 (0) | 2014.03.16 |
| 앨런 튜링 (0) | 2014.03.16 |
| 거짓말쟁이의 역설 (0) | 2014.03.16 |
| 트로피코 (0) | 2014.02.15 |
