프로그램 분석에서의 Soundness

PL에서 Soundness와 Completeness는 자주 언급되는 개념이다. 하지만 이에 대한 정의는 일정하게 사용되지 않는 양상을 보여, 가끔 혼동을 주기도 한다. 그리고, 정적분석에 대해서 Sound(안전하다), Complele(완전하다), 혹은 Soundy(적당히 안전하다)라는 개념 또한 고려해 보아야할 것이다.정적분석에서의 Soundness(안전성)

Soundness의 개념은 형식적인 수학 논리 모델에서 온 것이다. 어떤 증명 시스템과 모델이 있다고 가정하자. 증명 시스템은 성질들을 증명할 수 있는 규칙들의 집합이고, 이는 수학적인 구조를 가진다. 증명 시스템 L이 증명하는 모든 statement들이 true라면 Sound하다고 할 수 있다. 그리고 L이 모델에 있는 모든 true인 statement들을 증명할 수 있다면 이는 Complete 하다고 한다. 하지만 대부분의 증명 시스템에서는 Sound한 동시에 Complete하기는 어렵다.

우리는 그렇다면, 프로그램의 특정 성질에 대해 분석하는 정적분석을 이러한 증명 시스템에 대입해볼 수 있을 것이다. 이 경우에는 정적분석기가 증명 시스템으로, 프로그램들이 모델로 대입될 수 있다.

위 그림은 이러한 상황을 시각적으로 나타내준다. 좌측에 있는 초록색 사각형이 Sound해야하는 특정 성질을 나타내고, 절대 런타임 에러를 내지 않는다. 좌측 상단 원형의 분석 꼴은 이러한 Sound한 성질을 완전히 만족시키는 분석기 A를 나타낸다. 이 경우 프로그램 p1과 p2를 커버하지만 해당 원 밖에 있는 프로그램에 대해서는 Sound하더라도(p3, p4) 오탐을 낼 것이다. 그럼에도 불구하고 분석기 A는 좌측 초록색 사각형에 완전히 속하기 때문에, Sound하다고 볼 수 있을 것이다.

 

 

오탐과 Completeness(완전성)

그렇다면, 이제 A의 원 밖에 있는 프로그램들이 문제가 될 것이다. p3과 p4는 분명 문제가 없는 프로그램이지만, 분석기 A에서는 문제가 있다고 판단할 것이다. 이는 우리가 흔히 말하는 False alarm(오탐)의 결과로 나타난다. 위 그림에서 분석기 B는 Unsound하다. p1~4까지의 오류를 잘 찾아내지만, 에러가 있는 프로그램인 p5에 대해서도 문제가 없다고 받아들일 것이다. 그리고 마지막으로 분석기 C는 Complete하다고 할 수 있다.

 

 

Soundiness(적당한 안전성)

문제는, 현실세계에서 Soundness와 Completeness를 모두 만족시킨다는 것은 어려운 일이라는 것이다. 받아들이는 모든 프로그램에 대해서 알람을 내는 분석기는 개념적으로 Sound하다고 할 수 있고, 세상 모든 프로그램에 대해 알람을 내지 않고 받아들이는 분석기는 개념적으로 Complete하다고 할 수 있을 것이다. 이상적으로는 분석기는 Soundness와 Completeness를 모두 추구해야할 것이다. 하지만 그 것은 불가능에 가깝다.

그에 대해 새롭게 만들어진 표현이 Soundiness(적당한 안전성)이라는 것이다. Soundy한 분석기는 특정 프로그래밍 패턴이나, 언어의 특성에 대해서는 불안전하지만, 이를 제외한 프로그램에 대해서는 안전한 분석을 하는 것이다.(False alarm을 적게내는) 완전성에 대해서는 어느정도 타협을 하지만, 실제로 쓸만하게 오류에 대해서 알람을 잘 내는 것이다.

 

 

Precision(정밀도)과 Recall(재현율)

(Precision과 Recall을 한국 위키피디아에서는 정밀도와 재현율이라 표현하였지만 딱히 이해가 잘 되는 단어가 아니라고 판단하여 영어 표현을 그대로 사용하겠다.) Soundness를 가정에 맞게 증명하는 것은 모든 상황을 설명하지는 못한다. 좋은 분석기는 잘 짜여진 프로그램부터 엉성한 프로그램까지 증명이 가능하며 오탐수도 적어야 한다. 이 것을 수량적인 방법으로 표현하는 것에는 Precision과 Recall이 있다. 아래 그림에서 보듯이, Precision은 전체 알람에서의 진짜 알람의 비율을 의미하고( t·a / (t·a + f·a) ), Recall은 실제 존재하는 프로그램을 얼마나 커버했는 지를 의미한다. 그러면 자연스럽게 Sound한 분석기는 Precision을 1로 만드는 분석기이고, Complete한 분석기는 Recall을 1로 만드는 분석기로 연결될 수 있을 것이다.

 

Precision과 Recall의 한계점

Precision과 Recall이 분석의 Soundness와 Completeness의 실용적인 간극을 줄여주긴 하지만, 이 것들은 또한 문제점을 가지고 있다. 문제는, 이러한 측정값들이 정확한 개념에 뒷받침되는 것이 아니라, 실증적인 결과에 의해서 결정된다는 것이다. 프로그램의 특정 성질을 증명하기 위해서 우리는 직접 그 경계를 정해야 할텐데 이것은 모든 프로그램에 대해 적용되기는 어려울 것이다.

Precision과 Recall의 또 다른 문제점은, 이 두 개념이 프로그램 전체에 대해 정의된 것이지만, 실용적인 프로그램들은 실제 크기가 매우 크거나 그 구조가 복잡하여 프로그램 전체에서 봤을 때 분석기가 적은 수의 알람을 발생시킨 것처럼 보일 수도 있다는 것이다.(Precision과 Recall의 개념을 그대로 프로그램 전체에 적용시켰을 때) 우리는 프로그램 전체에 관심이 있다기보다 문제가 되는 특정 버그나 성질에 대해 관심이 있을 것이다.

결론

Soundness와 Completeness는 정적 분석의 효율을 측정하는 척도가 된다. 완벽한 분석기는 둘 다 성취할 수 있을 것이다. 하지만, 이는 일반적으로 불가능하다. Precision과 Recall이라는 개념이 이에 대해 수량적인 측정 결과를 줄 순 있지만 이는 특정 성질에 대한 Ground truth가 주어졌을 때만 의미가 있다. 따라서 이에 대해 실용적이고 의미있는 측정 결과를 주기 위해 모든 프로그램의 statement에 대해 적용될 수 있는 개념적인 측정 방법이 필요할 것이다.

 

출처 : Programming Languages Enthusiast 블로그

본 글은 위 출처의 포스팅을 번역, 정리한 것입니다. 오역 및 잘못된 내용이 있다면 댓글로 남겨주세요.