From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp
이 논문은 SpecMon 런타임 모니터를 사용하여 관찰된 WhatsApp Web 및 Signal Desktop의 실행이 새롭게 개발된 Tamarin 호환 모델을 준수하는지 검증함으로써, 실제 실행과 공식 프로토콜 명세 사이의 간극을 메우고, 이를 통해 보안 속성을 확인하며 애플리케이션 간의 문서화되지 않은 차이점을 밝혀낸다.
원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기
디지털 시대에 수십억 명의 사람들이 가장 사적인 생각을 공유하고, 금융 데이터를 보호하며, 일상을 조율하기 위해 메시징 앱에 의존하고 있습니다. 이러한 애플리케이션의 이면에는 메시지를 어떻게 잠그고, 보내고, 해제할지에 대한 청사진 역할을 하는 프로토콜이라는 복잡한 규칙 체계가 자리 잡고 있습니다. 이 청사진 중 가장 유명한 것이 바로 시그널(Signal) 프로토콜로, 이는 해커가 메시지를 가로채더라도 읽을 수 없도록 설계된 시스템입니다. 수년 동안 보안 전문가들은 강력한 컴퓨터 도구를 사용하여 이 청사진이 수학적으로 건전하다는 것을 증명해 왔습니다. 그들은 규칙이 완벽하게 준수된다면 이 시스템이 난공불락임을 보여주었습니다. 하지만 청사진은 건물 그 자체와는 다릅니다. 설계도가 종이 위에서 완벽해 보인다고 해서, 그것이 실제 건물을 짓는 건설팀이 모든 지침을 따랐거나, 적절한 자재를 사용했거나, 벽을 쌓는 과정에서 실수 없이 작업했다는 것을 의미하지는 않습니다. 소프트웨어의 세계에서는 이론적인 설계와 사용자의 휴대폰에서 실제로 실행되는 코드 사이의 간극 속에 종종 취약점이 숨어 있습니다.
CISPA 헬름홀츠 정보 보안 센터의 연구진은 이 간극을 메우기 위해 나섰습니다. 그들은 왓츠앱(WhatsApp)과 시그널 앱 내부에서 실행되는 실제 버전의 시그널 프로토콜이 설계된 엄격한 규칙을 실제로 잘 따르고 있는지 알고 싶었습니다. 연구진은 이 거대한 애플리케이션들의 전체 코드베이스를 읽으려고 시도하는 대신—이는 일부 부분이 숨겨져 있거나 폐쇄되어 있어 매우 어려운 작업입니다—특수한 감시자(watchdog)를 구축했습니다. '스펙몬(SpecMon)'이라 불리는 이 감시자는 애플리케이션이 실행되는 동안 이를 지켜보며, 네트워크와 나누는 모든 대화와 보안 키를 이용한 모든 계산 과정을 경청합니다. 이 감시자는 실시간으로 이러한 실제 동작들을 완벽한 이론적 모델과 비교합니다. 만약 애플리케이션이 지름길을 택하거나, 단계를 건너뛰거나, 청사진이 허용하는 것과 다른 방식을 사용하려고 하면 감시자는 경보를 울립니다.
연구진은 이 방법을 두 가지 주요 애플리케이션에 적용했습니다. 누구나 검사할 수 있도록 공개된 시그널 데스크톱(Signal Desktop)과 거대 기업이 소유한 폐쇄형 독점 시스템인 왓츠앱 웹(WhatsApp Web)입니다. 시그널 데스크톱 애플리케이션의 경우, 연구진은 기존의 매우 상세한 프로토콜 수학 모델을 바탕으로, 미래의 양자 컴퓨터에 저항하도록 설계된 새로운 유형의 암호화 방식 처리와 같은 실제 소프트웨어에서 발견되는 구체적이고 복잡한 세부 사항들을 추가했습니다. 반면 왓츠앱의 경우, 연구진은 역으로 작업해야 했습니다. 사전 모델 없이 시작하여, 애플리케이션의 동작을 관찰하고 기록함으로써 소프트웨어가 수행하는 동작과 정확히 일치하는 새로운 맞춤형 청사진을 직접 구축했습니다. 이는 왓츠앱의 프로토콜 구현으로부터 직접 형식 모델(formal model)을 도출해 낸 첫 사례라는 점에서 중요한 성과였습니다.
모델이 준비되자 연구진은 이를 테스트에 부쳤습니다. 메시지가 지연되거나, 순서가 바뀌어 전송되거나, 네트워크 연결이 끊기는 시나리오를 포함하여 수천 번의 시뮬레이션 대화를 실행했습니다. 모든 경우에 애플리케이션은 모델이 예측한 대로 정확하게 작동했으며, 이는 핵심 보안 메커즘이 올바르게 기능하고 있음을 확인시켜 주었습니다. 또한 연구진은 감시자가 오류를 잡아낼 수 있는지 확인하기 위해 의도적으로 소프트웨어에 오류를 주입했습니다. 그들은 앱이 오래된 암호화 키를 재사용하거나, 서명 확인을 건너뛰거나, 예상치 못한 방식으로 비밀 데이터를 유출하도록 만들었습니다. 시스템은 이러한 모든 보안 결함을 탐지해 냈으며, 이는 모니터링 도구가 위험한 규칙 이탈을 포착할 수 있을 만큼 민감하다는 것을 입증했습니다.
그러나 모니터링 과정에서 즉각적으로 드러나지 않는 두 애플리케이션 간의 미묘한 차이점도 발견되었습니다. 연구진은 왓츠앱이 '읽음 확인(메시지를 읽었다는 알림)'을 처리하는 방식이 시그널과 다르다는 것을 발견했습니다. 시그널에서 이러한 영수증(receipts)은 메시지와 동일한 강력한 암호화 체계 내에 포함되어 있으며, 보안 키의 지속적인 업데이트 과정에 참여합니다. 반면 왓츠앱에서 이러한 영수증은 암호화 계층 외부에서 전송되며, 이는 보안 업데이트를 트리거하지 않는다는 것을 의미합니다. 연구진은 이 차이점을 근거로 왓츠앱의 보안을 뚫을 수 있는 방법을 찾아내지는 못했지만, 이것이 만약 비밀 키가 도난당했을 경우 애플리케이션이 보안을 회복하는 데 더 오랜 시간이 걸릴 수 있음을 시사한다고 언급했습니다. 또한 연구진은 왓츠앱이 아직 발신자의 신원을 서버로부터 숨기는 것과 같은 일부 고급 개인정보 보호 기능을 포함하고 있지 않다는 점도 확인했습니다. 이는 시그널 앱에는 존재하는 기능입니다.
이 연구는 소스 코드의 모든 줄을 볼 필요 없이도, 실제 작동하는 복잡한 소프트웨어를 관찰하고 그것이 보안 약속을 준수하는지 검증하는 것이 가능하다는 것을 보여줍니다. 이 과정은 효율적이어서 설정 및 실행에 단 몇 주밖에 걸리지 않았으며, 애플리케이션의 속도에 거의 지장을 주지 않았습니다. 이론적 모델과 실시간 모니터링이 동일한 언어를 공유하도록 함으로써, 연구진은 개발자와 보안 전문가들이 애플리케이션이 진화함에 따라 보안성을 지속적으로 확인할 수 있는 방법을 제공했습니다. 이 접근 방식은 우리가 매일 사용하는 디지털 도구에 대한 신뢰를 구축하는 새로운 길을 제시하며, 우리가 사는 건물이 그 설계도만큼이나 안전할 수 있도록 보장합니다.
연구 분야의 논문에 파묻히고 계신가요?
연구 키워드에 맞는 최신 논문의 일일 다이제스트를 받아보세요 — 기술 요약 포함, 당신의 언어로.