5 posts
Cleanroom software engineering은 디버깅 대신 mathematical verification을 통해 zero-defect increment를 약속했다. 우리는 IBM의 실제 프로젝트 데이터를 살펴보아 그 주장이 성립했는지 본다.
1980년대 소프트웨어 업계 평균은 천 줄당 30~60개의 결함이었다. IBM의 Cleanroom 팀은 2만 줄짜리 컴파일러 인크리먼트를 테스트에서 53개의 결함이 발견된 상태로 출시했다. 이는 KLOC당 2.6개이다. 1만 줄짜리 개별 인크리먼트 중 일부는 시스템 테스트에서 결함이…
AutoVerus는 LLM 에이전트 네트워크를 사용해 Rust 코드에 대한 Verus 정합성 증명을 생성하며, SMT 솔버 피드백에 의해 구동되는 생성-수정-디스차지 루프를 통해 90% 이상의 증명 의무를 자동화한다.
형식 검증에서 가장 어려운 부분은 검증기 자체가 아니다. 증명을 작성하는 것이다. 숙련된 Rust 엔지니어에게 Microsoft Research의 SMT 기반 검증기인 Verus를 주면, 오후 한때에 함수에 precondition과 postcondition을 주석으로 달 수 있다.…
Kani 같은 경계 model checker과 Alloy 같은 관계 모델 탐색기는 일반적인 어서션과 제약 조건으로 속성을 검증할 수 있게 한다. 활성 증명을 포기하는 대신, 학습 곡선은 주가 아닌 시간 단위로 측정된다.
model checker을 사용하기 위해 선형 시간 논리를 배울 필요는 없다. Kani, CBMC, Alloy 같은 도구는 일반적인 어서션과 관계 제약으로 속성을 검증할 수 있게 한다. 활성 속성을 증명하는 능력을 포기하는 대신, 학습 곡선은 주 대신 시간 단위로 측정되며, 대부분의…
Kani 같은 model checking 도구를 사용하면 형식적 증명 대신 단언으로 Rust 속성을 검증할 수 있다. 문제는 루프의 경계가 작지 않을 때 무슨 일이 일어나는지다.
한 줄의 증명도 쓰지 않고 Rust 코드의 정확성을 증명할 수 있다. 이 일을 하는 도구를 model checker라 부르며, 현재 Rust 에 가장 실용적인 것은 AWS 가 개발한 Kani 다. 평범한 Rust 단언을 작성하면 된다. Kani 는 이를 수학적 명제로 변환하고 가능한…
N-version programming은 구현체들이 서로 일치한다고 가정한다. 테스트가 왜 부족한지, SMT solver가 어떻게 실제로 동등성을 증명할 수 있는지, 그리고 '충분히 좋음'과 '형식적으로 검증됨' 사이의 경계를 어디에 그어야 하는지 살펴본다.
n-version 시스템을 구축했다. 동일한 중요 함수를 독립적으로 구현한 세 가지 구현체, 다수결 결과를 선택하는 voter, 그리고 단일 장애점을 뛰어넘었다는 따뜻한 만족감까지. 하지만 함수들이 동등하다는 것을 증명한 게 아니다. 컴파일된다는 것만 증명했을 뿐이다.…