AI를 정말 유용하게 활용한 사례로 보임. 대형 업체 중 Google이 유용한 기여나 AI 시스템 통제 면에서 가장 깔끔하게 해왔다고 느낌. 다만 내가 제대로 이해했다면 이번 증명 에이전트는 명세 자체가 아니라 구현만 검증하는 듯함.
결국 코드베이스를 돌아다니며 Lean이나 Rocq 코드를 작성하고 실행하는 과정을 반복한다면, 일반적인 코딩 에이전트와 어떻게 다른지 궁금함.
Lean으로 만든 프로세서 모델에서 실행되는 컴파일된 Rust 코드의 동작이 실제 프로세서의 동작과 같다는 것은 어떻게 보장하나? 문서 명세를 바탕으로 작성한 Lean 명세가 Signal을 구현한 Rust 코드와 일치하는지는 어떻게 알 수 있나?
Google이 벤치마크 점수 극대화에 매달린 탓에 Gemini 모델은 위험할 정도로 의도와 어긋나게 행동하고 거짓말도 심하게 함. AI Overview나 학교에서의 검색 관련 행보도 상당히 나쁨.
Gemini와 검색 외에는 AlphaFold 같은 단백질 연구로 유용한 영역을 개척하고 있음. 하지만 Gemini에서는 책임감 있고 악행을 하지 않는 기술 기업이라는 평판을 이용하면서 OpenAI나 Anthropic보다 훨씬 나쁘게 행동하고 있다고 봄.
대부분의 AI 기업이 내놓는 과장 홍보와는 달라 보임. Google은 AI를 도구로 활용하고 있으며, 핵심적인 1%를 사람이 검토하도록 한 접근이 매우 영리함.
초보적인 질문인데, 암호 시스템 외의 일반 소프트웨어에도 이런 증명을 만드는 것이 유용할까?
실제 운영 환경의 핵심 실행 경로에 AI 에이전트가 들어가, 복구할 수는 있더라도 비결정적인 행동이 발생할 수 있는 시스템에 적용한 적이 있나?
또 어떤 경우에 처음부터 Lean 증명을 갖추는 것이 합리적일까? ACID 보장이 필요한 데이터베이스라면 처음부터 도입하는 편이 좋겠지만, API 기반 서비스에는 그다지 유용하지 않을 것 같음.
소프트웨어 검증은 대개 가능한 모든 입력에 대해 증명함. 어떤 행동 순서가 주어져도 시스템이 불변 조건을 유지하는지 확인하는 식임. 입력은 사용자 조작이나 라이브러리 API 호출일 수 있으며, AI 에이전트의 선택도 같은 방식으로 모델링할 수 있음.
AI가 선택할 수 있는 모든 행동 순서에 대해 원하는 불변 조건이 유지됨을 증명하면 됨. 에이전트가 도메인에 특화된 단순한 행동 집합에서만 고르도록 제한된다면 비교적 수월할 수 있지만, 제약 없는 Bash 셸을 제공하면 보장할 수 있는 것이 별로 없음.
사후에 임의의 코드 덩어리를 분석하기보다는 검증을 염두에 두고 작성하고 구조화한 소프트웨어를 검증하는 편이 훨씬 쉬움. 증명을 원한다면 처음부터 설계에 반영해야 함.
적어도 중요한 영역의 API 서비스라면 이런 보장을 원함. 물론 누구나 자기 사업이나 API가 중요하다고 생각할 수는 있음.
예를 들어 Stripe API는 돈이 걸려 있으니 모든 상황에서 문서대로 정확하게 동작한다는 보장이 있으면 좋지 않겠나? 다만 Stripe API를 Lean으로 작성하는 것은 별개의 과제임.
AI를 활용한 소프트웨어 검증은 강력하게 느껴짐. 위험성이 높은 함수에 간단한 정형 증명을 만들어 버그를 찾는 방법을 구축했는데, 경쟁 상태나 발견하기 어려운 다른 버그들을 꾸준히 찾아냄. https://verity.md/benchmark#calcom
앞으로 2~3년 안에, 검증하지 않은 소프트웨어를 시스템에서 실행했다는 사실 자체가 황당하게 느껴질 것으로 예상함. 지금 Telnet이나 평문 HTTP를 사용하던 시절을 바라보는 것과 비슷해질 듯함.
아직 검증할 수 있는 범위는 매우 좁음. 프로그램이 비정상 종료하지 않는다는 보장에는 잘 작동하지만, 암호화가 안전하다거나 압축한 데이터를 항상 원본대로 복원한다는 보장은 매우 어려움.
SQL 데이터베이스와 통신하는 GUI 프로그램이 기대대로 동작한다는 수준의 검증은 사실상 불가능하며, 아직 근처에도 도달하지 못함. 진전을 이루려면 더 발전한 LLM을 투입하는 것 이상의 변화가 필요함.
지난해에는 AI에 더 많은 일을 맡기면서 소프트웨어 버그도 크게 늘어날 것이라고 생각했는데, 이런 도구를 보니 오히려 소프트웨어가 더 안전해질 미래를 기대하게 됨.
우리 회사에서는 코딩을 전면적으로 에이전트 기반으로 전환한 뒤 사고와 서비스 중단이 크게 줄어듦.
개발 속도가 제품팀의 속도를 상당히 앞서게 되면서, 남는 개발 역량을 테스트·검증·자동 코드 검토 개선에 투입할 수 있었고 그 결과 놓치는 결함이 거의 없어짐.
시작할 때는 팀에서도 버그 증가와 품질 저하를 걱정했는데, 6개월 후 결과는 예상과 반대로 보임.
거대한 증명을 망가뜨리지 않았는지 AI가 확인하느라 CI 실행 한 번에 1만 달러가 들게 되면 참 좋아지겠음.
이번에는 검증을 위해 소프트웨어를 정형 수학 모델로 옮겼는데, 왜 반대 방향으로 개발을 시작하지 않는지 궁금함. 원하는 속성을 갖춘 정형 모델부터 만든 뒤 소프트웨어로 변환하면 안 되나?
사람이 작성한 Signal 프로토콜 명세만이 아니라 libsignal Rust 라이브러리 전체를 검증했다는 뜻으로 이해해도 되나?
libsignal 저장소에는 attest가 SGX 엔클레이브와 서버 측 HSM의 원격 증명 기능을 제공한다고 적혀 있음. https://github.com/signalapp/libsignal.
Intel의 SGX나 AMD의 하드웨어 보안 기능은 얼마나 신뢰할 수 있나? Cloudflare는 여러 ISP의 데이터센터와 신뢰하기 어려운 관할 지역에서도 엣지 네트워크를 운영하면서 AMD의 TSME만으로 충분히 안전하다고 보장함.
SGX는 확실히 완전히 뚫린 상태임. Signal 계정에는 제대로 된 비밀번호를 사용해야 함.
임대한 코로케이션 랙 위에 웹캠을 설치해 두면, 연방 수사기관이 SGX나 유사 기술을 뚫으려고 서버를 가져가러 올 때 알아챌 수는 있음.
보안 버그를 구현에 다시 삽입해 검증 절차가 실제로 문제를 잡아내는지 확인한 점이 좋음. 요즘 AI의 성과를 내세우는 글은 제대로 해냈는지보다 AI가 무언가를 했다는 사실에만 집중하는 경우가 너무 많음. 이런 작업으로 더 신뢰할 수 있는 라이브러리와 의존성을 얻게 되길 바람.
Google 팀은 Signal의 암호화 핵심부가 안전하다고 미리 전제한 뒤, 그 선입견을 확인하는 결과를 발표한 것처럼 들림.
이번 증명은 미리 정한 특정 속성이 성립함을 보여줄 뿐, 취약점이 존재하지 않음을 보여주지는 않음. 연구진이 예상하지 못한 공격까지 배제할 수 있는 접근은 아님.
예를 들어 서버 소프트웨어는 시뮬레이션만 했으며, 키 생성 부분도 평가하지 않은 것으로 보임. 키나 초기화 벡터(IV)가 부실하게 생성되면 겉보기에는 안전한 종단간 암호화 시스템도 무너질 수 있음.