소개

Lean은 의존 타입 이론을 기반으로 하는 대화형 정리 증명기 입니다. 원래 Microsoft Research에서 개발되었으나, 현재는 Lean FRO에서 개발이 진행되고 있습니다. 의존 타입 이론은 프로그램과 증명의 세계를 하나로 묶어주기 때문에 Lean은 프로그래밍 언어이기도 합니다. Lean은 이러한 이중적 특성을 진지하게 받아들이며, 범용 프로그래밍 언어로 사용하기에 적합하도록 설계되었습니다. 심지어 Lean은 Lean 자체로 구현되어 있습니다. 이 책은 Lean으로 프로그램을 작성하는 법에 관한 것입니다.

프로그래밍 언어로서의 Lean은 의존 타입을 가진 엄격한 순수 함수형 언어입니다. Lean으로 프로그래밍하는 법을 배우는 과정의 상당 부분은 이러한 각 속성이 프로그램 작성 방식에 어떤 영향을 미치는지, 그리고 어떻게 함수형 프로그래머처럼 생각할 수 있는지를 익히는 것으로 구성됩니다. 엄격성 은 Lean의 함수 호출이 대부분의 언어와 유사하게 작동하는 것을 의미합니다. 즉, 함수의 본문이 실행되기 전에 인자값이 완전히 계산된다는 의미입니다. 순수성 은 프로그램에서 타입에 명시되지 않는 한, Lean 프로그램이 메모리 위치 수정, 이메일 전송, 파일 삭제와 같은 부수 효과(side effect)를 가질 수 없음을 의미합니다. Lean이 함수형 언어라는 것은 함수가 다른 값들과 마찬가지로 일급 객체이며, 실행 모델이 수학적 표현식의 평가에서 영감을 얻었음을 뜻합니다. Lean의 가장 독특한 특징인 의존 타입은 타입을 언어의 일급 구성 요소로 만들어, 타입이 프로그램을 포함하거나 프로그램이 타입을 계산할 수 있게 합니다.

이 책은 Lean을 배우고 싶지만 반드시 함수형 프로그래밍 언어를 사용해 본 적은 없는 프로그래머들을 대상으로 합니다. Haskell, OCaml, F#과 같은 함수형 언어에 익숙할 필요는 없습니다. 반면, 이 책은 대부분의 프로그래밍 언어에서 공통적으로 쓰이는 루프, 함수, 데이터 구조와 같은 개념에 대한 지식은 갖추고 있다고 가정합니다. 이 책이 함수형 프로그래밍에 관한 좋은 입문서가 될 수는 있지만, 프로그래밍 전반에 관한 입문서로는 적합하지 않습니다.

Lean을 증명 보조기로 사용하는 수학자들도 언젠가는 맞춤형 증명 자동화 도구를 작성해야 할 때가 올 것입니다. 이 책은 그분들을 위한 것이기도 합니다. 이러한 도구들이 정교해질수록 함수형 언어의 프로그램과 닮아가지만, 대부분의 현직 수학자들은 Python이나 Mathematica 같은 언어에 익숙합니다. 이 책은 그 간극을 메워줌으로써 더 많은 수학자가 유지보수 가능하고 이해하기 쉬운 증명 자동화 도구를 작성할 수 있도록 도울 것입니다.

이 책은 처음부터 끝까지 순서대로 읽도록 구성되었습니다. 개념은 하나씩 도입되며, 뒷부분은 앞부분의 내용을 숙지하고 있다고 가정합니다. 때로는 앞서 짧게 다루었던 주제를 나중에 더 깊이 있게 파고들기도 합니다. 책의 일부 섹션에는 연습 문제가 포함되어 있습니다. 해당 섹션의 이해를 공고히 하기 위해 풀어볼 가치가 있습니다. 또한 책을 읽으면서 배운 내용을 창의적이고 새로운 방식으로 활용하며 Lean을 직접 탐구해 보는 것도 유익합니다.

Lean 시작하기

Lean으로 작성된 프로그램을 작성하고 실행하기 전에, 먼저 컴퓨터에 Lean을 설치해야 합니다. Lean 도구 모음은 다음과 같이 구성됩니다:

• elan은 rustup이나 ghcup과 유사하게 Lean 컴파일러 툴체인을 관리합니다.
• lake는 cargo, make, 또는 Gradle과 유사하게 Lean 패키지와 그 의존성을 빌드합니다.
• lean은 개별 Lean 파일의 타입을 검사하고 컴파일하며, 현재 작성 중인 파일에 대한 정보를 프로그래머 도구에 제공합니다. 보통 lean은 사용자가 직접 실행하기보다는 다른 도구에 의해 호출됩니다.
• Visual Studio Code나 Emacs와 같은 에디터용 플러그인은 lean과 통신하여 관련 정보를 편리하게 보여줍니다.

Lean 설치에 관한 최신 지침은 Lean 매뉴얼을 참조하시기 바랍니다.

타이포그래피 관례

Lean에 입력으로 제공되는 코드 예제는 다음과 같은 형식으로 표시됩니다:

def add1 (n : Nat) : Nat := n + 1

#eval add1 7

위의 마지막 줄(#eval로 시작하는 줄)은 Lean에게 답을 계산하도록 지시하는 명령입니다. Lean의 응답은 다음과 같은 형식으로 표시됩니다:

8

Lean이 반환하는 오류 메시지는 다음과 같은 형식으로 표시됩니다:

Application type mismatch: The argument
  "seven"
has type
  String
but is expected to have type
  Nat
in the application
  add1 "seven"

경고는 다음과 같은 형식으로 표시됩니다:

declaration uses 'sorry'

유니코드

관용적인 Lean 코드는 ASCII에 포함되지 않는 다양한 유니코드 문자를 사용합니다. 예를 들어, 그리스 문자 α, β 및 화살표 →는 모두 이 책의 첫 번째 장에 등장합니다. 이를 통해 Lean 코드는 일반적인 수학적 표기법과 더 유사해질 수 있습니다.

기본 Lean 설정에서 Visual Studio Code와 Emacs 모두 백슬래시(\) 뒤에 이름을 입력하여 이러한 문자를 입력할 수 있습니다. 예를 들어, α를 입력하려면 \alpha를 입력합니다. Visual Studio Code에서 문자를 입력하는 방법을 알아보려면 해당 문자 위에 마우스를 올려 툴팁을 확인하세요. Emacs에서는 해당 문자 위에 커서를 두고 C-c C-k를 사용하세요.

저자 소개

David Thrane Christiansen 은 20년 동안 함수형 언어를 사용해 왔으며, 의존 타입을 사용한 지는 10년이 되었습니다. 그는 Daniel P. Friedman과 함께 의존 자료형 이론의 핵심 아이디어를 소개하는 The Little Typer 를 집필했습니다. 코펜하겐 IT 대학교에서 박사 학위를 받았으며, 재학 시절 Idris 언어의 첫 번째 버전에 주요 기여자로 참여했습니다. 학계를 떠난 후에는 미국 오리건주 포틀랜드의 Galois와 덴마크 코펜하겐의 Deon Digital에서 소프트웨어 개발자로 일했으며, Haskell Foundation의 상임 이사를 역임했습니다. 집필 당시 그는 Lean Focused Research Organization 에 소속되어 풀타임으로 Lean 프로젝트에 매진하고 있습니다.

감사의 글

이 무료 온라인 도서는 Microsoft Research의 아낌없는 지원 덕분에 집필 및 무료 배포가 가능했습니다. 집필 과정에서 그들은 Lean 개발팀의 전문 지식을 제공하여 제 질문에 답해주고 Lean을 더 사용하기 쉽게 만들어 주었습니다. 특히 Leonardo de Moura는 이 프로젝트를 시작하고 제가 첫발을 뗄 수 있게 도와주었으며, Chris Lovett은 CI 및 배포 자동화를 구축하고 테스트 독자로서 훌륭한 피드백을 주었습니다. Gabriel Ebner는 기술 검토를 맡았고, Sarah Smith는 행정적인 업무가 원활히 돌아가도록 힘써주었으며, Vanessa Rodriguez는 소스 코드 하이라이트 라이브러리와 특정 버전의 iOS용 Safari 간의 까다로운 상호작용 문제를 진단하는 데 도움을 주었습니다.

이 책을 쓰는 데는 평소 근무 시간 외에도 많은 시간이 소요되었습니다. 제 아내 Ellie Thrane Christiansen은 평소보다 더 많은 가사 분담을 도맡아 주었으며, 아내의 헌신이 없었다면 이 책은 존재할 수 없었을 것입니다. 매주 하루씩 추가로 일하는 것이 가족들에게 쉽지 않은 일이었음에도, 집필 기간 동안 인내심을 갖고 지지해 준 가족들에게 감사의 마음을 전합니다.

Lean을 둘러싼 온라인 커뮤니티는 기술적으로나 정서적으로 이 프로젝트에 열렬한 지지를 보내주었습니다. 특히 Sebastian Ullrich는 에러 메시지 텍스트를 CI에서 확인하고 책에 쉽게 포함할 수 있도록 지원 코드를 작성할 때, 제가 Lean의 메타프로그래밍 시스템을 익히는 데 핵심적인 도움을 주었습니다. 새로운 개정판을 게시한 지 불과 몇 시간 만에 열정적인 독자들이 오류를 찾아내고, 제안을 건네며, 따뜻한 격려를 보내주었습니다. 특히 문체와 기술적인 면에서 많은 제안을 주신 Arien Malec, Asta Halkjær From, Bulhwi Cha, Craig Stuntz, Daniel Fabian, Evgenia Karunus, eyelash, Floris van Doorn, František Silváši, Henrik Böving, Ian Young, Jeremy Salwen, Jireh Loreaux, Kevin Buzzard, Lars Ericson, Liu Yuxi, Mac Malone, Malcolm Langfield, Mario Carneiro, Newell Jensen, Patrick Massot, Paul Chisholm, Pietro Monticone, Tomas Puverle, Yaël Dillies, Zhiyuan Bao, 그리고 Zyad Hassan에게 감사의 인사를 전하고 싶습니다.

당신은 게임에 갇힌 미소녀들을 보기 위해 PlayStation을 켰습니다. 마침 친구가 "나 이쪽 루트 클리어했는데 너도 볼래?" 라며 세이브 파일을 주네요. 마침 그 루트로 갈 시기를 놓친 당신은 친구의 세이브를 이용해 확인해보려고 합니다. 세이브를 등록 후, 미연시를 켜서 로드했는데..? 갑자기 콘솔이 멈추며 결국 콘솔 내부 저장공간을 포맷했습니다!

... 당연히 위 내용은 실제 스토리가 아니지만, 충분히 일어날 수 있습니다. 이 글에서 설명할 내용들로 말이죠.

yarpe

yarpe(Yet Another Ren'Py PlayStation Exploit)를 소개합니다!

이 스크립트는 Ren'Py 기반의 PlayStation 게임들에서 적용되는 취약점이며, 현 시점에서 적용 가능한 게임은 다음과 같습니다:

• A YEAR OF SPRINGS PS4 (CUSA30428, CUSA30429, CUSA30430, CUSA30431)
• Arcade Spirits: The New Challengers PS4 (CUSA32096, CUSA32097)

그런데, 이 모든 것이 어떻게 시작되었고, 어떻게 만들어진걸까요?

Xbox One/Series

사실 저는 PlayStation(이하 PS로 줄여서 말하겠습니다)에 관심이 없었습니다. 반대로 Xbox에 많은 관심이 있었죠. 처음 Xbox One/Series의 커널 취약점이 생겼을 때 Warhammer: Vermintide 2의 게임 세이브 취약점을 이용한 게임 덤프가 제 눈에 잡혔습니다. 그때 문뜩 든 생각이: "다른 게임은 이런 세이브 취약점이 없을까?" 였는데요, 저와 같이 이런 작업에 관심을 두는 친구가 먼저 추천해준 것은 RPG Maker(쯔꾸르 라고도 많이 불리죠)로 만들어진 게임들이었습니다. 아쉽게도, 콘솔 버전에서 사용하는 RPG Maker 게임들은 다른 세이브 구조를 가지고있었고, ACE(Arbitrary Code Execution)가 불가능했습니다.

그러다 문뜩 생각이 났습니다: "Ren'Py 게임들이 세이브로 Pickle을 사용하지 않나?"

Pickle

Python에는 Pickle이라는 직렬화(serialization) 방식이 존재합니다. 이는 Python의 (왠만한) 모든 object를 직렬화할 수 있는 특징이 있습니다.

하지만 만약 직렬화하지 못하는 object가 class의 property로 존재하는데, 이 class를 직렬화하고 싶다면 어떻게 해야할까요? Python은 이를 위해 __reduce__라는 method를 지원합니다. 이는 class가 직렬화/역직렬화 될 때 어떤 데이터를 사용하여 class를 다시 구성해야할지 명시해줍니다. 사용법은 다음과 같습니다:

class A:
    def __init__(self, a):
        self.a = a
        self.b = "b"

    def __reduce__(self):
        return self.__class__, (self.a,)

# serialize
a = A()
b = pickle.dumps(a)

그런데, 만약 __reduce__에 다른 Python 함수가 있으면 어떨까요? 예를 들어, exec 같은거라면 말이죠?

class Exploit:
    def __reduce__(self):
        return exec, ("print('Hello, World!'),)

exploit = Exploit()
a = pickle.dumps(exploit)

pickle.loads(a) # Hello, World!

...네, Pickle이 로딩될 때 문자열에 담긴 코드를 실행해버립니다... 이것이 Python 공식 Pickle 문서에서 Pickle이 안전하지 않다고 하는 이유겠죠.

세이브 하나로 Ren'Py 게임 가지고 놀기

이제 Ren'Py가 Pickle을 사용한다는 사실과, Pickle로 코드를 실행할 수 있다는 사실을 알았으니, 직접 실행해볼 시간입니다!

Ren'Py의 세이브는 1-1-LT1.save 같은 파일 이름을 가지고 있습니다. 멋져보이지만, 사실 그냥 Zip 파일이며, 확장자만 .save로 변경된겁니다. 이를 흔한 Zip 프로그램으로 풀어보면, 여러 파일들이 나오지만 우리가 관심있는 파일은 log 파일입니다. 이 파일이 Ren'Py의 Pickle을 담고있는 파일이죠. 이제 이 파일을 제가 만든 코드가 담긴 Pickle로 바꿔치기 하고, 다시 압축을 해서 넣으면..?

코드 실행이 됩니다! 너무 멋지네요!

코드 실행은 되는데, 이제 어쩌죠?

이제 코드 실행이 되는걸 알았으니, 다음 단계는 무엇일까요? 당연히 메모리 조작이죠! Google에서 잠시 조사한 결과 unsafe-python 이라는 저장소가 눈에 들어왔습니다. 이 저장소는 Python에서 직접적인 메모리 접근을 가능하게 합니다.

해당 취약점은 LOAD_CONST opcode가 아무 범위 검사를 하지 않는다는 점을 이용하여 가짜 PyObject를 만들 수 있고, 이를 이용하여 0부터 사실상 64비트 주소 끝자락까지의 bytearray 객체를 만들어 직접적인 메모리 접근을 합니다.

이제 우리는 메모리 주소만 알면 언제든지 해당 메모리를 수정할 수 있습니다! 덤으로, Python의 사랑스러운 slicing 문법은 이를 더 편하게 만듭니다.

# Assume we got raw memory bytearray
mem = getmem()

mem[0x18000000:0x18000008] = b'\0' * 8

이제 마음대로 메모리 조작도 가능하고, PyObject 생성도 가능하니, 저만의 프로그램을 메모리에 저장한 후 Python의 function 객체를 만들어 제 코드를 향하게 하면 끝입니다!

...가 된다면 정말 쉬울건데 말이죠...

메모리 영역 권한

메모리 영역에는 특정 권한이 부여되어 있습니다. Read, Write, eXecute 권한이 분리되어 있는데, 이름에서 알 수 있듯 execute 권한 없이는 해당 메모리 영역을 코드로서 실행할 수 없습니다.

문제되는 부분은, 보통 우리가 작성하는 영역은 read와 write만 있고, execute 권한이 없습니다! 만약 execute 권한이 없는 영역을 실행하려 한다면, CPU에서 권한 부족 오류를 발생시킬 것이고, 이는 segfault로 이어질 것입니다.

그럼 현재 부족한 메모리 권한으로 원하는 명령을 어떻게 실행할 수 있을까요? 답은 ROP에 있습니다.

ROP

ROP, Return Oriented Programming은 말 그대로 asm의 ret 명령을 기준으로 작동하는 코드를 말합니다.

ret 명령의 특징은 현재 CPU가 가리키는 stack pointer(x86_64 기준 RSP register) 에 적힌 주소 값을 instruction pointer(x86_64 기준 RIP register)에 적고 stack pointer를 움직인다는 것입니다. 그럼 ret를 실행하는 때에 stack pointer를 (실행 가능한 메모리 영역에 있는) 저희가 원하는 코드로 향하게 하면 어떨까요? 이를 하기 위해선, ret로 끝나면서 원하는 명령을 실행하는 메모리 주소를 미리 찾아놓아야 할 것입니다. 이를 우리는 gadget이라고 부릅니다.

Stack pointer에서도 권한 오류가 발생할 수 있지 않을까 하실 수도 있지만, stack pointer가 가리키는 메모리 영역은 read, write 권한만으로 충분하기 때문에 괜찮습니다.

이 사실을 알게된다면 이제 이런 구상을 할 수 있습니다:

1. Python list를 통해 custom stack을 만든다.
2. Custom stack에는 적절히 gadget을 배치한다.
3. Stack pointer를 원하는 주소(여기선 Python list의 elements 주소)로 변경하는 gadget을 향하도록 한 Python function 객체를 만든다.
4. 해당 Python function 객체를 실행한다. Stack pointer가 옮겨지고 ret가 호출되며 원하는 명령이 실행된다!

...많은 것들이 축약되있지만 대략적으로 이런 구상이 가능하죠. 이제 이를 이용해서 취약점을 만들 시간입니다!

Gadget 찾기

앞서 말했듯 ROP를 하기 위해선 적절한 gadget을 찾는 것이 중요합니다. 저는 이를 위해 ROPgadget 툴을 이용했습니다. 원하는 executable과 함께 툴을 실행하면 ret로 끝나는 모든 asm 명령들을 메모리 주소 값과 함께 찾아줍니다! (가상 메모리 주소까지 고려해서요!)

다음엔 두 가지 방법이 있습니다:

1. Executable 메모리를 읽으며 gadget 주소를 동적으로 찾기
2. 미리 해당 gadget들의 주소를 적어둔 dict 만들기

Xbox One/Series에선 1번 방법을 사용할 수 있었지만, PS에선 후에 언급할 내용 때문에 2번 방법을 쓸 수 밖에 없었습니다.

Stack pointer를 원하는 주소로 옮기기

이제 stack pointer를 만들어둔 Python list 주소로 옮기면 되는데, 어떻게 옮길까요? 저희가 원하는건 (x86_64 기준) mov rsp, ???와 ret입니다. 여기서 저 ???부분이 중요한데, 왜냐하면 Python function 호출이 어떻게 이루어지는지 알아야하며, 실행되는 CPU와 OS의 함수 호출 convention도 알아야하기 때문입니다.

여기서 함수 호출 convention이란 함수를 호출할 때 몇번째 argument가 어떤 register에 들어가는지를 뜻합니다.

Linux/UNIX 기반 OS의 x86_64 함수 호출 convention 순서는 다음과 같습니다: RDI, RSI, RDX, RCX, R8, R9

그리고 Python function 호출은 다음과 같이 이루어집니다: function_call(PyObject* func, PyObject *arg, PyObject *kw)

따라서 만약 mov rsp, [rdi + 0x30]; ret 라는 명령을 찾았다면, 직접 만드는 Python function 객체 안 0x30 정도 되는 곳에 원하는 stack 주소를 넣어야할 것이고, mov rsp, [rsi + 0x10]; ret 라는 명령을 찾았다면, 직접 tuple 객체를 만든 후 0x10 정도 되는 곳에 stack 주소를 저장, 만든 function 객체를 부를 때 my_func(*custom_tuple)과 같이 호출해야 할 것입니다.

다 만들었으니 실행하면 되는데... Python으로 못 돌아오고 crash?

ROP에서 가장 중요한걸 깜빡했네요. 직접 만든 stack을 실행하고 나선 다시 원래 stack으로 돌아와야겠죠.

저같은 경우는 push rbp; mov rbp, rsp; xor esi, esi; call [rdi + 0x130] 명령을 이용하여 rbp에 rsp를 저장한 후 원하는 명령을 실행하도록 만들었습니다(rdi + 0x130에는 stack pointer를 변경하는 명령이 있습니다).

이 다음 원하는 명령 실행 후 mov rsp, rbp; pop rbp; ret 명령을 통해 다시 원래 stack pointer로 돌아옵니다. 이렇게만 하면 될까요..? 아닙니다. 이렇게 하면 Python이 함수의 return value(x86_64 기준 RAX register)를 참조하려다 잘못된 값을 참조하여 오류가 발생합니다. 그럼 어떻게 해야할까요?

정답은 None 객체를 반환해주는 것입니다. 이렇게 하면 Python에게 정상적인 값을 반환하게 되며, 오류가 발생하지 않게 됩니다. (그리고 네, None도 하나의 객체입니다.)

주의할 점은 None 객체의 refcount를 1만큼 올려주어야 합니다. 그렇지 않으면 Python이 return value의 refcount를 줄이려 할 때, underflow 문제가 발생할 수 있습니다.

이것까지 마치면, 진짜로 저희가 원하는 명령을 실행할 수 있게 됩니다!

Xbox에서 테스트!

Xbox One Research 팀의 도움을 받아 Ren'Py 게임 파일을 받은 뒤 gadget을 찾고, 돌려봤습니다!

Xbox에서 먼저 테스트한 결과 정상적으로 socket을 여는데 성공했으며, 해당 socket으로 다른 Python script를 실행하는 데 성공했습니다! (참고로 해당 게임은 Python의 socket 모듈을 지원하지 않습니다.)

Xbox 같은 경우 Windows와 거의 비슷한 함수를 사용할 수 있어서 편하게 진행할 수 있었습니다.

대망의 PS...

그렇게 Xbox에서 테스팅 후 몇달 뒤, PS 해킹에도 관심이 생겨 알아보게 되었습니다.

그렇게 알게된 Xbox와의 차이점은...

• FreeBSD 기반의 OS를 사용함
• 자체적인 syscall들이 존재함
• 메모리에 올라간 실행 파일에는 ELF 해더가 없음(Import table 알 수 없음)
• 실행 파일에 기록된 모듈만 로드할 수 있음
• PS5 기준: 실행 파일이 담긴 메모리 영역을 읽을 수 없음(XOM)

...Gadget 찾기에서 2번 방법을 사용한 이유가 XOM(eXecutable Only Memory) 때문입니다. 사실 PS4에선 1번 방법을 사용할 수 있지만, 저는 PS5 게임도 지원하고 싶었습니다.

PS5 Research & Development Discord 서버의 도움을 받아 게임 파일을 받았고, 똑같이 gadget을 찾아 작성하였습니다.

위에 적힌 제약들이 있어도, 기본 작동은 비슷하기 때문에 큰 문제 없이 만들 수 있었고, 그렇게 테스트를 한 결과..!

성공적으로 작동되었고, yarpe가 탄생할 수 있었습니다.

마무리

여기까지 오는데 (중간에 쉬었지만) 거의 1년이라는 시간이 걸렸습니다. 만들면서 힘든 것 보단 재밌다는 느낌을 더 많이 받았네요. (만드는 동안은 잠자는 시간마저 줄여가며 만들었던 것 같습니다.)

마무리하기 전에, 저에게 도움이 되었던 분들을 소개하며 끝내고자 합니다.

• Xbox One Research 팀: 이 프로젝트의 시작점이 되어주었으며, 핵심 부분을 구성하는데 큰 도움이 되었습니다. (tuxuser, LukeFZ, Billy, harold님 등이 도와주셨습니다.)
• Dr.Yenyen: PS4/5 게임들의 파일을 제공해주셨고, 많은 테스트를 진행해주셨습니다.
• Gezine: 취약점을 개발하며 제가 궁금했던 부분이나 잘못된 부분을 답변/지적 해주셨습니다.
• Sajjad: Dr.Yenyen님과 함께 많은 테스트를 진행해주셨습니다.
• cow: 직접 파일 대조까지 해주시며 문제가 되는 부분을 고쳐주셨습니다.
• earthonion: 테스트를 진행해주셨으며 많은 조언을 해주셨습니다.

긴 글 읽어주셔서 감사합니다.

Claude API의 Request는 크게 4가지 분류를 가지고 있다.

• System Messages
• Messages
• Tools
• Model & Config

각각은 다음과 같은 역할을 한다.

System Messages

System Messages는 Claude에게 역할, 성격, 제약사항 등을 지시하는 최상위 설정이다. 배열 형태로 여러 개의 시스템 메시지를 전달할 수 있다.

"system": [
  {
    "type": "text",
    "text": "You are Claude Code, Anthropic's official CLI for Claude.",
    "cache_control": {
      "type": "ephemeral"
    }
  },
  {
    "type": "text",
    "text": "You are an interactive CLI tool that helps users with software engineering tasks...",
    "cache_control": {
      "type": "ephemeral"
    }
  }
]

System Messages에는 다음과 같은 내용이 포함된다:

• Claude의 페르소나 및 역할 정의
• 보안 및 윤리 가이드라인
• 응답 형식 및 톤 설정
• 프로젝트 정보 등 컨텍스트
• cache_control을 통한 캐싱 설정

Messages

Messages는 user와 assistant 역할이 번갈아가며 주고받은 대화를 누적하는 배열이다. assistant 메시지는 반드시 모델의 실제 응답일 필요가 없다. 이를 활요해 API 호출 시 assistant 메시지를 미리 작성해서 전달하면, Claude는 그 내용 이후부터 이어서 응답한다. 이를 Prefill 기법이라 한다.

이 대화 기록을 통해 Claude는 맥락을 유지하며 응답한다.

"messages": [
  {
    "role": "user",
    "content": [...]
  },
  {
    "role": "assistant",
    "content": [...]
  },
  {
    "role": "user",
    "content": [...]
  }
]

User Message

User의 content는 주로 두 가지 type으로 구성된다:

1. text - 사용자의 일반 메시지나 시스템 리마인더

{
  "role": "user",
  "content": [
    {
      "type": "text",
      "text": "선물을 주고받는 기능을 위한 entity를 설계하라."
    }
  ]
}

2. tool_result - Tool 실행 결과 반환

{
  "role": "user",
  "content": [
    {
      "tool_use_id": "toolu_01Qj7gnFLKWBNjg",
      "type": "tool_result",
      "content": [
        {
          "type": "text",
          "text": "## Entity 구조 탐색 보고서\n\n철저한 탐색을 통해..."
        }
      ]
    }
  ]
}

Assistant Message

Assistant의 content는 주로 세 가지 type으로 구성된다:

1. text - Claude의 응답 메시지

{
  "type": "text",
  "text": "선물 주고받기 기능을 위한 entity 설계를 시작하겠습니다."
}

2. thinking - Extended Thinking 기능 활성화 시 사고 과정 (signature로 검증)

{
  "type": "thinking",
  "thinking": "사용자가 선물을 주고받는 기능을 위한 entity 설계를 요청했습니다...",
  "signature": "EqskYIChgCKknyFYp5cu1zhVOp7kFTJb..."
}

3. tool_use - Tool 호출 요청

{
  "type": "tool_use",
  "id": "toolu_01Qj7gn6vLKCNjg",
  "name": "Task",
  "input": {
    "subagent_type": "Explore",
    "prompt": "이 NestJS TypeScript 프로젝트에서 entity 구조를 탐색해주세요...",
    "description": "Entity 구조 탐색"
  }
}

User와 Assistant의 협력

Tool 사용 흐름은 다음과 같이 진행된다:

1. Assistant: tool_use로 Tool 호출 요청
2. User: tool_result로 실행 결과 반환
3. Assistant: 결과를 바탕으로 text 응답 또는 추가 tool_use

이 과정에서 어떤 Tool을 사용할 수 있는지는 tools 배열이 정의한다.

Tools

Tools는 Claude가 사용할 수 있는 도구들을 정의하는 배열이다. 각 Tool은 name, description, input_schema 세 가지 필드로 구성된다.

Tool의 기본 구조

"tools": [
  {
    "name": "ToolName",
    "description": "Tool에 대한 설명...",
    "input_schema": {
      "type": "object",
      "properties": {...},
      "required": [...],
      "additionalProperties": false,
      "$schema": "http://json-schema.org/draft-07/schema#"
    }
  }
]

필드	설명
name	Tool의 고유 식별자. Claude가 tool_use에서 이 이름으로 호출
description	Tool의 용도, 사용법, 주의사항 등을 상세히 기술. Claude가 어떤 Tool을 선택할지 판단하는 근거
input_schema	JSON Schema 형식으로 입력 파라미터 정의

input_schema 구조

input_schema는 JSON Schema draft-07 스펙을 따르며, Tool 호출 시 필요한 파라미터를 정의한다.

"input_schema": {
  "type": "object",
  "properties": {
    "pattern": {
      "type": "string",
      "description": "The regular expression pattern to search for"
    },
    "path": {
      "type": "string",
      "description": "File or directory to search in. Defaults to current working directory."
    },
    "output_mode": {
      "type": "string",
      "enum": ["content", "files_with_matches", "count"],
      "description": "Output mode: 'content' shows matching lines, 'files_with_matches' shows file paths..."
    },
    "-i": {
      "type": "boolean",
      "description": "Case insensitive search"
    },
    "head_limit": {
      "type": "number",
      "description": "Limit output to first N lines/entries"
    }
  },
  "required": ["pattern"],
  "additionalProperties": false,
  "$schema": "http://json-schema.org/draft-07/schema#"
}

properties 내 각 파라미터 정의

각 파라미터는 다음 필드들로 정의된다:

필드	설명
type	데이터 타입 (string, number, boolean, array, object 등)
description	파라미터의 용도와 사용법 설명
enum	(선택) 허용되는 값의 목록. 이 중 하나만 선택 가능
default	(선택) 기본값

input_schema의 메타 필드

필드	설명
type	항상 "object"
properties	파라미터 정의 객체
required	필수 파라미터 이름 배열. 여기 포함되지 않은 파라미터는 선택적
additionalProperties	false면 정의되지 않은 파라미터 전달 불가
$schema	JSON Schema 버전 명시

실제 예시: Grep Tool

{
  "name": "Grep",
  "description": "A powerful search tool built on ripgrep\n\n  Usage:\n  - ALWAYS use Grep for search tasks...",
  "input_schema": {
    "type": "object",
    "properties": {
      "pattern": {
        "type": "string",
        "description": "The regular expression pattern to search for in file contents"
      },
      "path": {
        "type": "string",
        "description": "File or directory to search in (rg PATH). Defaults to current working directory."
      },
      "glob": {
        "type": "string",
        "description": "Glob pattern to filter files (e.g. \"*.js\", \"*.{ts,tsx}\")"
      },
      "output_mode": {
        "type": "string",
        "enum": ["content", "files_with_matches", "count"],
        "description": "Output mode. Defaults to 'files_with_matches'."
      },
      "-A": {
        "type": "number",
        "description": "Number of lines to show after each match"
      },
      "-B": {
        "type": "number",
        "description": "Number of lines to show before each match"
      },
      "-i": {
        "type": "boolean",
        "description": "Case insensitive search"
      },
      "multiline": {
        "type": "boolean",
        "description": "Enable multiline mode. Default: false."
      }
    },
    "required": ["pattern"],
    "additionalProperties": false,
    "$schema": "http://json-schema.org/draft-07/schema#"
  }
}

이 Tool을 Claude가 호출할 때의 tool_use:

{
  "type": "tool_use",
  "id": "toolu_01ABC123",
  "name": "Grep",
  "input": {
    "pattern": "class.*Entity",
    "path": "src/modules",
    "glob": "*.ts",
    "output_mode": "content",
    "-i": true
  }
}

required에 pattern만 있으므로 나머지는 선택적이다. Claude는 input_schema의 description을 참고하여 적절한 파라미터를 선택한다.

Model & Config

마지막으로 모델 선택과 각종 설정 옵션들이다:

{
  "model": "claude-opus-4-5-20251101",
  "max_tokens": 32000,
  "thinking": {
    "budget_tokens": 31999,
    "type": "enabled"
  },
  "stream": true,
  "metadata": {
    "user_id": "user_2f2ce5dbb94ac27c8da0d0b28dddf815fc82be54e0..."
  }
}

옵션	설명
model	사용할 Claude 모델 (claude-opus-4-5, claude-sonnet-4-5 등)
max_tokens	최대 출력 토큰 수
thinking	Extended Thinking 설정 (budget_tokens로 사고 토큰 예산 설정)
stream	스트리밍 응답 여부
metadata	사용자 ID 등 메타데이터

마치며

지금까지 Claude API Request Body의 4가지 핵심 구성 요소를 살펴보았다:

1. System Messages: Claude의 역할과 행동 방식을 정의
2. Messages: user-assistant 간 대화 기록을 누적하며, tool_use/tool_result를 통해 Tool과 상호작용
3. Tools: JSON Schema 기반으로 사용 가능한 도구의 이름, 설명, 입력 파라미터를 정의
4. Model & Config: 모델 선택, 토큰 제한, 스트리밍 등 설정

이 구조를 알면 Claude가 주고받은 메시지를 어떻게 관리하는지, 도구를 어떻게 사용하는지 이해하고 API를 더 효과적으로 활용할 수 있다.