Logic & Formal Verification

1. Overview

논리 및 형식 검증(Logic & Formal Verification, LFV)은 하드웨어와 소프트웨어 시스템이 설계 의도대로 정확하게 동작함을 수학적 논증을 통해 입증하는 무결성 핵심 분야입니다.

단순한 테스트(Testing)가 오류의 존재를 샘플을 통해 보여준다면, 형식 검증은 논리 모델 탐색을 통해 오류의 부재를 이론적으로 증명합니다. 학습자는 명제 논리(Propositional Logic)와 일차 술어 논리(First-order Logic)를 기초로, 모델 체킹(Model Checking)과 자동 정리 증명(Automated Theorem Proving) 기법을 습득하여 분산 시스템이나 암호화 프로토콜 같은 미세한 결함도 사전에 차단하는 고도의 엔지니어링 역량을 배양합니다.

2. Scope & Boundaries

In-Scope

• 컴퓨팅 논리 기초: 명제/술어 논리, 정규화(CNF/DNF), 논리적 추론 법칙
• 형식 증명 기법: 자연 연역(Natural Deduction), 수리적 귀납법, 분해법(Resolution)
• 자동 추론 도구: SAT 및 SMT 솔버의 이론적 원리와 프로그래밍적 적용
• 시스템 모델 검증: 상태 전이 시스템, 시간 논리(LTL/CTL), 시스템 불변량(Invariants) 증명

Out-of-Scope

• 비결정적인 순수 철학적 논리학 및 수사학 (비기술 도메인)
• 전통적인 동적 테스트 및 QA 자동화 프로세스 (09. Software Engineering 영역으로 위임)
• 암호학적 프로토콜의 성능 분석 (10. Security & Cryptography 영역으로 일부 위임)

Boundaries

• LFV vs. Testing: SWEBOK 및 CyBOK에 따르면, Testing은 '프로그램 실행 결과'를 관찰하는 경험적(Empirical) 활동이나, LFV는 '모델의 모든 가능한 상태 공간'을 수학적으로 탐색하여 결론을 도출하는 정적인 성격이 강합니다.

3. Counterexample

• 단순히 코드의 특정 경로를 디버거로 한 줄씩 확인하거나 에지 케이스를 손으로 입력해보는 행위는 LFV가 아닙니다. 시스템의 **불변 조건(Invariant)**을 논리식으로 정의하고, 어떤 입력 시퀀스에서도 해당 조건이 거짓이 되지 않음을 **모델 체커(TLA+, SPIN 등)**를 통해 모든 탐색 경로에서 입증해야 진정한 의미의 형식 검증입니다.

4. Prerequisites

• 이산 구조 및 모델링 (Recommended): 집합론과 관계에 대한 이해가 원활한 논리식 모델링과 관계 대수적 해석에 필수적입니다. (01. Discrete Structures)

5. Learning Map

1. Syntax & Semantics: 논리 기호의 의미와 문장 구성 원리(Well-formed Formulas)를 명확히 정의합니다.
2. Formal Proofs: 수작업 증명을 통해 논리적 추론의 엄밀함을 연습하고 연역적 사고를 강화합니다.
3. Automated Reasoning: SAT/SMT 솔버 도구를 이용해 수만 개의 변수가 포함된 제약 조건을 자동 해결하는 법을 익힙니다.
4. Formal Verification Tools: TLA+, Alloy, SPIN 등을 사용해 실무의 분산 알고리즘이나 커널 레벨 시스템을 정밀 검토합니다.

6. Learning Topics

Basic

Core: 명제 논리와 추론 법칙 (Propositional Logic & Rules of Inference)

• Why to Learn: 프로그램 조건문의 결합과 불리언 연산의 무결성을 판단하기 위한 가장 기초적인 도구이기 때문입니다.
• What to Learn:
  • AND, OR, NOT, Implication(함축)의 논칙적 결합
  • 진리표(Truth Table)를 이용한 항진식(Tautology) 및 모순(Contradiction) 판별
  • 긍정 논법(Modus Ponens), 부정 논법(Modus Tollens) 등 기초 추론 규칙
• How to Learn:
  • 복합적인 자연어 문장을 논리 기호로 변환하는 연습
  • 특정 논리식이 항상 참임을 진리표로 증명하기
• Implement: 파이썬 등을 이용한 간단한 진리표 생성기 프로그래밍

Recommended

Core: 일차 술어 논리와 증명론 (First-order Logic & Proof Theory)

• Why to Learn: 객체와 그 성질, 한정자를 다루어야만 실제 시스템의 복잡한 요구사항을 명세할 수 있기 때문입니다.
• What to Learn:
  • 전칭 한정자(Universal)와 존재 한정자(Existential)의 적용
  • 정규형 변환(CNF, DNF) 및 스콜렘화(Skolemization)
  • 분해법(Resolution)을 이용한 기계적 증명 원리
• How to Learn:
  • '모든 사용자는 접근 권한이 있다' 같은 비정형 요구사항을 일차 논리식으로 명세
  • 모순 증명(Proof by Contradiction)을 활용한 수학적 정리 증명 연습
• Implement: 명제 논리식을 CNF로 변환하는 파서 구현

Practical

Core: SAT/SMT 솔버 활용 (SAT/SMT Solver Application)

• Why to Learn: 현대 소프트웨어 검증, 스케줄링, 리소스 할당 문제를 수작업이 아닌 자동화된 도구로 해결하기 위해서입니다.
• What to Learn:
  • DPLL 알고리즘과 Conflict-Driven Clause Learning (CDCL)의 이해
  • SMT(Satisfiability Modulo Theories) 솔버의 배경 이론(Linear Arithmetic, Bit-vectors)
  • Z3 솔버 API를 이용한 제약 조건 프로그래밍
• How to Learn:
  • 스도쿠 퍼즐 해결이나 패키지 의존성 문제를 SAT 모델로 만들어 솔버 실행
  • 불리언 변수를 이용해 하드웨어 소자의 상태 도출 실습
• Implement: Z3 Python API를 활용한 서버 리소스 배치 최적화 도구

Advanced

Core: 모델 체킹 및 시공간 논리 (Model Checking & Temporal Logic)

• Why to Learn: 시간의 흐름에 따라 상태가 변하는 시스템(분산 시스템, OS 커널)의 안전성을 보장하기 위함입니다.
• What to Learn:
  • LTL(Linear Temporal Logic)과 CTL(Computation Tree Logic) 연산자 기초
  • 교착 상태(Deadlock) 및 기아 상태(Starvation)를 논리적으로 정의
  • TLA+(Temporal Logic of Actions)를 이용한 알고리즘 설계 검증
• How to Learn:
  • 간단한 분산 락(Distributed Lock) 알고리즘을 TLA+로 명세하고 위반 사례 탐지
  • SPIN 모델 체커를 이용해 메시지 큐의 데이터 유실 가능성 검사
• Implement: Raft 또는 Paxos 합의 알고리즘의 주요 불변량을 정의한 TLA+ 명세서

7. Terminology

8. References

Primary References

• [P1] CS2023 - Basic Logic — Foundations of computational logic.
• [P3] CyBOK - Formal Methods — Security verification and rigorous analysis.

Secondary References

• [Logic in Computer Science] Huth & Ryan, Cambridge University Press — The de facto standard textbook.
• [Specifying Systems] Leslie Lamport (TLA+) — Guide to rigorous system design.

Industry References

• [AWS Architecture] Using TLA+ for Service Overhaul — Amazon's experience in formal methods.
• [Microsoft Research] Z3 Solver Documentation — Practical SMT solver resource.

9. Final Checklist

Primary Checklist

• 비정형 요구사항이나 서버 동작 규칙을 일차 논리식으로 모호성 없이 기술할 수 있는가? (P1, P3)
• SAT/SMT 솔버를 사용해 대규모 불리언 변수가 포함된 제약 조건 충족 문제를 자동화할 수 있는가? (P1)

Secondary Checklist

• 시스템의 불변량(Invariant)과 진행 속성(Liveness)을 정의하고 상태 전이 추상 모델에서 검토할 수 있는가?
• '모든 실행 경로'에 대한 논리적 증명이 '샘플 기반 테스트' 대비 가지는 엔지니어링적 우위를 설명할 수 있는가?

Industry Checklist

• TLA+나 SPIN 같은 도구를 활용해 복잡한 병행성 시스템의 교착 상태를 구동 전 탐지할 수 있는가?
• 하드웨어 명세 혹은 프로토콜 설계를 논리 모델로 추상화하여 보안 취약점을 증명할 수 있는가?