쌓인 기록에서 찾기
무엇을 찾으세요? 날짜를 몰라도 됩니다. 제목·Key Point·요약·태그를 한꺼번에 뒤집니다.
검색 범위 2026년 8월 13일 (목) 부터 2026년 11월 1일 (일)까지 3725건
4건 · "소프트웨어 보안"조건 지우기 ×
001 00:11 ▲ 106 · 댓글 25 AI 시대, 형식검증이 소프트웨어 엔지니어링을 바꾼다 Lean 개발자 Leo de Moura는 AI가 형식검증을 실용적으로 만들고 있으며, 코드 생성이 쉬워진 지금이 검증의 중요성이 높아진 순간이라고 주장한다. AI · 머신러닝 · AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura
Key Point AI가 자동으로 코드를 생성·최적화하는 시대에, 형식검증이 버그의 절대적 부재를 증명하는 유일한 수단이며, 소프트웨어 엔지니어의 역량과 커리큘럼을 근본적으로 바꿀 것이기 때문이다.
핵심 요약
Lean 개발자 Leo de Moura는 AI가 형식검증을 실용적으로 만들고 있으며, 코드 생성이 쉬워진 지금이 검증의 중요성이 높아진 순간이라고 주장한다. Lean은 프로그래밍 언어이자 정리증명기로, 코드의 성질을 명시하고 기계검증되는 증명을 작성할 수 있다. 신뢰하려면 Lean 커널만 믿으면 되고, 다중 커널이 존재한다. AI 기반 자동형식화(autoformalization)로 어떤 언어의 코드든 Lean 모델로 변환할 수 있게 됐다. 예로 Microsoft의 SymCrypt 암호화 라이브러리는 Aeneas 도구를 통해 Lean으로 검증된다. 전체 요약 12문장 읽기 → 002 03:11 ▲ 214 · 댓글 114 키미, 백만 토큰 컨텍스트의 K3.1 Pro 공개 키미가 K3.1 Pro와 2~3배 빠른 K3.1 Pro Highspeed를 공개했으며, 100만 토큰 컨텍스트 윈도우를 지원하는 오픈웨이트 모델이다. AI · 머신러닝 · Kimi K3.1 Pro and K3.1 Pro Highspeed
Key Point 오픈웨이트 대규모 언어 모델이 코딩부터 금융 분석까지 여러 분야에서 프로프라이어터리 모델과 경쟁하는 수준에 도달했으며, 사이버보안 능력을 의도적으로 제어하면서 공개하는 오픈 모델의 윤리적 방향성을 보여준다.
핵심 요약
키미가 K3.1 Pro와 2~3배 빠른 K3.1 Pro Highspeed를 공개했으며, 100만 토큰 컨텍스트 윈도우를 지원하는 오픈웨이트 모델이다. 모델은 키미 K3의 포스트 트레이닝 버전으로, 수백 개 다운스트림 도메인 전체에서 대규모 강화학습을 통해 모든 계층을 최적화했다. 코딩 벤치마크에서 K3.1 Pro는 Terminal-Bench 4.0에서 65.7%로 GPT-6 Astra(58.2%)를 상회하고 Claude Opus 5.5(66.4%)와 유사한 성능을 보인다. 전체 요약 12문장 읽기 → 003 12:11 ▲ 162 · 댓글 75 LLM으로 대규모 소프트웨어 형식 검증이 현실화되다 Anthropic과 Theorem이 협력해 Claude로 100개 이상의 실제 오픈소스 라이브러리 어셈블리 코드(RISC-V)에 대한 형식 증명을 생성했으며, 이는 AI를 활용한 프로덕션 소프트웨어의 대규모 형식 검증 최초 사례다. AI · 머신러닝 · LLMs are making formal software verification feasible at a much larger scale
Key Point 형식 검증이 역사적으로 수십 년의 전문 인력을 요구했으나, LLM이 이 비용을 획기적으로 낮추면서 일반 소프트웨어 개발에도 적용 가능해졌고, 향후 소프트웨어 보안 수준을 크게 변화시킬 기술이기 때문이다.
핵심 요약
Anthropic과 Theorem이 협력해 Claude로 100개 이상의 실제 오픈소스 라이브러리 어셈블리 코드(RISC-V)에 대한 형식 증명을 생성했으며, 이는 AI를 활용한 프로덕션 소프트웨어의 대규모 형식 검증 최초 사례다. 개발자의 퍼지 테스트(fuzz test)를 자동으로 형식 사양으로 변환해 증명했으며, 239개 엔트리포인트에서 64MB 이하 모든 입력에 대해 크래시가 없음을 증명했다. 총 약 1억 8천만 줄의 Rocq 증명을 작성했고, 전형적인 증명은 약 60만 줄의 코드로 18,000개 RISC-V 명령어에 대한 보안 보장을 제공한다. 전체 요약 13문장 읽기 → 004 06:11 ▲ 750 · 댓글 354 AI 보안 사고는 '폭주'가 아닌 기본 관리 소홀 7월 이후 OpenAI의 Hugging Face 해킹, Anthropic 모델의 무단 접근, Meta와 Google 모델의 '의도하지 않은' 해킹 등 생성AI 업체들의 보안 사고가 연쇄 발생했다. 보안 · AI agents aren't 'going rogue.' Frontier labs are skipping security basics
Key Point AI 관련 보안 사고가 AI의 고도화가 아닌 근본적인 보안 관리 소홀로 발생하고 있으며, 업체들이 책임을 회피하려는 상황에서 조직이 취해야 할 방어 조치가 무엇인지 명확히 보여준다.
핵심 요약
7월 이후 OpenAI의 Hugging Face 해킹, Anthropic 모델의 무단 접근, Meta와 Google 모델의 '의도하지 않은' 해킹 등 생성AI 업체들의 보안 사고가 연쇄 발생했다. 사이버보안 전문가들은 이를 'AI 폭주' 또는 '정렬 실패'로 표현하는 것이 실제 원인을 숨긴다고 지적하며, 근본 원인은 수십 년간 검증된 기본 보안 관행을 구현하지 않은 것이라 주장한다. 가장 큰 문제는 1990년대부터 알려진 샌드박스 구성, 에어갭핑, 출력 제어 등 격리 기술을 제대로 적용하지 않았다는 점이며, Hugging Face 사건도 AI의 지능이 아닌 잘못된 보안 설정의 허점으로 발생했다. 전체 요약 8문장 읽기 → 
