VUPER: Verified ASN.1 UPER Parser
이 논문은 5G 및 V2X 프로토콜에 대한 동적 테스트를 통해 인기 있는 오픈 소스 및 상용 파서에서 20가지 유형의 불일치와 구체적인 보안 취약점을 발견하는 데 사용된, 형식적으로 검증되고 비트 정밀한(bit-precise) ASN.1 UPER 파서 및 직렬화기를 생성하는 프레임워크인 VUPER를 제시한다.
원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기
인터넷과 우리의 휴대전화를 매초 수십억 개의 메시지가 건물 사이를 질주하는 거대하고 북적이는 도시라고 상상해 보세요. 이 도시가 계속 돌아가기 위해서는 뉴욕의 전화기가 도쿄의 타워와 대화할 때 혼란을 겪지 않도록 하는 보편적인 언어가 필요합니다. 이 언어를 ASN.1이라고 부르며, 이는 컴퓨터가 정보를 작고 효율적인 디지털 상자에 정확히 어떻게 담을지 알려주는 문법이자 어휘와 같습니다. 하지만 까다로운 점은, 공간을 절약하고 속도를 높이기 위해 이 상자들이 표준 컴퓨터 단어(바이트)처럼 깔끔한 행에 맞춰 정렬되지 않고, 데이터의 가장 작은 단위인 비트(bit) 단위까지 아주 촘촘하게 채워진다는 것입니다. 이 특유의 초정밀 패킹 방식이 바로 UPER입니다.
문제는 이 미세한 비트 단위의 상자를 풀어내는 번역기(또는 "파서(parser)")를 작성하는 것이 매우 어렵다는 점입니다. 만약 번역기가 단 하나의 비트라도 잘못 읽거나, 새로운 미지의 정보를 처리하는 규칙을 하나라도 잊어버린다면 시스템 전체가 충돌하거나, 비밀이 유출되거나, 해커가 몰래 침입하는 일이 발생할 수 있습니다. 수년 동안 엔지니어들은 수백만 개의 무작위 메시지로 번역기를 테스트하여 이러한 버그를 잡으려 노력해 왔습니다. 하지만 이것은 마치 건초더미를 흔들어서 바늘을 찾는 것과 같습니다. 바늘을 찾을 수는 있겠지만, 모든 바늘을 다 찾았다고 확신할 수도 없고, 찾은 것이 정말 진짜 바늘인지도 알 수 없습니다.
이때 펜실베이니아 주립대 연구진이 만든 새로운 도구인 VUPER가 판도를 바꿉니다. VUPER는 단순히 건초더미를 흔드는 대신, 처음부터 수학적으로 완벽한 번역기를 구축합니다. 이것은 컴퓨터 수학자에 의해 100% 정확함이 증명된 "골드 스탠다드(표준)" 사전과 문법책을 만드는 것과 같습니다. 연구진은 이 완벽한 번역기를 사용하여 실제 5G 네트워크와 차량 사물 통신(V2X) 시스템에서 사용되는 11개의 다른 인기 있는 파서들을 테스트했습니다. 그 결과, 널리 사용되는 많은 번역기가 실제로 20가지 유형의 규칙을 놓치는 등 규격에 맞지 않는다는 사실을 발견했습니다. 어떤 경우에는 이러한 불일치로 인해 해커가 휴대전화를 마비시키거나 네트워크가 암호화되지 않은 메시지를 보내도록 속일 수도 있었습니다. VUPER는 우리가 가진 번역기를 항상 신뢰할 수는 없지만, 수학적으로 안전함이 보장된 번ers를 만들 수 있으며, 이를 통해 고장 난 것들을 고칠 수 있다는 것을 증명합니다.
VUPER 이야기: 완벽한 번역기 만들기
컴퓨터 네트워크의 세계에서 데이터는 파이프를 통해 흐르는 긴 물줄기와 같습니다. 메시지를 보내기 위해 컴퓨터는 데이터를 "직렬화(serialize)"하여 압축된 비트 스트림으로 짜 넣습니다. 이를 받기 위해 다른 컴퓨터는 스트림을 "파싱(parse)"하여 비트를 다시 읽을 수 있는 메시지로 풀어냅니다. 5G 셀룰러 네트워크와 차량 사물 통신(V2X)이라는 고도의 기술이 요구되는 환경에서, 이 과정은 UPER(Unaligned Packed Encoding Rules)라고 불리는 특정 규칙 세트를 사용합니다. "언얼라인드(unaligned, 비정렬)"라고 불리는 이유는 바이트 경계에 신경 쓰지 않고 대역폭을 아끼기 위해 데이터를 비트 단위로 최대한 촘촘하게 채우기 때문입니다.
어려운 점은 UPER의 공식 규칙 책이 코드가 아닌 밀도가 높은 서술형 텍스트로 작성되어 있다는 것입니다. 이로 인해 엔지니어들은 규칙을 구현하는 방식을 추측해야 하며, 이는 미세한 오류로 이어집니다. VUPER의 연구진은 추측하는 것을 멈추기로 했습니다. 그들은 파서가 올바르다는 것을 증명하는 프레임워크를 구축했습니다. 단순히 코드를 쓰고 작동하기를 바라는 것이 아니라, 모든 논리 단계를 검증하기 위해 **Rocq 프로버(prover)**라는 강력한 수학적 도구를 사용했습니다.
"왕복(Round-Trip)" 테스트
VUPER가 어떻게 작동하는지 이해하려면, 책을 비밀 코드로 바꾸었다가 다시 되돌리는 마법의 번역기가 있다고 상상해 보세요. "왕복" 테스트란 문장을 코드로 바꾸고, 그 코드를 다시 문장으로 되돌리는 과정을 의미합니다. 만약 정확히 똑같은 문장이 돌아온다면 번역기가 제대로 작동하는 것입니다.
하지만 UPER에는 특별한 변칙이 있는데, 바로 **확장(extensions)**입니다. 기술이 진화함에 따라(예: 4G에서 5G로 이동) 메시지에 새로운 기능이 추가됩니다. 오래된 번역기는 새로운 메시지를 읽을 때, 자신이 이해하지 못하는 새로운 부분은 무시하면서도 기존의 부분들은 여전히 이해할 수 있어야 합니다. 이를 **순방향 호환성(forward compatibility)**이라고 합니다. VUPER는 다음 두 가지를 증명함으로써 이를 처리합니다:
- 엄격한 왕복(Strict Round-Trip): 메시지가 동일한 버전에서 온 경우, 번역기는 반드시 원래의 비트 패턴과 정확히 일치하도록 되돌려 놓아야 합니다. 추가적인 비트도, 누락된 비트도 없어야 합니다.
- 약한 왕복(Weak Round-Trip): 메시지에 새로운 미지의 확장이 포함된 경우, 번역기는 이를 건너뛸 수 있지만, 여전히 알려진 부분들을 유효한 메시지로 되돌릴 수 있어야 합니다. (모르는 부분이 사라졌으므로) 비트 단위로 완벽히 일치할 필요는 없지만, 나머지 부분을 손상시켜서는 안 됩니다.
버그 찾기
연구진은 VUPER에 의해 생성된 "신뢰할 수 있는 오라클(trusted oracle)" 즉, 완벽한 파서를 구축했고, 이를 사용하여 11개의 다른 파서를 테스트했습니다. 여기에는 7개의 오픈 소스 도구(asn1c, pycrate 등)와 실제 4G 및 5G 기지국(휴대전기를 네트워크에 연결하는 하드웨어) 내부에서 사용되는 4개의 상용 파서가 포함되었습니다.
그들은 단순히 무작위 쓰레기 데이터를 보낸 것이 아니라, 메시지의 구조를 이해하는 스마트한 "퍼저(fuzzer)"를 사용하여 수백만 개의 까다로운 테스트 케이스를 만들어냈습니다. 결과를 비교했을 때, 다른 파서들에서 20가지 유형의 불일치를 발견했습니다.
가장 흥-미로운 발견 중 일부는 다음과 같습니다:
- "너무 긴" 문제: 일부 파서는 할당된 공간보다 큰 숫자를 수용하거나, 데이터와 일치하지 않는 길이를 수용했습니다. 이는 우체부에게 "편지에 5페이지가 있다"라고 적힌 편지를 받았는데 실제로는 100페이지가 들어있어, 우편함이 넘쳐나고 결국 고장 나는 상황과 같습니다.
- "미지의 확장" 혼란: 메시지에 오래된 파서가 모르는 새로운 기능이 포함되었을 때, 일부 파서는 혼란에 빠져 메시지의 엉뚱한 부분을 읽기 시작했고, 그것을 전혀 다른 것으로 오해했습니다. 이는 번역가가 외국어의 새로운 단어를 보고 당황하여 문장의 나머지 부분을 잘못 번역하는 것과 같습니다.
- "기본값(Default Value)" 실수: 규칙에 따르면 공간을 아끼기 위해 값이 "기본값"인 경우 아예 전송하지 않아야 합니다. 하지만 일부 파서는 여전히 이를 보내거나, 값이 누락되었을 때 이를 인식하지 못했습니다.
현실 세계의 위험성
이 논문은 단순히 이론적인 버그를 찾아낸 것에 그치지 않고, 이것이 어떻게 악용될 수 있는지 보여주었습니다. 연구진은 네 가지 구체적인 공격을 시연했습니다:
- 휴대전기 충돌: 제약 조건을 위반하여 약간 너무 길게 설계된 네트워크 ID 목록이 담긴 메시지를 보냄으로써, 휴대전지의 소프트웨어를 충돌시켜 서비스 거부(DoS) 상태를 만들었습니다.
- 기지국 충돌: 해킹된 기지국이 다른 기지국에 잘못된 메시지를 보내, 두 번째 기지국이 이를 처리하는 동안 기지국을 충돌시킬 수 있습니다.
- 비밀 유출: 미지의 확장 기능 때문에 파서가 메시지를 잘못 해석하면, 보안 설정이 "켜져" 있음에도 "꺼져" 있다고 생각하거나 그 반대의 상황이 발생할 수 있습니다. 이는 휴대전기는 보안 통신을 하고 있다고 믿지만, 실제로는 네트워크가 데이터를 평문으로 보내고 있어 도청자가 내용을 읽을 수 있는 상황을 초래할 수 있습니다.
- 장치 지문 채취(Device Fingerprinting): 서로 다른 파서들이 오류를 처리하는 방식이 다르기 때문에, 해커는 특정 "트릭" 메시지를 보내고 장치가 어떻게 반응하는지 관찰할 수 있습니다. 만약 장치가 이상한 메시지를 수용한다면, 해커는 해당 장치가 특정 브랜드의 하드웨어(예: 삼성 베이스밴드)를 사용하고 있음을 알 수 있고, 이를 통해 알려진 취약점을 이용해 특정 장치를 정밀 타격할 수 있습니다.
성능과 미래
연구진은 자신들의 완벽하고 수학적으로 검증된 파서가 현재 가장 빠른 것은 아니라는 점을 인정합니다. 현재 업계에서 사용되는 고도로 최적화된 C 라이브러리보다 약 4배 느립니다. 하지만 Python 기반 파서들보다는 4배 빠릅니다.
VUPER의 목표는 즉시 기존의 빠른 파서들을 대체하는 것이 아니라, 참조 구현(reference implementation) 역할을 하는 것입니다. 마치 숙련된 요리사가 요리를 맛보고 레시피의 잘못된 점을 정확히 짚어내는 것처럼, VUPER는 엔지니어들에게 그들의 파서가 어디에서 실패하고 있는지 정확히 알려줄 수 있습니다. 연구진은 VUPER를 사용하여 이러한 버그를 찾아 고침으로써, 궁극적으로 빠르면서도 수학적으로 안전함이 보장되는 파서를 구축할 수 있기를 기대하고 있습니다.
결론적으로 VUPER는 5G와 그 이후의 복잡하고 고속인 세상에서, 더 이상 "적당히 괜찮은" 테스트에 의존해서는 안 된다는 것을 보여줍니다. 우리의 디지털 도시를 안전하고 보안이 유지되며 원활하게 돌아가게 하려면, 수학적으로 증명된 번역기가 필요합니다.
연구 분야의 논문에 파묻히고 계신가요?
연구 키워드에 맞는 최신 논문의 일일 다이제스트를 받아보세요 — 기술 요약 포함, 당신의 언어로.