당신이 거대하고 첨단 기술이 집약된 도서관의 관리자라고 상상해 보십시오. 수십 년 동안, 비밀을 지키는 규칙은 믿기지 않을 정도로 간단했습니다. 일단 어떤 책에 "비밀(Secret)"이라는 표시가 붙으면, 그 책은 영원히 "비밀" 상태로 남는 것이었습니다. 당신은 그 책을 선반에서 꺼낼 수도 없고, 일반 방문객에게 보여줄 수도 없습니다. 컴퓨터 세계에서는 "비간섭성(noninterference)"이라고 불리는 이 규칙은 무언가를 안전하게 지키는 데는 매우 훌륭하지만, 믿기지 않을 정도로 경직되어 있습니다. 현실 세계에서 비밀은 영원히 비밀로 남지 않습니다. 때로는 비밀이 공개되어야 할 때도 있고(예: 게임의 승자를 발표하는 것), 때로는 공적인 정보가 비밀이 되어야 할 때도 있습니다(예: 물건을 구매한 후 신용카드 정보를 삭제하는 것). 만약 당신의 도서관 규칙이 너무 엄격하다면, 규칙을 어기지 않고서는 이러한 필수적인 일들을 수행할 수 없습니다. 하지만 규칙을 너무 느슨하게 만들면, 실수로 비밀을 유출할 수도 있습니다. 이것이 바로 컴퓨터 과학자들이 해결하려고 노력해 온 까다로운 퍼즐입니다. 즉, 언제 비밀의 상태를 변경할 수 있는지 똑똑하게 판단하면서도, 나쁜 놈들이 몰래 침입하지 못하게 하는 보안 시스템을 어떻게 구축할 것인가 하는 문제입니다.

"동적 정보 방출 정책의 건전한 강제 실행(Sound Enforcement of Dynamic Release Information Flow Policy)"이라는 제목의 이 논문은 바로 그 퍼즐을 다룹니다. 저자인 제프리 칭(Jeffrey Ching)과 단펭 장(Danfeng Zhang)은 데이터의 보안 라벨을 실시간으로 변경할 수 있게 하되, 오직 안전할 때만 가능하도록 하는 새로운 규칙 세트와 "마법의 검사기(타입 시스템)"를 구축했습니다. 그들은 단순히 아이디어만 제시한 것이 아니라, 이를 구현하기 위해 Rust 프로그래밍 언어로 프로토타입을 만들었으며, 그것이 작동한다는 것을 수학적으로 증명했습니다. 그들은 자신들의 시스템이 입찰 게임(게임이 끝날 때까지 입찰가는 비밀이지만 그 후에는 공개되는 상황)이나 투표 시스템(사용 후 자격 증명이 삭제되어야 하는 상황)과 같은 복잡한 시나리오를 보안 유출 없이 처리할 수 있음을 보여주었습니다. 이는 마치 도서관 관리자에게 "비밀" 책을 방문자에게 전달해도 되는 정확한 시점을 알려주는 스마트 워치를 쥐여주어, 규칙이 변하더라도 도서관의 보안을 유지하는 것과 같습니다.

문제점: "정적(Static)" 보안 요원

해결책을 이해하기 위해, 먼저 기존의 방식부터 살펴보겠습니다. 오랫동안 컴퓨터 보안은 **비간섭성(noninterference)**이라는 개념에 의존해 왔습니다. 은행의 보안 요원이 "금고가 잠겨 있으면 내부의 어떤 것도 밖으로 나갈 수 없다"라는 엄격한 규칙을 가지고 있다고 상상해 보십시오. 금고가 항상 잠겨 있다면 이 규칙은 아주 잘 작동합니다. 하지만 은행 매니저가 "좋아요, 오후 5시에는 금고를 열어서 돈을 세겠습니다"라고 말한다면 어떻게 될까요? 기존의 규칙 아래에서 보안 요원은 "안 됩니다! 금고가 잠겨 있으니 열 수 없습니다!"라고 말할 것입니다. 보안 요원은 금고가 특정 시간에 열려야 한다는 사실을 이해하지 못합니다.

컴퓨터 용어로 말하자면, 전통적인 보안 시스템은 정보가 "비밀"이거나 "공개" 상태이며, 이 상태는 절대 변하지 않는다고 가정합니다. 하지만 현실 세계에서 데이터는 동적입니다. 경매의 입찰가는 경매가 끝날 때까지 비밀이지만, 경매가 끝나면 공개됩니다. 신용카드 번호는 거래를 위해 필요하지만, 거래가 완료되면 더 이상 사용할 수 없도록 "삭제"되어야 합니다. 기존의 "정적" 보안 요원들은 이러한 변화를 처리할 수 없습니다. 그들은 모든 것을 차단하거나(시스템을 쓸모없게 만듦), 혹은 혼란에 빠져 비밀을 유출하게 됩니다.

해결책: "동적 방출(Dynamic Release)" 정책

저자들은 **동적 방출(Dynamic Release)**이라고 불리는 새로운 사고방식을 제안합니다. 정적인 "비밀" 또는 "공개" 라벨 대신, 모든 데이터가 이벤트에 따라 변할 수 있는 "스마트 라벨"을 가지고 있다고 상상해 보십시오.

이것은 콘서트의 마법 티켓과 같습니다.

• 티켓: 이것은 당신의 데이터(입찰가나 비밀번호 같은 것)입니다.
• 이벤트: 이것은 "경매 종료"나 "거래 완료"와 같은 특정 시점입니다.
• 규칙: 티켓에는 이렇게 적혀 있습니다. "나는 이벤트가 발생할 때까지 VIP 티켓(비밀)이다. 일단 이벤트가 발생하면, 나는 일반 티켓(공개)으로 변한다."

이 논문은 이러한 규칙을 명시적으로 작성할 수 있는 언어를 소개합니다. 당신은 "이 데이터는 비밀이지만, auction_over(경매 종료) 이벤트가 발생하면 공개가 된다"라고 말할 수 있습니다. 또는 "이 데이터는 공개이지만, transaction_done(거래 완료) 이벤트가 발생하면 최고 비밀(즉, 파기되어야 함)이 된다"라고 말할 수도 있습니다.

"마법의 검사기" (타입 시스템)

스마트한 라벨을 갖는 것도 좋지만, 컴퓨터가 실제로 규칙을 따르도록 만드는 방법은 무엇일까요? 프로그래머에게 조심해달라고 부탁할 수는 없습니다. 그들은 실수할 수 있기 때문입니다. 저자들은 **타입 시스템(Type System)**을 구축했는데, 이는 마치 보안을 위한 초강력 맞춤법 검사기와 같습니다.

당신이 이야기를 쓰고 있는데, 맞춤법 검사기가 단순한 철자 오류뿐만 아니라 줄거리의 구멍(설정 오류)까지 체크한다고 상상해 보십시오.

• 만약 당신이 "영웅이 비밀의 문을 연다"라고 쓴다면, 맞춤법 검사기는 다음과 같이 확인합니다: "영웅이 열쇠를 가지고 있는가?"
• 만약 당신이 아직 영웅에게 열쇠를 주지 않았다면, 맞춤법 검사기는 비명을 지릅니다: "오류! 아직 문을 열 수 없습니다!"

이 논문에서 "맞법 검사기"는 프로그램이 시작되기 전(컴파일 타임)에 실행되는 타입 시스템입니다. 이것은 모든 코드 라인을 살펴보고 다음과 같이 질문합니다:

1. "이 데이터는 현재 비밀인가?"
2. "데이터를 공개로 바꿀 수 있게 하는 이벤트가 지금 실제로 일어나고 있는가?"
3. "만약 당신이 이 데이터를 대중에게 보여주려 한다면, 규칙이 허용하는가?"

만약 이 질문 중 하나라도 답이 "아니오"라면, 프로그램은 실행을 거부합니다. 이것은 클럽의 문지기가 당신의 신분증과 초대 명단을 확인하는 것과 같습니다. 만약 당신의 초대장에 "입장은 오후 10시 이후에만 가능"이라고 적혀 있는데 지금이 9시 59분이라면, 문지기는 당신이 아무리 항변해도 들여보내 주지 않을 것입니다.

"relabel" 명령어

그들이 발명한 가장 멋진 기능 중 하나는 **relabel**이라고 불리는 명령어입니다. 이것은 프로그래머가 사용할 수 있는 "마법 지팡이"와 같지만, 오직 조건이 충족되었을 때만 사용할 수 있습니다.

당신이 마법사라고 상상해 보십시오. 당신에게는 "독약"이라고 라벨이 붙은 포션이 있습니다. 당신은 이것을 "치유의 물"로 바꾸고 싶습니다. 그냥 지팡이를 휘둘러서 라벨을 바꿀 수는 없습니다. 그것은 위험하기 때문입니다. 당신에게는 "해가 뜨고 있다"와 같은 특정한 조건이 필요합니다.

• 명령어: relabel(potion, Poison to Healing using sun_rising)
• 체크: 마법 검사기가 하늘을 봅니다. 해가 뜨고 있습니까?
  • 예: 포션은 치유의 물로 변합니다. 라벨이 안전하게 변경되었습니다.
  • 아니오: 명령은 아무 일도 하지 않습니다. 포션은 독약 상태로 남습니다. 시스템은 특정 "이벤트"(예: 해가 뜨는 것)가 실제로 발생하지 않았다면 당신이 규칙을 바꾸는 것을 방지합니다.

이를 통해 프로그래머가 특정 "이벤트"(예: 해가 뜨는 것)가 실제로 발생하지 않았음에도 불구하고 규칙을 변경하려고 시도하더라도, 시스템은 이를 허용하지 않습니다.

작동 증명

저자들은 단순히 이것을 만들고 운에 맡긴 것이 아닙니다. 그들은 두 가지 매우 중요한 일을 수행했습니다.

1. 수학적 증명: 그들은 자신들의 시스템이 "건전(sound)"하다는 것을 보여주는 공식적인 증명(엄격한 수학적 논증)을 작성했습니다. 쉬운 말로, 만약 프로그램이 그들의 맞춤법 검사기를 통과한다면, 비밀이 유출되는 것은 불가능함을 수학적으로 증proved했다는 뜻입니다. 이것은 단순한 추측이 아니라 논리에 기반한 보장입니다. 기존의 방식들은 비밀이 변하지 않는다고 가정했기 때문에, 그들은 이 동적인 시스템을 위해 새로운 증명 방식을 만들어내야 했습니다.
2. 실제 환경 테스트: 그들은 인기 있는 안전하고 빠른 언어인 Rust로 프로토타입을 구축했습니다. 그리고 두 가지 실제 사례를 새로운 시스템으로 가져왔습니다:
   • 컨퍼런스 심사 시스템: 교수들이 논문을 심사하는 시스템과 같습니다. 심사 점수는 심사가 완료될 때까지 비밀입니다. 그들의 시스템은 점수가 조기에 유출되는 것을 성공적으로 막았습니다.
   • 보안 투표 시스템 (Civitas): 이 시스템은 투표와 자격 증명을 처리합니다. 투표자의 프라이버시를 보호하기 위해 사용 후 자격 증명을 삭제해야 합니다. 그들의 시스템은 이 "삭제" 정책을 성공적으로 강제했습니다.

결과

그들이 시스템을 테스트했을 때, 결과는 완벽했습니다. 기존 시스템이 놓쳤을 법한 모든 보안 실수를 잡아냈으며, 동시에 프로그램이 필요한 동적인 작업들(입찰가를 공개하거나 카드를 삭제하는 등)을 수행할 수 있도록 허용했습니다.

또한, 추가적인 보안 체크로 인해 프로그램이 얼마나 느려지는지도 측정했습니다. 결과는 놀라울 정도로 좋았습니다: 컨퍼런스 시스템의 경우 약 0.004 밀리초(0.029ms에서 0.033ms로)의 지연이 발생했습니다. 투표 시스템의 경우 약 0.042 밀리초(5.694ms에서 5.736ms로)가 추가되었습니다. 이는 인간이 전혀 느낄 수 없을 정도로 미미한 수준입니다. 이는 매우 강력하고 동적인 보안을 갖추면서도 컴퓨터를 느리게 만들지 않을 수 있음을 입증합니다.

이것이 왜 중요한가

이 논문은 이론과 실제 사이의 간극을 메웠다는 점에서 큰 진전을 이루었습니다. 오랫동안 연구자들은 변화하는 비밀을 다루는 훌륭한 아이디어들을 가지고 있었지만, 그것들은 실제 소프트웨어에 적용하기에는 너무 복잡했습니다. 이 논문은 이를 위한 통합적이고 단순하며 검증된 방법을 제공합니다.

이것은 잠긴 금고(너무 엄격함)와 열린 문(너무 느슨함) 사이에서 하나를 선택해야 했던 세상에서, 정확히 언제 잠그고 언제 열어야 할지 아는 스마트 도어가 있는 세상으로 이동하는 것과 같습니다. 저자들은 이 스마트 도어가 가능하다는 것뿐만 아니라, 빠르고 신뢰할 수 있다는 것까지 보여주었습니다. 그들은 단순히 "될 수도 있다"라고 말한 것이 아니라, 수학적으로 증명하고 실제 코드로 작동함을 보여주었습니다.

미래에는 우리가 매일 사용하는 앱들—뱅킹 앱, 투표 시스템, 소셜 미디어 등—이 훨씬 더 안전해질 수 있습니다. 이 앱들은 데이터가 민감할 때 자동으로 보호하고, 때가 되면 안전하게 공개할 수 있으며, 그 배후의 복잡한 규칙들을 우리가 걱정할 필요 없이 말입니다. "마법의 검사기"가 규칙 준수를 보장함으로써, 우리는 디지털 세상을 조금 더 신뢰할 수 있게 될 것입니다.