형식 검증 및 증명 보조 도구

형식 검증은 소프트웨어가 사양을 충족하는지 기계적으로 검증된 수학적 증명을 통해 확립하는 것이며, 증명 보조 도구는 이러한 증명을 구축하고 확인하는 도구입니다.

Definition

형식 검증은 시스템이 형식 사양을 만족한다는 엄격하고 기계적으로 검증된 증명을 구성하는 것이며, 증명 보조 도구는 사용자가 그러한 증명을 개발하고 그 유효성을 기계적으로 확인하도록 돕는 소프트웨어입니다.

Scope

이 주제는 연역적 검증과 대화형 정리 증명을 다룹니다. 여기에는 유형 이론 또는 고차 논리(Coq, Isabelle, Lean, Agda 등)에 기반한 증명 보조 도구, 신뢰할 수 있는 증명을 위한 LCF 접근 방식, 명제-유형 동치(propositions-as-types) 기반, 증명 자동화 및 전술, 그리고 컴파일러 및 운영 체제 커널을 포함한 주요 검증된 아티팩트가 포함됩니다.

Core questions

• 완전한 기능적 정확성을 어떻게 증명하고 기계적으로 확인할 수 있는가?
• 증명 보조 도구는 왜 신뢰할 수 있으며, 신뢰할 수 있는 컴퓨팅 기반(trusted computing base)은 무엇인가?
• 커리-하워드 대응(Curry-Howard correspondence)은 증명과 프로그램을 어떻게 연결하는가?
• 컴파일러 및 커널과 같은 실제 시스템을 검증하는 데 무엇이 필요한가?

Key theories

신뢰할 수 있는 증명을 위한 LCF 접근 방식

고든(Gordon), 밀너(Milner), 워즈워스(Wadsworth)의 에든버러 LCF는 모든 정리가 통과해야 하는 작은 신뢰할 수 있는 증명 커널을 도입하여 복잡한 자동화조차도 불건전한 증명을 생성할 수 없도록 했습니다.

검증된 컴파일러 (CompCert)

르로이(Leroy)의 CompCert는 증명 보조 도구에서 정확성이 증명된 C 컴파일러로, 생성된 코드가 소스 프로그램의 의미론을 정제한다는 기계적으로 검증된 정리를 포함합니다.

검증된 운영 체제 커널 (seL4)

클라인(Klein)과 동료들은 seL4 마이크로커널에 대한 기능적 정확성 기계 검증 증명을 생성하여 저수준 시스템 소프트웨어의 종단 간 검증을 시연했습니다.

Clinical relevance

기계화된 검증은 중요한 소프트웨어에 대해 가장 높은 수준의 보증을 제공하며, 테스트 기반의 신뢰 대신 입증된 보증을 통해 컴파일러, 커널 및 암호화 라이브러리를 생산합니다. 증명 보조 도구는 또한 수학 자체를 형식화하는 데 점점 더 많이 사용되고 있습니다.

History

대화형 정리 증명은 1970년대 에든버러 LCF에서 시작되었으며, 그 ML 메타언어와 신뢰할 수 있는 커널은 이후 시스템에 영향을 미쳤습니다. Coq 및 Agda와 같은 유형 이론 기반 보조 도구와 Isabelle/HOL과 같은 고차 논리 시스템은 수십 년에 걸쳐 발전하여 CompCert 컴파일러(2009) 및 seL4 커널(2009)과 같은 획기적인 검증된 아티팩트를 탄생시켰습니다.

Debates

검증 비용 대 얻어지는 보증

대규모 시스템에 대한 기계 검증 증명을 구축하는 데는 막대한 노력이 필요하며, 이는 완전한 검증이 정당화되는 경우와 경량 방법으로 충분한 경우, 그리고 증명을 얼마나 자동화할 수 있는지에 대한 논쟁을 불러일으킵니다.

Key figures

• Robin Milner
• Michael Gordon
• Xavier Leroy
• Gerwin Klein
• Robert Harper

Seminal works

• gordon1979
• leroy2009
• klein2009
• harper2016

Frequently asked questions

증명 보조 도구란 무엇인가?

증명 보조 도구는 사용자가 시스템이 모든 단계를 기계적으로 확인하는 동안 형식 증명을 대화식으로 구성하는 소프트웨어로, 완성된 증명은 작고 면밀히 검토된 커널에 이르기까지 신뢰할 수 있습니다.

프로그램 검증은 테스트와 어떻게 다른가?

테스트는 선택된 입력에 대한 동작을 확인하고 버그의 존재만을 밝힐 수 있는 반면, 형식 검증은 사양에 의해 허용되는 모든 입력에 대한 정확성을 증명하여 지정된 오류의 부재를 확립합니다.