[Paper] 다중 언어 계약 추적성을 위한 Minimal Executable Proof

Source: arXiv - 2605.28546v1

개요

Werner Kasselman의 논문은 작고 완전 실행 가능한 개념 증명을 제시하여, 간단한 “Hello, world!” 계약을 여섯 가지 프로그래밍 언어(Rust, Go, C, Java, TypeScript, 그리고 AWK)에서 엔드‑투‑엔드 추적성을 보여줍니다. 각 구현을 단일 관찰 가능한 계약, 의존성 그래프, 추적 파일, 준비 게이트, 그리고 증거 매트릭스에 연결함으로써, 자동 검사가 모든 아티팩트가 실제로 계약을 만족하는지를 검증할 수 있음을 보여줍니다—단, 이를 프로덕션 수준의 보증 시스템이라고 주장하지는 않습니다.

주요 기여

• Minimal multi‑language artifact: 하나의 계약에 연결된 여섯 개의 서로 다른 “Hello, world!” 프로그램.
• Executable contract definition: 계약은 구체적인 관찰 가능 객체(정확한 UTF‑8 출력 Hello, world!\n, stderr 없음, 종료 코드 0)이다.
• Implementation DAG & traceability file: 방향성 비순환 그래프(DAG)가 소스 파일, 빌드 단계, 계약 간의 관계를 포착한다.
• Readiness gate & evidence matrix: 테스트 결과에 따라 아티팩트 승격을 제어하고 기계 판독 가능한 증거 보고서를 생성하는 자동 검사.
• Side‑car witnesses: 두 개의 추가 검증자는 소스‑분석 도구(예: sqry)가 코드 변환 후에도 인사 문자열을 찾을 수 있음을 보여준다.
• Open, falsifiable artifact: 전체 설정을 복제하고 실행하며(예: 출력을 변경하여) 깨뜨릴 수 있어 재현 가능한 시연이며 벤치마크가 아니다.

Methodology

1. 구체적인 계약 정의 – 프로그램을 실행하고, stdout, stderr, 종료 코드를 캡처한 뒤 기대값과 비교하는 witness harness 형태로 표현합니다.
2. 구현 생성 – 서로 다른 언어로 작성된 여섯 개의 작은 프로그램을 만들어 정확히 계약된 출력을 내보냅니다.
3. 구현 DAG 구축 – 노드는 소스 파일이나 빌드 단계를 나타내고, 엣지는 “의존 관계”(예: go build는 main.go에 의존)를 인코딩합니다.
4. 추적 파일 생성 – JSON/YAML 매니페스트가 DAG의 각 노드를 해당 계약에 매핑합니다.
5. 준비 게이트 실행 – 자동화 스크립트가 DAG를 순회하면서 각 구현을 실행하고 PASS/SKIP/FAIL 결과를 기록합니다.
6. 증거 매트릭스 생성 – 게이트는 간결한 표(“evidence matrix”)를 출력하여 다운스트림 CI/CD 또는 감사 도구가 활용할 수 있게 합니다.
7. 사이드‑카드 위트니스 추가 – 두 개의 추가 검사는 정적 분석 쿼리(sqry)를 사용해 인사 문자열이 코드 리팩터링 후에도(Go) 혹은 검증기가 지원하지 않는 언어(AWK)에서도 여전히 발견 가능한지 확인합니다.

모든 단계는 표준 도구(쉘, make, 언어별 컴파일러/인터프리터)로 스크립트화되어 일반 개발자 워크스테이션에서 실행할 수 있습니다.

결과 및 발견

Side‑car witnesses는 다음을 확인했습니다:

• Go 버전은 소스 텍스트에 리터럴을 숨기는 “복잡한 재작성”에도 불구하고 AST 수준에서 인사말을 노출시켜 쿼리가 성공하도록 했습니다.
• AWK 버전은 검증기의 언어 허용 목록에 포함되지 않았지만 선언된 소스 프로필에 연결될 수 있어 메타데이터를 통해 추적성을 확장할 수 있음을 보여줍니다.

이 결과는 작고 재현 가능한 아티팩트가 이질적인 코드베이스 전반에 걸쳐 계약을 강제할 수 있음을, 그리고 소스 변환이 발생하더라도 추적성 체인이 유지된다는 것을 증명합니다.

Practical Implications

• Cross‑language compliance checks – 다중 언어 서비스를 유지하는 팀은 가벼운 계약 + DAG 접근 방식을 채택하여 모든 언어 구현이 공유 API 또는 출력 계약을 준수하도록 보장할 수 있습니다.
• CI/CD gate integration – 준비 게이트를 기존 파이프라인(GitHub Actions, Jenkins, GitLab CI)에 연결하면 구현 중 하나라도 계약을 위반할 경우 자동으로 머지를 차단합니다.
• Audit‑ready evidence – 생성된 증거 매트릭스는 기계가 읽을 수 있는 증명을 제공하여 수동 서명 없이도 규제 또는 내부 컴플라이언스 감사를 충족할 수 있습니다.
• Rapid prototyping of traceability frameworks – 아티팩트가 최소이기 때문에 개발자는 더 큰 코드베이스로 확장하기 전에 다양한 그래프 표현, 메타데이터 형식, 정적 분석 백엔드를 실험할 수 있습니다.
• Educational tool – 신규 입사자나 학생들은 레포를 복제하고 계약을 깨뜨려(예: 출력 문자열 변경) 게이트가 실패하는 것을 확인함으로써 재현 가능한 소프트웨어 보증 개념을 직접 체험할 수 있습니다.

제한 사항 및 향후 작업

• 범위가 사소한 계약에만 제한됨 – 증명은 단일 정적 문자열을 사용합니다; 실제 계약은 종종 복잡한 스키마, 네트워크 상호작용, 또는 비결정적 동작을 포함합니다.
• 환경 의존성 – 실행 환경에 도구가 없어 Java 구현을 생략했습니다; 실제 운영에서는 견고한 환경 프로비저닝(Docker 이미지, 툴체인)이 필요합니다.
• 검증기 언어 지원 범위 – 정적‑분석 사이드카는 일부 언어만 지원합니다; sqry 또는 유사 도구를 확장해 더 많은 생태계를 포괄하는 것은 아직 해결 과제입니다.
• 확장성 – 현재 DAG와 추적 파일은 수작업으로 만들었습니다; 향후 작업에서는 빌드 시스템(Bazel, Gradle)으로부터 자동 생성 및 대규모 의존성 그래프 처리 방안을 탐구할 수 있습니다.
• 보안 및 샌드박스 – 게이트의 일부로 임의 구현을 실행하면 보안 문제가 발생합니다; 샌드박스 실행(e.g., Firecracker, gVisor) 통합이 더 넓은 채택을 위해 필요합니다.

이러한 사항들을 해결하면 최소 실행 증명을 계약 기반 개발 및 지속적인 보증을 위한 견고하고 언어에 구애받지 않는 프레임워크로 발전시킬 수 있습니다.

저자

• Werner Kasselman

논문 정보

• arXiv ID: 2605.28546v1
• 분류: cs.SE
• 출판일: 2026년 5월 27일
• PDF: Download PDF