프로그램 분석 견고성 연구: 범주론으로 정적 분석의 예측 가능성을 정의하고 설계하는 법

핵심 메시지

• 개발자는 코드를 조금 고치면 정적 분석 경고도 그만큼만 달라지리라 기대하지만 실제 분석기는 그 기대를 자주 배반한다.
• 쓰이지 않는 변수 하나를 더했을 뿐인데 이전에 증명되던 하한이 사라지거나, 기호 상수를 구체적인 숫자로 바꿨더니 종료성 증명이 시간 초과로 실패하는 사례가 보고됐다.
• 연구팀은 프로그램과 그 성질을 범주로 보고, 견고한 분석을 구조를 보존하는 함자로 규정하는 언어를 제안했다.
• 정밀도와 견고성 사이에는 긴장이 있어, 강력한 분석을 떠받치는 확대 연산이나 보간 같은 도구가 오히려 표현 방식에 민감하게 반응한다.
• 제한된 계산 모형에서 안전하고 견고한 분석을 만든 뒤 일반 프로그램으로 끌어올리는 조리법이 기존 루프 분석 여러 편의 공통 구조임을 밝혔다.

쉽게 이해하기

PLDI 2026에서 프린스턴대 연구팀이 정적 분석의 '견고성'을 주제로 발표했다. 출발점은 소박한 기대다. 개발자는 코드를 고치면 분석기가 내놓는 경고 목록도 그 변경에 상응해 달라지기를 바라고, 분석 도구를 만드는 쪽도 어떤 변환이 분석을 개선하는지 악화시키는지 알고 싶어 한다. 그런데 많은 분석기가 이 기대를 충족하지 못한다.

발표에서 든 첫 사례는 폴리헤드럴 분석이다. 어떤 프로그램에서 변수 i가 1과 5 사이에 있음을 증명했는데, i의 계산에는 손대지 않고 i 값을 누적하는 변수 j를 추가하기만 해도 i의 하한을 더 이상 증명하지 못하게 된다. 두 번째 사례는 중첩 루프의 종료성이다. 기호 상수 n에 대해 종료성을 증명했다면 n을 4096 같은 구체적 수로 바꾼 프로그램은 당연히 증명될 것 같지만, 검증 도구가 15분 뒤 시간 초과로 실패했다. 발표자는 이것이 장난감 예제에 그치지 않는다며, 상용 정적 분석기 사용 경험 보고서에 불안정한 오류 보고에 대한 사용자 불만과 이를 피하려는 우회 노력이 한 절을 차지한다는 점을 짚었다.

이 문제를 다루기 위해 연구팀이 택한 도구는 범주론이다. 예컨대 분석 결과가 변수 이름에 좌우되지 않아야 한다는 성질은, 이름 바꾸기로 서로 옮겨지는 두 프로그램의 분석 결과도 같은 이름 바꾸기로 서로 옮겨져야 한다는 뜻이다. 연구팀은 프로그램을 대상으로, 이름 바꾸기 관계를 화살표로 삼는 범주를 만들고 분석 결과 쪽에도 같은 구조를 세운 뒤, 두 범주를 밑에 깔린 치환의 범주로 각각 사영했다. 견고성은 이 도식이 가환이라는 조건, 즉 분석이 구체 함자라는 조건으로 정리된다.

이 언어의 강점은 견고성이 하나의 성질이 아니라 관심 있는 변환의 종류마다 달라지는 성질들의 집합임을 그대로 담아낸다는 데 있다. 발표자는 이를 추상 해석이 건전성에 대해 해준 일을 견고성에 대해 해보려는 시도라고 표현했다. 기존 순서 이론 어휘를 잃지도 않는다. 항등 함수로 사영되는 화살표들을 모으면 늘 순서 관계가 정의되어, 추상 해석에서 익숙한 근사 순서를 그대로 복원할 수 있기 때문이다.

두 번째 축은 실제로 견고한 분석을 만드는 방법이다. 발표자는 정밀도와 견고성 사이의 긴장을 인정했다. 더 많은 것을 증명하는 강력한 분석일수록 확대 연산이나 크레이그 보간처럼 표현 방식에 민감한 부품에 기대게 되고, 그만큼 견고성이 나빠진다. 대신 연구실이 몇 해에 걸쳐 다듬어온 조리법이 있다. 튜링 완전하지 않은 제한된 계산 모형에서 어떤 성질이 계산 가능함을 보인 이론 결과를 가져와, 루프를 그 모형으로 추상화하고 분석한 뒤 결과를 원래 프로그램의 안전한 근사로 되돌리는 방식이다. 논문은 이 조리법이 여러 루프 요약·종료성 분석의 공통 구조임을 형식적으로 보였고, 그 결과 이들이 단조로울 뿐 아니라 선형 변환에 대해서도 견고하다는 더 강한 결론을 얻었다고 밝혔다.

마지막으로 이 조리법이 프로그램 전체로 어떻게 확장되는지도 다뤘다. 대수적 프로그램 분석은 제어 흐름 그래프에서 관심 있는 경로 집합을 정규 표현식으로 뽑아낸 뒤, 정규 표현식의 연산을 전이 공식에 대한 연산으로 재해석해 전체 경로를 근사한다. 앞서 말한 견고한 루프 분석들은 이 틀에서 별표 연산자의 서로 다른 구현에 해당한다. 연구팀은 함자를 끌어올리는 전략이 자연 변환도 함께 옮겨준다는 점을 이용해 반복 연산자가 만족하는 대수 법칙을 증명했고, 이를 개별 연산자의 견고성과 결합해 루프 전개나 루프를 여러 단계로 쪼개는 변환에 대해 분석 전체가 견고함을 보였다.

주요 인사이트

• 정적 분석 도구의 실용성을 가르는 것은 얼마나 많이 증명하느냐만이 아니라, 같은 코드를 조금 고쳤을 때 결과가 어떻게 움직일지 개발자가 예상할 수 있느냐다.
• 견고성은 단일 조건이 아니라 관심 있는 변환의 종류에 따라 달라지는 성질의 집합이므로, 어떤 변환을 보존하고 싶은지 먼저 정하지 않으면 논의가 성립하지 않는다.
• 확대 연산이나 보간처럼 분석의 정밀도를 끌어올리는 부품 상당수가 프로그램의 표현 방식에 민감하다는 점에서, 정밀도와 예측 가능성은 실제로 맞바꿔야 하는 관계다.
• 제한된 계산 모형에서의 결과를 일반 프로그램으로 끌어올리는 조리법은 개별 논문마다 따로 쓰던 정당성 증명을 하나의 틀로 대체해, 반복되는 증명 부담을 줄인다.
• 분석이 특정 변환에 대해 견고하다는 것이 증명되면 그 변환 뒤에 분석을 처음부터 다시 돌릴 필요가 줄어들 수 있어, 이론적 성질이 곧 성능 이점으로 이어질 여지가 있다.

자주 묻는 질문

관련 AI 소식