1979년 SRI가 그린 '증명 가능하게 안전한 운영체제' - 47년 전 논문이 오늘날 보안에 던지는 질문

47년 된 논문이 왜 지금 다시 회자될까

1979년, 미국 SRI International의 피터 노이만(Peter Neumann)과 동료들이 PSOS(Provably Secure Operating System, 증명 가능하게 안전한 운영체제)라는 이름의 논문을 발표했어요. 인터넷도 제대로 없던 시절, 유닉스가 막 자리 잡아가던 무렵에 그들은 이미 "운영체제의 보안성을 수학적으로 증명할 수 있어야 한다"는 야심찬 비전을 제시했죠. 그리고 거의 반세기가 지난 지금, 이 논문이 다시 사람들의 입에 오르내려요.

왜냐고요? 우리가 매일 쓰는 리눅스, 윈도우, macOS는 본질적으로 "버그가 발견되면 패치한다"는 사후 대응 모델이에요. CVE가 매년 수만 개씩 쏟아지고, 제로데이 공격이 끊이지 않잖아요. 반면 PSOS의 접근은 "애초에 시스템 설계 자체가 수학적으로 안전함이 증명되어야 한다"는 거였어요. 이게 다시 주목받는 이유는, AI 시대에 신뢰할 수 있는 컴퓨팅 기반이 그 어느 때보다 절실해졌기 때문이에요.

PSOS의 핵심 아이디어

논문이 제안한 건 계층적 능력 기반(capability-based) 아키텍처예요. 좀 어려운 말이죠? 풀어 설명할게요. 보통의 OS는 "이 사용자는 이 파일에 접근할 권한이 있는가"를 매번 체크하는 방식이에요. 그런데 능력 기반 시스템은 "이 프로그램이 들고 있는 토큰(capability)이 이 자원에 대한 접근권을 명시하는가"를 봐요. 마치 영화관 입장권 같은 거죠. 표를 들고 있으면 들어갈 수 있고, 없으면 못 들어가요. 단순해 보이지만 권한 위임과 격리를 훨씬 우아하게 처리할 수 있어요.

PSOS는 이걸 17개 계층으로 나눠 설계했어요. 가장 아래 계층은 하드웨어에 가까운 능력 관리, 그 위로 메모리 객체, 프로세스, 파일 시스템, 사용자 인증 등이 쌓여 올라가는 구조예요. 각 계층은 자신보다 아래 계층의 인터페이스만 사용하고, 위로 올라갈수록 추상화 수준이 높아져요. 핵심은 각 계층의 동작이 형식적 명세(formal specification)로 기술되어, 수학적 증명이 가능하다는 점이에요.

이걸 형식 검증(formal verification)이라고 부르는데, 코드의 동작을 수학적 논리로 표현하고 정리(theorem)를 증명하듯 안전성을 보이는 방법이에요. 테스트는 '있는 버그를 찾는' 활동이지만, 형식 검증은 '특정 종류의 버그가 없음을 보이는' 활동이라 본질적으로 강력해요.

이 비전은 실현됐을까

솔직히 PSOS 자체는 완전히 구현되진 못했어요. 1970년대 기술로는 너무 야심찬 목표였거든요. 하지만 그 후예는 활발해요. 가장 유명한 게 호주 NICTA에서 시작된 seL4 마이크로커널이에요. seL4는 약 1만 줄의 C 코드로 구성된 마이크로커널인데, 그 동작 전체가 수학적으로 증명되어 있어요. 즉, "이 커널은 명세대로만 동작하고, 명세에 없는 짓은 절대 하지 않는다"는 게 증명된 거죠. 항공우주, 군용, 자율주행 차량 같은 고신뢰 영역에서 실제로 쓰여요.

또 다른 후예로는 캠브리지 대학과 SRI가 협력한 CHERI 아키텍처가 있어요. ARM과 협력해 Morello라는 시제품 CPU도 만들었는데, 능력 기반 보안을 하드웨어 수준에서 구현해서 메모리 안전성 문제(use-after-free, buffer overflow 같은 거)를 근본적으로 막으려는 시도예요. 영국 정부와 마이크로소프트도 이 프로젝트에 투자하고 있어요.

Rust 언어의 인기도 같은 흐름의 일부예요. 형식 검증까진 아니지만, 컴파일 타임에 메모리 안전성을 강제하는 접근은 PSOS가 꿈꿨던 "버그가 발생할 가능성 자체를 설계로 차단한다"는 철학과 닿아 있어요.

한국 개발자에게 주는 시사점

당장 우리 업무에 PSOS를 쓰진 않아요. 그래도 이 논문이 던지는 질문은 지금도 유효해요. "내가 만드는 시스템의 보안 가정은 무엇이고, 그 가정이 깨지는 시나리오는 무엇인가?"를 명확히 글로 적어보는 것만으로도 보안 수준이 크게 올라가거든요.

그리고 자율주행, 의료기기, 금융 코어시스템 같은 고신뢰 분야에 관심 있다면 seL4나 CHERI, 그리고 Coq나 Isabelle 같은 정리 증명기를 한 번쯤 들여다보면 좋아요. 한국에서도 자동차 SW나 국방 분야에서 형식 검증 인력 수요가 점점 늘고 있고, 학계와 산업계의 간극이 큰 만큼 진입하면 차별화될 수 있는 영역이에요.