2026년 8월 5일 Meta는 프로그램을 실행하지 않는 정적 분석기로 프로덕션 코드에서 10만 개의 버그를 찾아냈다 Meta의 Infer는 abstract interpretation과 양방향 추론을 사용해 코드 구조를 분석하여 null reference, memory leak, race condition을 발견한다. 실행은 필요 없다. 작동 방식과 자체 코드베이스에서의 활용법을 설명한다. abstract-interpretationstatic-analysismetainfer
2026년 8월 4일 정적 분석은 비행기가 추락하지 않음을 증명할 수 없습니다. 대신 더 유용한 것을 증명할 수 있습니다. 추상 해석은 모든 가능한 프로그램 상태를 과대 근사합니다. 추상화 안에서 0으로 나누기에 도달할 수 없다면, 실제 코드에서도 도달할 수 없습니다. 다음은 그 작동 원리와 한계입니다. abstract-interpretationstatic-analysissafety-criticalaviation
2026년 8월 3일 런타임 에러가 없음을 증명하는 방법(그리고 왜 아마도 포기하게 될 것인지) 추상 해석은 실행 전에 런타임 에러가 불가능함을 증명하게 해줍니다. 실제로 어떻게 작동하는지, 왜 어려운지, 그리고 도구 체인의 어디에 맞는지 알아봅니다. abstract-interpretationstatic-analysisruntime-errorsverification
2026년 8월 2일 C 코드를 전면 rewrite 없이 capability 하드웨어에서 실행할 수 있다 CHERI의 하이브리드 ABI를 사용하면 기존 C 코드를 capability 하드웨어로 점진적으로 이식할 수 있다. 컴파일 방법, 어떤 문제가 발생하는지, 그리고 전체 codebase를 rewrite하지 않고 해결하는 방법을 알아본다。 hardware-assisted-safetychericporting
2026년 8월 1일 캐퍼빌리티 하드웨어는 실패하지 않았다. 40년 일찍 도착했을 뿐이다. 1970년대부터 하드웨어 수준에서 메모리 안전성은 가능했다. 캐퍼빌리티 아키텍처가 평면 메모리 모델에 계속 패배한 이유와 CHERI가 마침내 판도를 바꾸는 이유를 설명한다. hardware-assisted-safetycapability-hardwarecherisoftware-history
2026년 7월 31일 C 의존성 라이브러리가 전체 프로세스를 중단시킬 수 있다. WebAssembly가 이를 막는다. 단일 C 라이브러리를 격리하기 위해 컨테이너를 사용하는 것은 과도하다. WebAssembly로 컴파일하여 WASI 샌드박스 내에서 실행하면 메모리 안전성, 캐퍼빌리티 기반 파일시스템 접근, 크래시 격리를 Docker 없이도 할 수 있다. hardware-assisted-safetysandboxingcwebassembly
2026년 7월 30일 당신의 스마트폰은 이미 memory corruption을 감지하는 하드웨어를 탑재하고 있다 ARM Memory Tagging Extension과 GWP-ASan을 통해 최신 모바일 기기에서 프로덕션 메모리 안전성 탐지가 가능해졌다. 이들의 작동 방식과 트레이드오프를 살펴본다. hardware-assisted-safetymemory-corruptionmobileasan
2026년 7월 29일 buffer overflow이 계속 발생하는 이유는 우리가 소프트웨어로 해결하기 때문이다 CHERI는 모든 포인터를 경계가 있는 capability로 변환하는 하드웨어 확장이다. CPU 수준에서 buffer overflow을 차단하는 원리, 비용, 그리고 실제 하드웨어에서 시험하는 방법을 설명한다. hardware-assisted-safetybuffer-overflowmemory-safetycheri
2026년 7월 28일 LLM이 코드의 정당성을 증명할 수는 없지만, 그것을 위한 상용구는 작성할 수 있다 클린룸 검증은 검증 조건을 생성하고 해소하는 것을 요구한다. 여기서 LLM이 주석과 VC 생성을 자동화하여 실제 어려운 증명에 집중할 수 있게 하는 방법을 소개한다. cleanroom-correctnessllmformal-proofsautomation
2026년 7월 27일 Cleanroom 은 1KLOC 당 0.1 defect 를 달성한다. 전체 도입 없이도 그 지점에 도달할 수 있다. Cleanroom software engineering 은 defect rate 를 100배 낮추지만, 완전 도입에는 별도의 test team 과 formal proof 가 필요하다. 여기서는 overhead 없이 그 대부분의 benefit 을 얻을 수 있는 pragmatic subset 을 소개한다. cleanroom-correctnessprocessefficiencypragmatism
