9 posts
AutoVerus는 LLM 에이전트 네트워크를 사용해 Rust 코드에 대한 Verus 정합성 증명을 생성하며, SMT 솔버 피드백에 의해 구동되는 생성-수정-디스차지 루프를 통해 90% 이상의 증명 의무를 자동화한다.
형식 검증에서 가장 어려운 부분은 검증기 자체가 아니다. 증명을 작성하는 것이다. 숙련된 Rust 엔지니어에게 Microsoft Research의 SMT 기반 검증기인 Verus를 주면, 오후 한때에 함수에 precondition과 postcondition을 주석으로 달 수 있다.…
대규모 언어 모델은 놀랄 만큼 훌륭한 Rust 코드를 작성하지만, 형식적 증명을 요청하면 불변 조건을 환각으로 만들어내고 어떤 검증기도 받아들이지 않는 문법을 지어낸다. 이들이 실제로 제대로 하는 것, 실패하는 부분, 그럼에도 불구하고 활용하는 방법을 소개한다.
LLM은 컴파일되고 까지 통과하는 Rust 코드를 작성할 수 있다. 하지만 모든 가능한 입력에 대해 코드가 올바르다는 형식적 증명을 믿을 수 있게 작성하는 것은 아직 불가능하다. 문제는 Rust 문법이 아니다. 형식적 검증에서는 무엇을 증명할지 명시하고, 증명을 성립시키는 불변 조건을…
Kani 같은 model checking 도구를 사용하면 형식적 증명 대신 단언으로 Rust 속성을 검증할 수 있다. 문제는 루프의 경계가 작지 않을 때 무슨 일이 일어나는지다.
한 줄의 증명도 쓰지 않고 Rust 코드의 정확성을 증명할 수 있다. 이 일을 하는 도구를 model checker라 부르며, 현재 Rust 에 가장 실용적인 것은 AWS 가 개발한 Kani 다. 평범한 Rust 단언을 작성하면 된다. Kani 는 이를 수학적 명제로 변환하고 가능한…
Rust 표준 라이브러리는 모든 의존성에 주변 파일 시스템 권한을 부여한다. cap-std는 이를 기능 기반 API로 대체하여 코드가 파일을 열기 전에 해당 경로에 접근할 권리가 있음을 증명하도록 강제한다.
의존성 트리의 모든 크레이트는 를 열거나 디렉터리에 쓰거나, 프로젝트의 모든 파일을 열거할 수 있다. Rust 표준 라이브러리는 접근 권한을 묻지 않는다. 을 호출할 수 있는 코드라면 운영체제가 허용하는 어떤 경로든 접근할 수 있다고 가정한다. cap-std는 이러한 가정을 뒤집는다.…
던져진 예외는 실패 경로를 타입 시스템에서 감춥니다. 명시적인 에러 반환이 코드를 더 정직하게 만드는 이유, 그리고 삶을 싫어하지 않으면서 이를 도입하는 방법을 알아봅니다.
함수 시그니처가 를 반환한다고 합니다. 그렇지 않습니다. 를 반환하거나 폭발합니다. 타입 시스템은 두 번째 분기에 대해 전혀 모릅니다. 이것이 예외 기반 에러 핸들링의 근본적인 불성실함입니다. 모든 는 컴파일러가 볼 수도, 검사할 수도, 강제할 수도 없는 제어 흐름 경로입니다.…
단일 필드 래퍼 struct가 단 한 바이트의 오버헤드도 추가하지 않고 단위 혼합 버그와 타입 혼란을 잡아낸다.
인 사용자 ID를 주문 ID를 기대하는 함수에 넘기면 Rust는 불평하지 않는다. 둘 다 이기 때문이다. 컴파일러는 두 타입이 동일하게 보이므로 당신을 도울 수 없다. 버그는 런타임에, 보통 프로덕션에서, 보통 당신이 안전하다고 생각한 리팩터링 이후에야 발견된다. 이것이 바로…
cargo-mutants는 코드를 검증하는 척만 하는 테스트를 찾아낸다. Rust에서 뮤테이션 테스트가 어떻게 작동하는지, 무엇을 잡아내는지, 그리고 컴파일 시간 비용이 감당할 만한 가치가 있는지 알아본다.
라인 커버리지는 100%다. 모든 분기를 커버한다. 모든 함수를 호출한다. 그런데 누군가 가격 책정 로직에서 를 로 바꾸고 테스트를 돌리면, 테스트가 모두 통과한다. 이것은 이론적인 문제가 아니다. 테스트가 코드를 실행하지만 실제로는 동작을 검증하지 않을 때 벌어지는 일이다.…
Example-based testing은 당신이 생각해낸 입력만 커버한다. Property-based testing은 무작위 데이터를 생성하고, invariant를 검증하며, 실패를 최소한의 counterexample로 축소한다.
당신은 함수를 작성했다. 과 로 테스트했다. 통과했다. 배포했다. 한 사용자가 한 개의 원소를 가진 slice를 넘겼다. 당신의 함수는 그것을 무시하고 지나쳤다. 이슈가 열렸다. 당신은 테스트 파일을 응시하며 이렇게 뻔한 것을 어떻게 놓쳤는지 의아해한다. 놓친 이유는…
Rust는 디버그 assertions를 자동으로 제거하지만, 진정한 design-by-contract는 debug_assert! 이상의 것이 필요하다. 릴리스 바이너리에서 완전히 사라지는 zero-cost runtime contracts를 만드는 방법을 소개한다.
Rust는 개발 환경에서 runtime contracts를 강제할 수 있고, 릴리스 빌드에서는 완전히 지워버릴 수 있다. 전제 조건은 이 언어가 contract를 first-class 개념으로 다루지 않는다는 것이다. 필요한 구성 요소는 주어지지만, 직접 연결해야 한다. 는 가장 먼저…