메모리 안전성은 정의하기 어려운 개념이며, 언어 자체가 아니라 구현의 성질로 이해해야 한다는 관점에서 기존 정의들의 문제점을 짚고, 컴파일러 정당성의 후방 시뮬레이션을 약화한 형태로 메모리 안전성을 정식화한다.
2025년 12월 30일
메모리 안전성은 지능, 의식, 혹은 포르노 같은, 말로 규정하려 하면 잘 빠져나가는 개념 중 하나다. 그래서 나는 이걸 정의하려고 시도하지 않겠다. 대신 다른 사람들이 내놓은 정의들에 구멍을 내보려 한다.
참고로 이 글은 제논(Zeno) 풍의 궤변이 90%다 — 합리적인 토론을 위해 물 샐 틈 없는 정의가 꼭 필요하다고 생각하지 않고, 어떤 정의도 비합리적인 토론을 구해주지 못한다. 하지만 정의를 생각해보는 과정은 정신을 집중시킨다.
내 주장의 핵심은 이것이다:
메모리 안전성은 _구현(implementation)_의 성질이다.
많은 정의가 문제인 이유가 바로 이것이다 — 잘못된 종류의 대상을 다루기 때문에 혼란이 생긴다. 예를 들어, Memory Safety for Skeptics에서 쓰인 정의:
어떤 나쁜 일들의 목록(메모리 접근 오류라 부름)이 결코 발생하지 않는 한, 프로그램 실행은 메모리 안전하다:
- 버퍼 오버플로
- 널 포인터 역참조
- 해제 후 사용(use-after-free)
- 초기화되지 않은 메모리 사용
- 불법 free(이미 free된 포인터, 또는 malloc으로 할당되지 않은 포인터)
이건 명백한 헛소리다! 자바 프로그램은 널 포인터를 늘 역참조한다! 그리고 일반적인 아키텍처에서 사용자 공간(user-space)에서의 널 포인터 역참조는 트랩(trap)으로 잘 정의되어 있다. 많은 JVM은 자바 수준의 NPE 검사를 OS 수준의 세그폴트(segfault)에 기대서 구현한다!
또 다른 유명한 정의는 Luca Cardelli의 Type Systems 논문에서 나온다.
어떤 프로그램 조각이(trapped되지 않은) 오류를 일으키지 않는다면 안전하다. 모든 프로그램 조각이 안전한 언어를 안전한 언어(safe languages)라 부른다.
이 정의는 틀렸다고 하긴 어렵지만, 공허하다. 내부적으로는 일관되지만, 유용한 무언가를 정의하지 못한다.
이를 보려면 우리가 다루는 담론의 영역을 그려봐야 한다.
우리는 자바나 C 같은 소스 언어 L에서 시작한다. L은 문법(syntax)과 의미론(semantics)으로 정의된다. 문법은 프로그램들의 집합을 정하고, 의미론은 그 프로그램들에 의미를 부여한다. 의미론은 필연적으로 추상 머신 LM — 프로그램의 실행 동작을 설명하기 위해 실제 및 “가상” 상태를 모두 포착하는 수학적 장치 — 의 관점에서 정의된다. 예를 들어 포인터 provenance가 있는 언어라면, provenance는 추상 머신에서 모든 포인터가 가지는 구체적인 “필드”다.
LM(추상 머신) 외에도, 우리는 x86_64 리눅스 사용자 공간, 혹은 브라우저의 Wasm 같은 구체 머신(concrete machine) CM을 가진다. 구체 머신은 그 자체의 언어 C와 그 자체의 의미론을 갖는다.
마지막으로, L 프로그램을 구체 머신 CM에서 실행하기 위해 사용하는 구현 I가 있다. 대략적으로, P가 L 프로그램이라면 구현은 이를 의미가 일치하는 C 프로그램으로 변환한다:
∀ P ∈ L:
I(P) ∈ C
∧ LSema(P) ≈ CSema(I(P))
구체적으로, 자바 프로그램이 있다면 우리는 이 프로그램이 무엇을 하는지, 어디서 실행될지를 굳이 생각하지 않고도 추론할 수 있다. 그 프로그램이 aarch64 노트북에서 실행될 때 우리의 정신 모델을 충실히 보존하는 것이 JVM의 일이다. 자세한 내용은 Compcert 논문을 보라.
여기서 핵심 디테일은: 추상 의미론의 수준에서는 정의되지 않은 동작(Undefined Behavior, UB)이 있을 수 없다는 점이다. 명세가 일관되려면, 어떤 경우든 추상 머신이 무엇을 하는지를 철저히 설명해야 한다. 설령 그 설명이 “AM이 막힌다(gets stuck)”뿐이라도 말이다. UB가 정의된 동작들의 여집합이라면, UB 또한 똑같이 정밀하게 정의된다! 다시 말해, Compcert 논문은 15페이지에서 UB가 무엇인지 _정의_한다.
이것이 내가 Cardelli의 정의에 불만을 갖는 이유다. 그 정의는 추상 의미론에서 어떤 집합을 어떻게 _이름 붙이느냐_에 달려 있다. 그 집합이 “트랩된 오류(trapped error)”라 불리면 언어는 안전하고, “정의되지 않은 동작(undefined behavior)”이라 불리면 안전하지 않다.
이건 무의미하다! 내가 방금 Lil-C라는 언어를 만들었다고 하자. C와 완전히 똑같지만, 모든 UB가 형식적으로 트랩하도록 정의되어 있다. 그럼 안전하다! 그리고 어떤 C 프로그램이든 실행할 수 있다! 내가 유용한 일을 한 건가? 아니다!
정리하자면, 우리는 소스 언어 L, 타깃 언어/머신 C, 그리고 L을 C로 매핑하는 구현 I를 갖고 있다. 어떤 메모리 안전성 정의든 I에 대해 말해야 한다. L이나 C에 대해 말한다면, 올바를 수 없다.
“야생 포인터(wild pointer) 역참조”를 생각해 보자. L 수준에서는, 이것은 추상 머신을 멈추게 만드는 잘 정의된 연산이다. 어떤 포인터가 역참조 가능한지 정확히 말해주는 것이 추상 머신의 _역할_이다. C 수준에서도 이 연산은 잘 정의되어 있다! 물리 주소가 페이지 테이블에서 조회되고, 보호 비트가 검사되고, 뭔가 이상하면 인터럽트가 올라가는 등등. UB와 메모리 비안전성은 L의 의미론이 C로 번역되는 _과정_에서 발생한다. L에서의 “막힌” 상태가 C에서는 “예상치 못한” 동작을 낳고, 그 동작은 L의 관점에서 설명할 수 없다.
Cardelli의 정의가 공허해지는 이유는, L을 고립된 채로 이야기하려 하기 때문이다.
“skeptics” 정의는 이중으로 혼란스럽다. L을 염두에 둔 것인지 C를 염두에 둔 것인지(소스 코드에서의 널 포인터 역참조인지, 생성된 머신 코드에서의 역참조인지) 불분명하고, 어느 쪽이든 I를 건드리지 않으니 틀릴 수밖에 없다.
긍정적인 예로 Fil-C(또한 A note on Fil-C 참고)를 보자. 이것은 C의 의미론을 유지하면서도 안전하고, 실용적일 만큼 충분히 효율적이라고 주장할 수 있는 C의 _구현_이다. 내 Lil-C와 달리 Fil-C는 유용한 물건이다(그리고 이를 해내려면 훨씬 더 많은 노력이 필요하다).
여기서는 메모리 안전성을 정의하지 않겠다고 약속했지만, Compcert 논문을 대충 훑어본 뒤(팁을 준 @pervognsen에게 감사), 그래도 한번 무리해서 정의해보고 싶어졌다. Compcert 논문은 후방 시뮬레이션(backward simulation)을 “컴파일된 프로그램의 모든 동작은 소스 프로그램의 동작이다”라는 성질로 정의한다(비결정성 때문에 프로그램의 의미론은 동작들의 _집합_이다). 이 글의 표기법을 쓰면:
P ∈ L -- 소스 프로그램
I: L -> C -- 구현(예: L에서 C로 가는 컴파일러)
I(P) ∈ C -- 컴파일된 프로그램
LSema(P) -- P의 가능한 동작들
CSema(I(P)) -- 구현 I 하에서의 P의 동작들
-- 후방 시뮬레이션:
∀B: B ∈ CSema(I(P)) => B ∈ LSema(P)
메모리 안전성은 후방 시뮬레이션의 약화 형태다:
-- 구현 I의 메모리 안전성:
MemorySafe(I) :=
∀ P: ∀B: B ∈ CSema(I(P)) => (B ∈ LSema(P) ⋁ B = crash)
언어 L의 구현 I가 메모리 안전하다는 것은, 임의의 프로그램 P(버그가 있는 것까지 포함)에 대해, 충돌(crash)을 허용하는 것을 제외하면 새로운 놀라운 동작을 만들어낼 수 없다는 뜻이다. 간단한 스모크 테스트로, 항상 즉시 크래시하는 프로그램을 생성하는 구현은 이 정의에 따르면 안전하다. 마땅히 그래야 한다.
정의를 생각해보는 일은 действительно(정말로) 정신을 집중시킨다!
업데이트(2025-12-31): 또 읽어볼 만한 흥미로운 논문은 The Meaning Of Memory Safety다. 나는 그들의 정의가 필요 이상으로 상당히 강해진다고 생각한다: 자바보다는 CHERI에 더 가깝고, 자바스크립트는 메모리 안전하지 않다고 판정한다. 그래도 읽을 가치는 있다!