쌓인 기록에서 찾기
무엇을 찾으세요?
날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위부터 2026년 10월 30일 (금)까지3636건
2건 · "커널 버그"조건 지우기 ×
001▲ 109 · 댓글 2837년 전 OpenBSD 커널 버그로 루트 권한 확보OpenBSD의 공유 메모리 첨부 카운터가 부호 있는 16비트 short로 정의된 것을 악용한 취약점이 37년 전 원래 BSD 소스까지 거슬러 올라간다.보안 · Big Fish: Exploiting a 37-Year-Old Kernel Bug in OpenBSD
Key Point37년된 버그로 최신 보안 기법들을 우회해 루트 권한을 획득하는 경로를 공개했으며, 이는 장기간 방치된 레거시 코드의 위험성과 커널 할당자 결정성이 얼마나 심각한 공격 표면인지를 보여준다.
핵심 요약
- OpenBSD의 공유 메모리 첨부 카운터가 부호 있는 16비트 short로 정의된 것을 악용한 취약점이 37년 전 원래 BSD 소스까지 거슬러 올라간다.
- 프로세스를 반복해서 fork하여 카운터를 32,767을 넘도록 밀어서 음수로 wrap되게 하는 정수 오버플로우를 유발할 수 있다.
- 이를 통해 race condition으로 use-after-free 취약점을 트리거하고, 별도의 커널 out-of-bounds write와 조합하면 로컬 권한 상승이 가능하다.
전체 요약 12문장 읽기 →AI · 머신러닝 · What mathematicians should know about the Lean Theorem Prover: reliability & AI
Key PointAI가 수학 증명을 자동 형식화하기 시작하면서 신뢰성·일관성 검증의 새로운 시대가 열렸지만, 커널 버그와 AI 자체에 대한 신뢰 문제가 수학의 기초를 위협할 수 있다.
핵심 요약
- 형식 증명은 수학의 기초와 논리 규칙 수준에서 철저히 검증한 증명으로, 컴퓨터로 자동 검사하는 것이 일반적이며 페르마 최종 정리·구 채움 문제 등이 형식화됐다.
- 증명 보조기(proof assistant) 중 Lean이 수학자들에게 가장 인기 있으며, 2013년 Leo de Moura가 개발했고 마이크로소프트에서 오픈소스로 공개됐다.
- Lean의 표준 수학 라이브러리인 mathlib은 약 30만 개 정리, 10만 개 이상 정의, 250만 줄 코드로 700명 이상이 기여했다.
전체 요약 13문장 읽기 →