AI 퍼스트 개발, 코딩 가드레일, 그리고 폐기 가능한 아키텍처를 탐구합니다.
Meta의 Infer는 abstract interpretation과 양방향 추론을 사용해 코드 구조를 분석하여 null reference, memory leak, race condition을 발견한다. 실행은 필요 없다. 작동 방식과 자체 코드베이스에서의 활용법을 설명한다.
Meta는 코드가 사용자에게 도달하기 전에 정적 분석기가 포착한 10만 건 이상의 버그 수정을 배포했다. 이 도구의 이름은 Infer이며 오픈 소스이고 코드를 실행하지 않는다. 코드를 읽어 코드가 할 수 있는 동작의 수학적 모델을 구축하고, 특정한 나쁜 일이 일어날 수 없음을…
추상 해석은 모든 가능한 프로그램 상태를 과대 근사합니다. 추상화 안에서 0으로 나누기에 도달할 수 없다면, 실제 코드에서도 도달할 수 없습니다. 다음은 그 작동 원리와 한계입니다.
정적 분석은 비행기가 추락하지 않음을 증명할 수 없습니다. 하지만 고도계 제어 루프가 0으로 나누기를 절대 하지 않고, 배열 범위를 벗어나는 인덱싱을 절대 하지 않으며, 고정 소수점 누산기에서 오버플로우가 절대 발생하지 않음은 증명할 수 있습니다. 이 둘의 차이가 중요한 이유는,…
추상 해석은 실행 전에 런타임 에러가 불가능함을 증명하게 해줍니다. 실제로 어떻게 작동하는지, 왜 어려운지, 그리고 도구 체인의 어디에 맞는지 알아봅니다.
테스트 스위트는 통과했다. 타입 체커는 초록불이다. 배포했다. 두 시간 후, 프로덕션에서 아묏도 테스트하지 않은 엣지 케이스에서 가 발생했다. 테스트는 버그를 찾는다. 타입은 일부를 방지한다. 둘 다 프로그램이 런타임 에러로부터 자유롭다는 것을 증명하지는 못한다. 그것을 위해서는 더…
CHERI의 하이브리드 ABI를 사용하면 기존 C 코드를 capability 하드웨어로 점진적으로 이식할 수 있다. 컴파일 방법, 어떤 문제가 발생하는지, 그리고 전체 codebase를 rewrite하지 않고 해결하는 방법을 알아본다。
Rust로 rewrite하기에는 너무 크고, 버퍼 오버플로우에 노출된 채로 두기에는 너무 중요한 C codebase가 있다고 하자. CHERI capability 하드웨어는 CPU 수준에서 메모리 안전성 위반을 잡아낼 수 있지만, 인터넷에서는 CHERI 포인터가 128비트이고 기존…
1970년대부터 하드웨어 수준에서 메모리 안전성은 가능했다. 캐퍼빌리티 아키텍처가 평면 메모리 모델에 계속 패배한 이유와 CHERI가 마침내 판도를 바꾸는 이유를 설명한다.
CVE의 70%는 메모리 안전성 버그다. buffer overflow, use-after-free, double free. 공격자가 변형된 JPEG에서 루트 접근권까지 확대할 수 있는 취약점이다. 1975년부터 하드웨어에서 이것들의 대부분을 막는 방법을 알고 있었다. 케임브리지 CAP…
단일 C 라이브러리를 격리하기 위해 컨테이너를 사용하는 것은 과도하다. WebAssembly로 컴파일하여 WASI 샌드박스 내에서 실행하면 메모리 안전성, 캐퍼빌리티 기반 파일시스템 접근, 크래시 격리를 Docker 없이도 할 수 있다.
C 라이브러리 내부의 단 하나의 널 포인터 역참조가 전체 애플리케이션을 중단시킬 수 있다. 해당 라이브러리가 사용자 입력을 파싱하거나, 이미지를 압축 해제하거나, 트워크 프로토콜을 처리한다면, 잘못된 하나의 패킷이 크래시를 일으킬 수 있다. 컨테이너는 이 문제를 해결하지만, 하나의…
ARM Memory Tagging Extension과 GWP-ASan을 통해 최신 모바일 기기에서 프로덕션 메모리 안전성 탐지가 가능해졌다. 이들의 작동 방식과 트레이드오프를 살펴본다.
당신의 스마트폰은 프로덕션 환경에서 memory corruption을 감지할 수 있다. CI에서 실행하는 전체 인스트루먼테이션으로도, 모든 할당에 대해서도 아니다. 하지만 당신의 주머니 속 하드웨어는 이미 수 년 전부터 필요한 프리미티브를 탑재해 출시되고 있으며, 점점 더 많은…
CHERI는 모든 포인터를 경계가 있는 capability로 변환하는 하드웨어 확장이다. CPU 수준에서 buffer overflow을 차단하는 원리, 비용, 그리고 실제 하드웨어에서 시험하는 방법을 설명한다.
buffer overflow은 스무 해 동안 CWE Top 25에 올라 있었다. 스택 카나리아, ASLR, DEP, 제어 흐름 무결성, 메모리 안전 언어 등이 있음에도 불구하고 중요한 코드에서 끊임없이 발생하고 있다. 이유는 단순하다. 이 모든 완화책은 소프트웨어에서 실행되며,…
클린룸 검증은 검증 조건을 생성하고 해소하는 것을 요구한다. 여기서 LLM이 주석과 VC 생성을 자동화하여 실제 어려운 증명에 집중할 수 있게 하는 방법을 소개한다.
클린룸 소프트웨어 공학은 코드를 컴파일하기 전에 그 정당성을 증명할 것을 요구한다. 그것은 고귀하게 들리지만, 열 개의 정수를 정렬하는 함수를 위해 루프 불변식을 세 시간 동안 작성하다 본다면 상황이 달라진다. 병목 지점은 증명 자체가 아니다. 상용구이다. 검증 조건을 생성하고,…
Cleanroom software engineering 은 defect rate 를 100배 낮추지만, 완전 도입에는 별도의 test team 과 formal proof 가 필요하다. 여기서는 overhead 없이 그 대부분의 benefit 을 얻을 수 있는 pragmatic subset 을 소개한다.
Cleanroom software engineering 은 1,000줄당 0.1개의 defect 를 달성한다. 업계 평균은 10에서 50이다. 문제는 완전한 Cleanroom 을 위해서는 팀을 author 와 verifier 로 분할하고, 모든 module 앞에 formal…