기술 요약: 충분한 부정확성 논리 (Sufficient Incorrectness Logic, SIL) 및 Separation SIL

1. 문제 정의

프로그램 검증을 위한 형식 방법론은 역사적으로 오류의 부재를 보장하기 위해 과대 근사(over-approximation) 기법(예: Hoare Logic, Abstract Interpretation)에 의존해 왔습니다. 이러한 방법들은 타당(sound)하지만, 필연적으로 허위 경보(false alarms)(가짜 오류)를 생성하여 프로그래머의 도입을 저해할 수 있습니다. 반대로, 과소 근사(under-approximation) 기법(예: Incorrectness Logic, Bounded Model Checking)은 버그 탐지를 위해 설계되었으며, 도달 가능한 오류 상태만을 보고하므로 허위 경보가 없습니다. 그러나 Incorrectness Logic(IL)과 같은 기존의 과소 근사 논리는 주로 전제 조건으로부터 도달 가능한 오류의 존재를 증명하는 데 집중합니다. 이들은 오류를 유발하는 초기 상태의 집합을 반드시 규명하지는 못합니다.

본 논문은 **부정확성의 근원(sources of incorrectness)**을 추론하는 과정에서의 공백을 지적합니다. 프로그래머는 단순히 버그가 존재한다는 사실뿐만 아니라, 구체적으로 어떤 입력 상태가 그 버그를 유발하는지 알아야 하며, 이를 통해 디버깅과 테스팅의 범위를 효과적으로 설정할 수 있습니다. "리스본 트리플(Lisbon triples)"(역방향 과소 근사)은 이전에 Outcome Logic(OL)의 맥락에서 논의된 바 있으나, **충분한 전제 조건(sufficient preconditions)**을 추론하기 위해 전용된 최소한의 완전한 증명 시스템은 결여되어 있었습니다.

2. 방법론

저자들은 **역방향 과소 근사(backward under-approximation)**를 위해 설계된 새로운 트리플 기반 프로그램 논리인 **Sufficient Incorrectness Logic (SIL)**을 소개합니다.

2.1 핵심 개념: SIL 트리플

SIL 트리플은 $\langle\langle P \rangle\rangle r \langle\langle Q \rangle\rangle$로 표기됩니다.

• 의미론(Semantics): 이 트리플은 프로그램 $r$의 역방향 수집 의미론(backward collecting semantics)을 오류 상태의 집합 $Q$에 적용했을 때, 그 결과가 초기 상태의 집합 $P$를 포함하는 경우에만 유효합니다. 형식적으로는 $J \leftarrow r K (Q) \supseteq P$입니다.
• 해석: "전제 조건 $P$를 만족하는 모든 입력 상태는 $Q$를 만족하는 오류로 이어지는 $r$의 실행을 적어도 하나 이상 갖는다."
• IL과의 차이점: IL($[P] r [Q]$)이 $P$에 속하는 어떤 상태에서 $Q$에 속하는 어떤 상태로의 도달 가능성을 보장한다면, SIL은 $P$의 모든 상태가 $Q$의 오류에 도달할 수 있음을 보장합니다. 이는 $P$를 부정확성에 대한 **충분 조건(sufficient condition)**으로 만듭니다.

2.2 증명 시스템

저자들은 정규 명령(비결정론 및 루프 포함)에 대해 타당하고 완전한(sound and complete) 최소한의 SIL 증명 규칙 세트(Figure 7)를 정의합니다.

• 역방향 의미론: 규칙들은 명령의 역방향 의미론(예: 할당은 역방향 치환을 사용)으로부터 유도됩니다.
• 결과 규칙(Consequence Rule): $\langle\langle \text{cons} \rangle\rangle$ 규칙은 전제 조건을 강화하고 후제 조건을 약화시킴으로써 과소 근사를 용이하게 합니다.
• 루프 처리: 이 논리는 반복($\langle\langle \text{iter} \rangle\rangle$)을 위한 규칙과 더불어, 종료를 위한 루프 불변식이 필요하지 않은 실용적인 분석을 지원하기 위한 $\langle\langle \text{iter0} \rangle\rangle$(루프 건너뛰기) 및 $\langle\langle \text{unroll} \rangle\rangle$(1회 언롤링)와 같은 추가 규칙을 포함합니다.
• 선택(Disjunction): Hoare Logic과 달리, SIL은 전제 조건에서 선언(disjuncts)을 탈락시키는 것을 허용하며($\langle\langle \text{choice} \rangle\rangle$ 및 $\langle\langle \text{disj} \rangle\rangle$를 통해), 이는 과소 근사에서의 확장성을 위해 매우 중요합니다.

2.3 Separation SIL

포인터와 동적 메모리 할당을 처리하기 위해, 저자들은 SIL을 Separation Logic 공식과 결합하여 Separation SIL을 구현합니다.

• 단언 언어(Assertion Language): 표준 Separation Logic(힙 분리, points-to)과 Incorrectness Separation Logic(ISL)에서 채택된 $x \not\mapsto$(해제된 포인터를 나타냄)를 결합합니다.
• 규칙: 힙 연산(alloc, free, load, store)에 대한 역방향 규칙과 로컬 메모리 오류에 대한 국소적 추론을 가능하게 하는 프레임 규칙($\langle\langle \text{frame} \rangle\rangle$)을 포함합니다.
• 완전성: 이 시스템은 타당성이 증명되었습니다. 루프가 없는 프로그램에 대해, 단언 간의 함의를 판단하는 오라클이 있다고 가정할 때 **상대적 완전성(relatively complete)**이 입증되었습니다.

3. 주요 기여

1. SIL의 도입: 오류의 존재뿐만 아니라 오류의 근원(초기 상태)을 식별하는 충분한 부정확성 트리플을 위한 새로운 논리를 제시했습니다.
2. 형식적 분류 체계: 저자들은 두 축을 기준으로 트리플 기반 논리의 분류 체계(Figure 3)를 구축했습니다.
   • 의미론 방향: 순방향(Hoare Logic, IL) vs 역방향(SIL, Necessary Conditions).
   • 근사 유형: 과대 근사(Hoare Logic, Necessary Conditions) vs 과소 근사(IL, SIL).
   • 이 분류를 통해 SIL이 역방향 의미론과 과소 근사의 유일한 조합임을 명확히 했습니다.
3. 비교 분석:
   • SIL vs IL: IL은 오류가 도달 가능한지 여부를 찾고, SIL은 어떤 입력이 이를 유발하는지를 찾습니다. 둘은 논리적으로 동등하지 않습니다.
   • SIL vs Hoare Logic (HL): 결정론적이고 종료되는 프로그램에 대해, SIL과 HL은 일치합니다(후제 조건을 오류 상태로 해석할 때). 비결정론적 프로그램의 경우 두 논리는 갈라집니다.
   • SIL vs Necessary Conditions (NC): 저자들은 NC가 이중 부정(double negation)을 통해 HL과 동형(isomorphic)임을 증명했으나, 일반적인 경우 IL이나 SIL과는 비교할 수 없음을 보여줍니다.
   • SIL vs Outcome Logic (OL): OL은 SIL 트리플(특히 "Lisbon" 패턴)을 표현할 수 있지만, 저자들은 SIL의 증명 시스템이 특히 선언 처리와 역방향 추론 측면에서 오류 사양으로부터 전제 조건을 추론하는 데 더 직접적이고 자연스럽다고 주장합니다.
4. Separation SIL: 메모리 오류를 위한 타당하고 상대적으로 완전한 구현을 제공하며, 특정 사례(예: 테스트를 위한 실제 witness 제공)에서 ISL보다 더 간결한 후제 조건과 강력한 보증을 제공할 수 있음을 보여줍니다.

4. 결과

• 정확성 및 완전성: 최소한의 SIL 규칙 세트는 정규 명령에 대해 타당하고 완전함이 증명되었습니다.
• 상대적 완전성: Separation SIL은 루프가 없는 프로그램에 대해 상대적 완전성이 입증되었습니다.
• 산업적 관련성: 저자들은 SIL이 보안 버그를 탐지하기 위해 충분한 부정확성 전제 조건을 추론하는 Meta의 산업용 도구들(Zoncolan, Mariana Trench, Pysa)에서 사용되는 역방향 분석 전략에 대한 공식적인 사후 정당성을 제공한다고 주장합니다.
• 유도 예시: 저자들은 free와 alloc을 포함하는 클라이언트 프로그램에 대한 상세한 유도 과정을 제공하여, Separation SIL이 어떻게 오류 발생을 보장하는 전제 조건을 도출하여 디버깅에 대한 더 직접적인 경로를 제공하는지 보여줍니다.

5. 의의 및 주장

본 논문은 역방향 지향적 과소 근사 프레임워크를 제공함으로써 중요한 이론적 공백을 메운다고 주장합니다. 그 의의는 다음과 같습니다:

• 디버깅을 위한 정밀도: 오류를 유발하는 정확한 입력 상태 집합을 식별함으로써, SIL은 단순히 오류의 도달 가능성만을 보여주는 순방향 과소 근사와 달리, 개발자가 "왜" 버그가 발생하는지 이해하는 데 더 자연스러운 "역방향 추론"을 지원합니다.
• 이론적 통합: Hoare Logic과 Necessary Conditions 사이에 쌍대성이 존재하는 반면, Incorrectness Logic과 Sufficient Incorrectness Logic 사이에는 그러한 단순한 쌍대성이 존재하지 않음을 밝혀 논리적 지형을 명확히 했습니다.
• 실용적 유용성: 저자들은 Separation SIL이 ISL보다 더 간결한 후제 조건과 강력한 보증을 생성할 수 있다고 주장합니다. 이는 전제 조건 내의 모든 상태가 오류로 이어진다는 것을 보장함으로써 구체적인 witness를 제공하기 때문입니다.

결론적으로, 본 논문은 어떤 하나의 논리가 반드시 "더 낫다"고 말하는 것이 아니라, 각 논리(HL, IL, NC, SIL)가 고유한 목적을 가지고 있다고 주장합니다. SIL은 특히 부정확성의 근원을 찾아내어 디버깅과 테스팅 작업을 가이드하고자 할 때 최적의 도구로 위치합니다.