Google DeepMind, AI로 Signal 프로토콜 코드의 보안을 수학적으로 증명하다

멋지네요, AI 활용 사례로 정말 좋습니다. 구글은 유용한 기여와 AI 시스템 통제 측면에서 빅플레이어 중 가장 깔끔한 것 같아요. 다만 이 새로운 증명 에이전트는 명세에 도전하는 게 아니라 구현만 검증하는 것 같네요, 제가 이해한 게 맞다면요.

이 에이전트가 고전적인 코딩 에이전트와 어떻게 다른지 궁금합니다. 결국 코드베이스를 반복하면서 Lean이나 Rocq 코드를 작성하고 실행하는 방식은 비슷해 보이니까요.

머지않아, 아마 2~3년 안에, 우리 시스템에서 검증되지 않은 소프트웨어를 _단 하나라도_ 돌렸다는 사실이 미친 짓처럼 보일 것 같습니다. 지금 우리가 Telnet이나 평문 HTTP를 썼다는 게 미친 짓처럼 보이는 것처럼요.

올해 초에 오래된 프로젝트를 대대적으로 리팩터링하고 있었습니다. 그때 코딩 에이전트가 막 떠오르면서 점점 더 자율적인 작업을 맡겨도 될 만큼 신뢰할 수 있게 되어서 기대하며 시도해 봤죠.

에이전트는 몇 시간 동안 돌면서 리팩터링을 해냈고, 심지어 방대한 테스트 스위트까지 알아서 만들어 줬습니다. 모든 테스트 통과!

아주 감동했는데, 잠깐 눈을 가늘게 뜨고 보니... 전체를 거꾸로 구현해 놓은 거였습니다. 무의미할 뿐만 아니라(제시한 목표를 하나도 달성하지 못함) 실제로 이전보다 상황을 더 나쁘게 만들었더군요!

그 순간까지 저는 AI 시대의 형식 검증 가능성에 꽤 낙관적이었습니다. 하지만 그 엉망진창을 보고 나서 깨달았죠. 어쩌면 그 녀석이 작성한 코드에 대한 수학적 증명을 써 줬을 수도 있고, 그 증명이 통과됐을 수도 있으며, 그래도 코드는 여전히 틀렸을 거라는 걸요!

아주 멋지네요. 몇 년 전에 AlphaZero 접근법 같은 걸로 형식 검증 전용 모델을 개발할까 하는 생각을 하고 있었습니다. 지난 몇 달간의 소식을 보니 안 하길 잘했네요. 범용 LLM이 정말 모든 걸 삼키고 있는 것 같습니다.

명세가 (Arm 시맨틱 포함) 2만 6천 줄이나 된다는 게 흥미롭네요. 꽤 큰 신뢰 컴퓨팅 기반(TCB)입니다. 상징적/계산적 모델을 처음부터 개발해야 했겠죠. mathlib처럼 재사용 가능한 라이브러리를 만들 수 있을지, 그리고 그쪽 인센티브는 어떻게 돌아갈지 궁금합니다. AI 연구소들은 아마 별로 관심이 없을 테고, 연구자들에게도 감사받기 어려운 작업일 가능성이 큽니다. 하지만 검증을 하거나 검증된 제품을 파는 회사들이 생겨난다면, 작업을 공유하고 표준화된 TCB를 가질 인센티브가 생길지도 모르죠. 그렇게 되면 좋든 싫든 "대화형 정리 증명기 전쟁"에도 실질적인 종지부가 찍힐 수 있습니다.

개발 중인 코드에 어떻게 작용할지도 흥미롭네요. ChatGPT는 이게 공개된 다음 날 libsignal이 크게 바뀌었다고 하던데요 :D 아마 Rust로 된 중간 수준의 비신뢰 모델이 도움이 될 수도 있겠죠(대부분의 증명이 Rust 모델과 명세를 연결하고, 그다음 더 기계적인 증명이 Rust 모델과 바이너리를 연결하는 식). seL4가 오래전에 이렇게 했습니다. 하지만 실용적인지는 전혀 모르겠네요, 들어본 적이 없어서 […]

저는 AI가 Lean 코드를 작성하는 게 얼마나 쉬운지를 활용하는 실험을 해 왔는데(https://metamagic.substack.com/p/beyond-the-proof-dump-lean-...), 몇 가지 교훈이 있습니다.

1. AI Lean은 완벽하지 않고, AI가 Lean을 작성한다는 점에서 쉽게 속일 수 있습니다. AI Lean 코드를 가지고 놀아본 사람이라면 최소한 AI가 생성한 Lean을 검토하는 또 다른 적대적 프롬프트가 필요합니다.

2. 논문을 뒤져보니 버그를 일부러 다시 넣어서 잡아내는지 확인했지만, 발견된 버그는 없는 것 같습니다. Signal은 많은 사람이 검토해서 그냥 놀라운 걸 수도 있지만, 우리 대다수에게 진짜 이야기는 AI로 Lean 변환을 시작하면 그 가치가 발견되는 가정에 있다는 겁니다. 제가 정말 논리적으로 빈틈없다고 생각했던 것에서도 Lean이 고쳐야 할 사소한 것 몇 개를 찾아냈습니다. 퍼징처럼, 코드베이스에 퍼징을 도입했을 때 버그를 못 찾은 적이 없었던 것처럼, 명세를 Lean으로 변환할 때도 비슷할 거라고 기대합니다.

3. AI를 통해 (저렴하게) Lean을 생성할 수 있는 능력은 코딩에 있어 매우 흥미로운 잠금 해제입니다. 잠재적으로 명세에서 Lean으로, 다시 코드로 갈 수 있고, Lean을 논리적 문지기로 사용하는 것은 연구에만 국한되지 않고 일상적으로 더 많이 쓰일 수 있는 진짜 역량이 될 가능성이 있습니다.

초보 질문입니다. 이런 암호 시스템 말고 일반적인 소프트웨어 조각들에 대해서도 이런 증명을 만드는 게 유용할까요? 구체적으로:

1. 프로덕션에서 AI 에이전트가 중요한 경로에 있는 시스템, 즉 비결정적 행동이 발생할 수 있는(복구는 되더라도) 시스템에 적용한 사례가 있나요?

2. 처음부터 Lean 증명을 갖는 게 합리적인 시나리오는 무엇인가요? 예를 들어 ACID에 대한 보장이 필요한 데이터베이스 시스템을 만든다면 처음부터 이걸 갖는 게 더 나을 수 있겠죠. 하지만 API 기반 서비스를 만드는 데는 별로 유용하지 않을 것 같습니다.

멋지네요. 작년에 사람들이 AI에 더 많이 일을 넘기면서 소프트웨어가 훨씬 더 버그투성이가 될 거라고 생각했던 게 기억나는데, 이런 도구들은 어쩌면 소프트웨어의 미래가 훨씬 더 안전해 보일 수도 있다는 희망을 줍니다.