From LaTeX and OCaml to LEAN4 and Executables: Lean-Checked Theorems and Generating Proof-Carrying Rust
이 논문은 상호 귀납적 타입, 부호 있는 정수 산술, 그리고 커널과 그 자기 기술적 방정식의 교차 구현 검증을 통해 시스템을 성공적으로 입증하며, Lean 4로 검증된 정리와 증명 탑재 계약(proof-carrying contracts)을 갖춘 실행 가능한 Rust 코드를 동시에 생성하는 OCaml의 부분 집합에 대한 Python 기반 Hindley–Milner 프런트엔드를 제시한다.
원본 논문은 CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기
소프트웨어의 세계에는 코드를 작성하는 방식과 그 코드가 안전하다는 것을 어떻게 아느냐 사이의 끊임없는 긴장이 존재합니다. 프로그래머들은 복잡한 로직을 읽기 쉽고 관리하기 용이한 방식으로 기술하기 위해 고수준 언어를 사용하지만, 이 코드를 실행하는 기계는 훨씬 더 단순하고 엄격한 언어를 사용합니다. 한 단계에서 다른 단계로 넘어가기 위해 컴파일러는 번역가 역할을 하지만, 바로 이 번역 과정에서 오류가 숨어들곤 합니다. 번역상의 실수는 안전한 명령을 위험한 명령으로 바꾸어 프로그램이 충돌하거나 예측 불가능하게 동작하게 만들 수 있습니다. 수십 년 동안 안전성을 보장하는 가장 신뢰할 수 있는 방법은 최종 기계 코드를 검증하는 것이었으나, 이는 원래 프로그램의 고수준 의미가 번역 과정에서 소실되는 경우가 많기 때문에 매우 어려운 일이었습니다. 연구자들이 던지는 질문은, 우리가 최종 기계 명령이 의도한 대로 정확히 수행될 것임을 절대적인 확신을 가지고 증명하면서도, 동시에 원래의 고수준 언어가 가진 명료함을 유지할 수 있는가 하는 것입니다.
브렌트 하트숀(Brent Hartshorn)은 하나의 코드 조각을 동시에 두 가지 서로 다른 것으로 취급함으로써 이 질문에 답하는 시스템을 구축했습니다. 마치 하나의 문서를 수학적 증명서인 동시에 기계를 위한 명령 세트로 동시에 읽을 수 있다고 상상해 보십시오. 이 새로운 연구에서 저자는 데이터가 처리되는 방식에 대해 엄격한 규칙을 가진 것으로 알려진 OCaml이라는 프로그래밍 언어의 하위 집합을 가져와, 모든 정의에 두 가지 뚜렷한 의미를 부여합니다. 첫째, 코드는 논리적 논거로서 읽히며, 프로그램의 구조 자체가 특정 조건이 항상 충족될 것임을 입증하는 증명 역할을 합니다. 둘째, 동일한 코드는 속도와 안전성을 위해 설계된 Rust라는 다른 언어로 번상되며, 이후 컴퓨터가 실제로 실행할 수 있는 프로그램으로 컴파일됩니다. 이 접근 방식의 탁월함은 검증에 있습니다. 논리적 증명은 작고 신뢰할 수 있는 수학적 엔진에 의해 확인되는 한편, 실행되는 프로그램은 코드를 단계별로 시뮬레이션하는 참조 인터프리터에 의해 대조됩니다. 만약 이 둘이 일치하고 논리적 증명이 성립한다면, 그 결과물은 자체적인 안전 인증서를 갖춘 소프트웨어가 됩니다.
연구진은 먼저 특정 OCaml 슬라이스를 이해하는 번역기를 구축하는 것부터 시작했습니다. 파이썬(Python)으로 작성된 이 번역기는 한 사람이 읽고 이해할 수 있을 만큼 충분히 작으며, 이는 번역기 자체가 너무 복잡하면 그 출력물을 신뢰할 수 없기 때문에 매우 중요한 요소입니다. 이 번역기는 OCaml 코드를 가져와 두 갈래의 경로로 나눕니다. 증명 경로에서는 코드를 수학적 커널이 확인할 수 있는 형식으로 변환합니다. 이 커널은 어떠한 가정도 없이 논리가 타당한지 검증하는 아주 작은 프로그램인 판사 역할을 합니다. 프로그램 경로에서 번역기는 코드를 Rust로 변환하며, Rust는 빠른 네이티브 기계 코드로 컴파일됩니다. 번역이 완벽했는지 확인하기 위해 연구진은 원래의 OCaml 코드를 직접 실행하는 참조 인터프리터도 함께 구축했습니다. 그 후 13개의 서로 다른 예제 프로그램을 컴파일된 Rust 버전과 인터프리터 모두에 통과시켰습니다. 모든 경우에서 컴파일된 코드는 인터프리터와 정확히 동일한 출력을 생성했으며, 이는 번역 과정이 프로그램의 동작을 변경하지 않았음을 입증했습니다.
코드가 성공적으로 번역되면, 팀은 컴파일된 Rust 버전에 대해 엄격한 안전 점검을 적용했습니다. 그들은 컴파일된 코드를 하나의 계약으로 취급하였는데, 프로그램이 어떻게 동작해야 하는지에 대한 특정 규칙들이 수학적 정리로서 기록되었습니다. 예를 들어, 정수 계산이 실수로 오버플로(overflow)되어 음수로 돌아가는 현상이 발생하지 않는지 확인했습니다. 이는 소프트웨어 버그의 흔한 원인입니다. 연구진은 이러한 안전 규칙 대부분은 유효했지만, 규칙이 깨지는 특정 엣지 케이스(edge cases)가 존재한다는 것을 발견했습니다. 11가지 서로 다른 시나리오에서, 컴파일된 코드는 0에서 가장 작은 숫자를 뺄 때와 같이 정수 계산이 되돌아가는(wrap around) 지점에 도달했습니다. 시스템은 이를 '열린 의무(open obligations)'로 정확히 식별해 냈는데, 이는 코드가 특정 알려진 한계점들을 제외하고는 모든 곳에서 안전하다는 것을 의미합니다. 총 90개의 안전 점검 중 79개는 완전히 증명되었으나, 나머지 11개는 컴퓨터가 숫자를 처리하는 방식에 있는 실제적인 한계치를 나타냈기에 미결 상태로 남겨두었습니다.
이 프로젝트는 더 나아가 컴퓨터 자원을 관리하는 핵심 소프트웨어인 소규모 운영체제 커널에 이 방법을 적용했습니다. 연구진은 기존에 파이썬과 Rust로 작성되었던 커널을 가져와 이를 자신들의 OCaml 하위 집합으로 다시 작성했습니다. 그런 다음 이 새로운 버전을 Rust로 번역하고 컴파일했습니다. 그 결과물은 동일한 커널의 세 번째 구현체가 되었습니다. 원래의 파이썬 버전과 대조했을 때, OCaml에서 파생된 이 새로운 버전은 236개의 모든 테스트 케이스에서 정확하게 응답했습니다. 팀은 이 새로운 커널의 안전성을 증명하려고 시도했습니다. 그들은 236개의 안전 의무 중 227개를 성공적으로 증명했습니다. 증명되지 않은 소수의 사례는 코드의 오류가 아니라, 복잡한 루프와 카운터를 처리하는 방식과 관련된 수학적 도구의 공백 때문이었습니다. 이는 이 방법이 작은 예제를 넘어 기능적인 운영체제 구성 요소로 확장될 수 있음을 보여주었습니다.
아마도 이 작업에서 가장 놀라운 부분은 수학 방정식을 작동하는 프로그램으로 직접 변환하는 능력이었습니다. 연구진은 커널의 동작을 설명하는 표준 수학 표기법의 형식을 갖춘 공식 방정식을 가져와, 이를 OCaml 코드로 변환하는 도구에 입력했습니다. 이 코드는 컴파일되어 실행되었습니다. 결과물인 프로그램은 방정식이 설명하는 대로 정확하게 동작했으며, 모든 사례에서 원래의 파이썬 모델의 출력과 일치했습니다. 이 과정은 고수준의 수학적 기술이 그 의미를 잃지 않고 검증된 실행 가능한 바이너리로 변환될 수 있음을 보여주었습니다. 팀은 이 방정식의 컴파일된 버전이 대부분의 안전 계약을 충족함을 증명했으나, 더 복잡한 논리 단계 중 일부는 체크 도구의 추가적인 개선이 필요했습니다.
이 연구의 결과는 신뢰할 수 있는 소프트웨어를 구축하는 새로운 길을 제시합니다. 고수준 소스 코드를 유지하면서 그 논리적 의미와 컴파일된 형태를 모두 검증함으로써, 연구진은 최종 프로그램의 안전성이 수학적 증명에 의해 뒷받받되는 시스템을 만들어냈습니다. 이 방법은 정수 오버플로와 같이 컴퓨터가 숫자를 다루는 방식에서의 실제적인 한계를 성공적으로 식별해 냈으며, 이를 실제 버그와 구별해 냈습니다. 비록 시스템이 가장 복잡한 커널 부분의 모든 안전 규칙을 증명하지는 못했지만, 대다수를 증명해 냈으며, 미결로 남은 부분들은 코드가 아닌 체크 도구가 개선되어야 할 영역임을 명확히 밝혔습니다. 이 연구는 고수준 코드에서 기계 명령으로의 번역 과정을 제어함으로써, 최종 실행 파일이 그 코드를 만든 논리만큼이나 엄격한 안전 인증서를 지닐 수 있음을 보여주는 증거입니다.
연구 분야의 논문에 파묻히고 계신가요?
연구 키워드에 맞는 최신 논문의 일일 다이제스트를 받아보세요 — 기술 요약 포함, 당신의 언어로.