7 posts
unit tests는 특정 입력을 검증합니다. symbolic execution은 모든 가능한 입력을 검증합니다. 작동 방식, 비용, 시작 방법을 알아보세요.
테스트 스위트는 94% 커버리지와 0개의 실패를 기록했습니다. symbolic execution 엔진은 3초 만에 코드의 크래시를 찾아냅니다. 테스트가 고장 난 것이 아닙니다. 커버리지 지표가 거짓말을 하는 것도 아닙니다. 문제는 테스트가 특정 지점에서의 동작을 검증한다는 것입니다.…
추상 해석은 실행 전에 런타임 에러가 불가능함을 증명하게 해줍니다. 실제로 어떻게 작동하는지, 왜 어려운지, 그리고 도구 체인의 어디에 맞는지 알아봅니다.
테스트 스위트는 통과했다. 타입 체커는 초록불이다. 배포했다. 두 시간 후, 프로덕션에서 아묏도 테스트하지 않은 엣지 케이스에서 가 발생했다. 테스트는 버그를 찾는다. 타입은 일부를 방지한다. 둘 다 프로그램이 런타임 에러로부터 자유롭다는 것을 증명하지는 못한다. 그것을 위해서는 더…
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, 그리고 단일 장애점을 뛰어넘었다는 따뜻한 만족감까지. 하지만 함수들이 동등하다는 것을 증명한 게 아니다. 컴파일된다는 것만 증명했을 뿐이다.…