형식 검증만으로 안전을 믿을 수 있을까?

프로그램 검증 결과를 믿는다면, 머리 위에 매달린 피아노 아래에서도 안심할 수 있을까? 이 글은 형식 검증의 의미와 신뢰성을 묻고, 실제 환경에서의 시험과 고장 분석도 안전한 시스템을 만드는 데 중요하다고 말한다.

가상의 상황에서 한 연구자가 특정 버전의 OpenSSH가 배열 범위 초과나 널 포인터 역참조 같은 메모리 오류를 일으키지 않는다고 증명했다고 하자. 사무실에는 피아노가 천장에 매달려 있고, 컴퓨터가 USB로 연결된 장치에는 명령을 받으면 밧줄을 끊는 칼이 들어 있다. OpenSSH가 충돌하면 SIGSEGV 처리기가 컴퓨터에 신호를 보내 밧줄을 끊도록 설정돼 있다. 이 검증 결과를 믿는다면, 피아노 아래에 앉아 퍼징 도구로 OpenSSH를 공격해도 괜찮을까?

글은 피아노 아래에 앉는 사람은 어리석어 보일 것이라고 말한다. 하지만 형식 검증 연구자 가운데 자신의 검증 결과를 이 정도로 믿는 사람은 많지 않을 것이라고 덧붙인다. 문제는 ‘검증됐다’는 말이 느슨하게 쓰이는 경우가 있고, 검증 결과가 수학적으로 타당할 뿐 아니라 검증하려던 의도에 부합하는지 설득력 있게 입증하기도 매우 어렵다는 점이다. 글에서 지적한 한 논문은 증명 개요만 담고도 ‘엄밀히 증명했다’, ‘형식적으로 검증했다’고 표현했다.

이 비유는 우스꽝스럽지만, 위험을 감수하는 상황 자체는 현실에 있다. 선진국의 교통 시스템을 이용할 때마다 사람들은 내장 컴퓨터의 오작동이 해를 끼칠 위험보다 이용의 이점이 크다고 판단한다. 글은 신호등이나 차량 안정성 제어 시스템이 검증돼 있기 때문이 아니라, 어제 잘 작동한 시스템이 오늘도 작동할 것이라고 가정하기 때문에 이런 판단을 한다고 설명한다.

글은 실제 환경에서 시스템을 시험하고, 고장을 엄밀히 살펴 그 결과를 다음 설계에 반영하는 방식이 신뢰성 있는 공학 시스템을 만드는 데 중요하다고 강조한다. 이는 형식 검증과 양립할 수 있지만, 검증 관련 문헌에서는 이런 관점이 자주 드러나지 않는다고 지적한다.

2011년 2월 1일 업데이트에서는 기술적인 세부 내용을 추가한 후속 글을 안내했다.