피드로 돌아가기
GeekNewsSecurity
원문 읽기
Lean이 프로그램의 정확성을 증명했지만, 그 안에서 버그가 발견됨
Lean 4 IO 핸들러 내 USize 오버플로우를 통한 메모리 손상 취약점 분석
AI 요약
Context
정밀한 프로그램 증명이 가능한 Lean 4 언어 환경의 IO 프리미티브 계층에서 발생한 결함. lean_io_prim_handle_read 함수가 입력값 nbytes에 대한 범위 검증 없이 메모리 할당을 수행하는 구조적 한계 존재.
Technical Solution
USize타입의 언더플로우를 이용한 최대값(0xFFFFFFFFFFFFFFFF) 유도- 비정상적으로 큰
nbytes값이lean_alloc_sarray로 전달되는 경로 식별 - 정수 오버플로우에 따른 잘못된 메모리 크기 계산 및 할당 로직 분석
- 입력값 상한선 검증 로직 추가를 통한 메모리 오버플로우 방지 PR 제출
실천 포인트
1. 외부 입력값 및 사이즈 변수에 대한 명시적 Boundary Check 수행 여부 확인
2. Unsigned Integer의 언더플로우가 메모리 할당 함수로 전달될 때의 영향도 평가
3. 정적 증명 도구를 사용하더라도 런타임 IO 라이브러리의 구현체 레벨 검증 병행