장재훈

13 minute read

들어가며

연구실의 지원을 받아 권위있는 프로그래밍 언어 학회인 PLDI 2025에 참석하게 되었다. 나의 첫 국제 학회 참석이고, 첫 프로그래밍 언어 학회 참석이자 다양한 사람들과 처음으로 네트워킹을 하게 되었다. 처음으로 다양한 경험을 한 만큼, 무엇을 경험하고 배웠는지 공유하려고 한다.

PLDI in Seoul
PLDI 2025가 개최된 웨스틴 조선 서울 호텔
서울의 랜드마크, 남산 타워

이번 PLDI는 대한민국 서울에서 개최되었다. 서울에서 열렸기 때문에 다행히 숙소나 교통에 대한 큰 걱정 없이 학회에 온전히 집중할 수 있었다.
PLDI 명찰과 기념품들

등록을 위해 안내데스크에 갔는데, 영어가 들려오기 시작했다. 내가 평생 살아온 대한민국이기에 잠시 잊고 있었지만, 이곳은 권위 있는 국제 학회 PLDI였다. 순간 당황했지만, 다행히 무사히 등록을 마칠 수 있었고, 그제야 “아, 정말 PLDI에 왔구나”라는 실감이 났다.


재미있는 이벤트들

PLMW 멘토링 워크샵
PLMW 멘토링 워크샵

PLMW 멘토링 워크샵은 PL 분야를 공부하는 학생들이 모여 교류하고, 교수님들의 조언을 들으며 어떻게 연구를 해나가야 할지, 또 같은 분야의 다른 학생들은 어떤 주제를 연구하고 있는지를 함께 이야기 나누는 시간이었다.

워크샵에서는 학생들 간의 네트워킹을 돕기 위해 “PL Cards”라는 활동도 준비되어 있었다. 학생들을 조별로 나누고, PL 관련 용어가 적힌 카드를 돌아가며 뽑는다. 카드를 뽑은 사람은 주어진 금지어를 말하지 않고 해당 단어를 설명하고, 다른 조원들이 그 단어를 맞히는 방식이다.

예를 들어 단어로는 “SMT Solver”, “Compiler”, “WebAssembly” 등이 있었고, 금지어 예시로는 “Compiler”가 제시어일 때 “gcc”, “lex” 등이 포함되었다.

PL Cards를 하며 기억에 남는 한 장면은 다음과 같다.

제시어: “버그 (Bugs)”
A: 이것은 작은 동물의 일종이야. (It’s a tiny animal.)
B: 바퀴벌레? (A cockroach?)
A: 좋아, 그 바퀴벌레가 너의 코드에 있으면? (If a cockroach in your code?)
B: 아, 버그! 😁 (Oh, bugs 😁)

이렇게 재미있는 아이스 브레이킹 활동도 하며 자연스럽게 네트워킹을 할 수 있었다. 돌아가며 자기소개를 하는데, 나를 제외한 모든 학생이 박사과정 학생이였다. 알고 보니, 해외에서는 대부분 학사 졸업 후 석박 통합과정으로 진학하는 경우가 많다고 한다. (출처: PLDI에서 만난 한 학생의 설명)

학생들이 연구하는 분야도 다양했다. 컴파일러나 유닛 테스트처럼 비교적 나에게 익숙한 주제를 연구하는 학생도 있었지만, 오토마타(Automata), 정형 검증(Formal Verification) 등 훨씬 더 PL스러운(?) 주제를 다루는 학생들도 많았다.

이런 차이를 직접 보며 내가 정말 PL 학회에 있다는 사실을 실감할 수 있었다. 불과 1년 전만 해도 이런 사람들과 직접 이야기하고 네트워킹할 기회가 생길 거라고는 생각조차 하지 못했다. 하지만 이번 워크샵을 통해 좋은 기회를 얻었고, 나도 이 커뮤니티의 일원이 된 것 같은 뿌듯함과 설렘을 느낄 수 있었다.

BINSEC Tutorial

학회를 구경하며 프로그램들을 살펴보다가, 보안쟁이인 나에게 익숙한 단어가 보였다.
“BINSEC: Adapting Symbolic Execution for Binary-level Security”1

“Symbolic Execution”, “Binary-level Security”라는 단어는 나를 유혹하기에 충분한 단어였다.

BINSEC는 바이너리 수준에서 소프트웨어 보안을 향상시키기 위한 오픈소스 도구 모음이다. 겉실행 (Symbolic Execution), 요약 해석 (Abstract interpretation), 퍼징 (Fuzzing) 등의 최신 분석 기법을 활용해 바이너리 코드를 정밀하게 분석한다.

해당 튜토리얼에서는 겉실행에 대한 설명과 실제 실습 위주로 이뤄졌다.

간단한 예제는 아래와 같다. 아래와 같은 피보나치를 계산하는 함수와 이를 실행하는 바이너리가 있다고 하자.

int fibonacci(int);

이때 인자로 어떤 값이 들어왔을 때 반환값이 무엇일지를 BINSEC 도구를 통해 계산할 수 있다. 다음은 fibonacci 함수의 인자가 5일 때 리턴값을 출력하는 BINSEC 스크립트의 예시이다.

starting from <fibonacci>
rdi := 5
reach <fibonacci> return then print dec rax

x86-64 함수 호출 규약에 따라 첫 번째 인자는 rdi 레지스터에, 반환값은 rax에 저장된다. 이 BINSEC 스크립트는 rdi가 5일 때, rax의 값을 계산한다.

실행 결과는 다음과 같다. fibonacci(5)의 결과가 5임을 확인할 수 있다.

Path 1 reached address 0x40008e (<fibonacci> return) (0 to go)
Value rax<64> : 5

이와 유사하게, rax의 값이 5일 때 그에 대응하는 인자값을 유추할 수도 있다. 자세한 내용은 BINSEC에서 제공하는 친절하고 재미있는 튜토리얼을 참고하길 추천한다.

바이너리 겉실행 자체는 완전히 새로운 기술은 아니지만, BINSEC 도구는 특히 인상 깊었다. 기존에 많이 사용되던 angr에 비해 스크립트 문법이 훨씬 직관적이고 읽기 쉬웠기 때문이다.

새로운 기술을 평가할 때 고려할 요소는 다양하지만, 요즘 들어 특히 중요하게 느끼는 점은 “얼마나 쉽게 사용할 수 있느냐”이다. 아무리 강력한 기술이라도 사용법이 어렵다면 사람들은 사용하지 않게 되고, 결국 잊혀지게 된다. 그런 의미에서 BINSEC의 스크립트는 사용자 친화적으로 잘 설계되어 있으며, 이는 매우 좋은 선택이라고 생각한다. (게다가 OCaml로 구현되었다는 점도 훌륭하다고 생각한다.)


흥미로운 발표들

A Concurrent Approach to String Transformation Synthesis2
이 논문은 문자열 변환 프로그램을 합성할 때, 병렬성을 도입해 성능을 향상시키는 새로운 접근을 제안한다. 문제 해결 과정을 문제 분해기(Deducer), 후보 생성기(Enumerator), 조건 조립기(Case Splitter) 세 가지 모듈로 분리하고, 이들이 비동기 큐를 통해 협업하도록 설계했다. 각 모듈은 독립적으로 동작한다. 문제 분해기는 큰 문제를 작게 분할하고, 후보 생성기는 가능한 함수 조합을 생성하며, 조건 조립기는 분기 조건에 따라 부분 프로그램들을 합성해서 조립한다. 이러한 구조는 기존의 직렬적인 합성 방식보다 훨씬 효율적이며, 실제로 116개의 어려운 문제를 기존 시스템보다 더 빠르게 해결했다.

이 발표가 인상 깊었던 이유는, 도입부 설명만 듣고도 전체적인 아이디어가 자연스럽게 그려졌기 때문이다. 연구 발표에서 중요한 점은 내용의 흐름이 청중에게 예측 가능해야 한다는 것이다. 특히 학회 발표는 시간이 짧기 때문에, 두괄식으로 핵심을 먼저 전달하고, 그 내용을 기반으로 “이 문제는 아마 이렇게 풀었겠구나” 하는 직관적인 추론이 가능해야 좋은 발표라고 생각한다.

이 연구의 핵심은 기존의 직렬적인 프로그램 합성을 병렬적으로 재구성한 점이다. 이 한 문장만으로도, 문제를 여러 작은 문제로 나누고, 각 모듈이 완전히 독립적이진 않더라도 선행 가능한 작업은 먼저 실행하고, 다른 모듈의 결과가 필요할 때는 큐를 통해 비동기적으로 통신했겠다는 구조가 머릿속에 그려졌다.

또한 인상 깊었던 점은, 평가 단계에서 비교군으로 한양대학교 이우석 교수님의 프로그램 합성기 DUET3이 사용되었다는 점이다. 공교롭게도 발표 당시 이우석 교수님이 바로 내 옆자리에 앉아 계셨다. DUET은 2021년에 발표된 연구인데, 4년이 지난 지금도 최신 연구의 비교 대상이 된다는 건 어떤 기분일까 상상해보게 되었다. 물론 자신의 도구보다 더 잘하는 최신 도구를 보면 아쉬울 수도 있겠지만, 동시에 최신 연구가 내 연구를 기반으로 발전하고 있다는 점에서 큰 자부심을 느낄 수도 있을 것이다.

나 역시 언젠가 훌륭한 도구를 만들고 공개해서, 다양한 연구에서 활용되고 비교될 수 있는 날을 떠올리며, 그 목표를 향한 열정이 다시 한번 불타올랐다.


Automated Exploit Generation for Node.js Packages4
Node.js 패키지에 대한 공격 코드 자동 생성 연구 발표

이 논문은 Node.js 패키지의 취약점에 대해 자동으로 실제 공격 코드를 생성하는 도구, Explode.js를 제안한다. Explode.js는 정적 분석을 통해 공격자가 호출할 수 있는 함수들과, execSync, eval과 같은 민감한 함수에 도달할 수 있는 함수 조합을 식별한다. 이 정보를 기반으로 자바스크립트 공격 코드 템플릿을 생성하며, 사용자 입력 등은 빈칸 변수(Symbolic Variable)로 처리된다. 이후 겉실행(Symbolic Execution)을 이용해 실제 경로 조건을 만족하는 구체적인 빈칸 변수를 계산하며 실행 가능한 공격 코드를 완성한다.

이 방식은 명령어 삽입(Command Injection), 프로토타입 오염(Prototype Pollution), 경로 탐색(Path Traversal) 등 복잡한 취약점도 재현 가능하게 하며, 실제로 동작하는 공격 코드를 생성함으로써 거짓 양성(False Positive) 경고 문제를 효과적으로 제거한다. 실험 결과, Explode.js는 실제 Node.js 패키지에서 44개의 제로데이 취약점과 4개의 신규 CVE를 발견하며, 기존 도구보다 우수한 성능을 입증했다.

이 연구는 공격 코드를 자동으로 생성했다는 점에서 매우 인상 깊었다. 다만, 사용자가 사전에 정의한 취약점 유형과 공격 코드 템플릿에 한정되기 때문에, 다양한 케이스로의 확장은 아직 어렵다는 점은 아쉬움으로 남았다. 그럼에도 불구하고 실제로 많은 버그를 찾아내어, 더 안전한 사이버 세상을 만드는 데 기여했다는 점에서 이 연구의 가치는 충분히 높다고 생각한다.

발표 이후에 누군가 “44개의 취약점을 발견했는데 왜 CVE는 4개뿐인가요?”라고 물은 적이 있었다. 이에 발표자는 해당 취약점들을 개발자에게 제보했지만, 받아들여지지 않았다고 답했다. 구체적인 사정은 알 수 없지만, 개발자가 해당 버그를 취약점으로 간주하지 않았거나, 단순히 패키지만 오픈소스로 공개해놓고 유지보수를 하지 않아 응답조차 받지 못한 경우도 있었다고 한다.

이러한 문제는 나 역시 과거에 버그를 제보하면서 직접 겪은 경험이 있다. 내 생각에 많은 개발자들이 제보된 취약점에 쉽게 대응하지 못하는 이유 중 하나는 패치의 부담 때문이다. 취약점을 수정하려면 우선 발생 원인을 정확히 파악해야 하고, 이를 근본적으로 해결할 수 있는 방안을 고민해 신중하게 수정 및 구현해야 한다. 잘못된 패치는 또 다른 버그를 유발할 수 있고, 경우에 따라 오히려 문제가 해결되지 않는 경우도 발생한다.

그래서 나는 앞으로는 자동 패치 생성(Automatic Program Repair)에 대한 연구도 활발해져야 한다고 생각한다. 만약 취약점 제보와 함께 그에 대한 자동 생성된 패치 코드도 함께 제공된다면, 개발자는 새로운 패치를 직접 작성하는 대신 제공된 패치를 검토하는 수준으로 부담을 줄일 수 있을 것이다. 이처럼 개발자와 보안 연구자 간에 상호 배려가 이루어진다면, 더 많은 버그를 더 빠르게 고치고, 결과적으로 더 안전한 소프트웨어 생태계를 만들어갈 수 있지 않을까 생각한다.


RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers5
RefinedProsa는 실시간 시스템에서 사용하는 단순한 스케줄러가 정해진 시간 안에 작업을 끝낼 수 있는지를 코드 수준에서 자동으로 검증해주는 도구다. 특히 인터럽트 없이 동작하는 시스템에서도 외부 타이머 없이 동작하는 경우에도 적용할 수 있다. 이를 위해 C 코드의 동작 흐름을 추적하고 검증하는 RefinedC와, 응답 시간을 수학적으로 분석하는 Prosa를 연결한다. 코드에 실행 위치를 표시하는 함수를 넣고, 각 동작이 언제 실행되고 얼마나 걸리는지 정보를 더해 시간이 포함된 실행 기록을 만든다. 이렇게 얻은 데이터를 바탕으로 Prosa가 모든 작업이 시간 내에 완료되는지 수학적으로 분석해준다. 이 방법을 통해 실제 C 코드 수준에서 실시간성 보장을 기계적으로 증명할 수 있다.

PLDI에 참석하면서 가장 흥미롭게 느낀 분야는 바로 정형 검증이었다. 나는 주로 프로그램 테스팅에 관심이 많다 보니, 정형 검증에 대해서는 개념만 알고 있을 뿐 깊이 있게 다뤄본 적은 없었다. 사실 속으로는 “정형 검증은 전문가의 개입이 많이 필요하고, 증명도 어렵기 때문에 실용적이지 않으며, 연구도 많지 않을 것이다”라는 선입견을 가지고 있었다.

하지만 이번 학회에서 다양한 연구자들이 정형 검증을 주제로 활발히 연구하고, 이를 실제 시스템이나 개발 도구에 적용한 사례들을 발표하는 모습을 보며 내 생각이 다소 편협했음을 깨달았다. 나는 검증이라는 기술이 적용하기 어렵고 비효율적일 수 있다는 단점만 바라보고 있었다. 하지만 그만큼 검증을 통해 100% 보장된 안전성을 얻을 수 있다는 큰 장점은 간과하고 있었던 것이다. 이번 PLDI에서 여러 프로그램 검증 발표를 들으며 내 시야를 넓힐 수 있었다. 그 덕분에 나는 정말로 우물 안 개구리 같은 시선을 갖고 있었구나 하는 자각을 할 수 있었다.


만난 사람들

학회의 꽃은 무엇일까? 최신 연구를 습득하는 것일까? 물론 그것도 중요하다. 하지만 요즘은 대부분의 최신 연구를 인터넷에서 미리 확인해 볼 수 있다.

그렇다면, 직접 학회에 참석해야만 가능한 일은 무엇일까? 바로 네트워킹이다.

이번에 좋은 기회로 PLDI에 참석하게 되었고, 그만큼 최대한 다양한 사람들과 이야기를 나눠보려고 노력했다. 많은 사람들을 만났지만, 그중에서도 특히 기억에 남는 몇몇 사람들과의 일화를 소개하고자 한다.

INRIA Paris의 Xavier Rival 교수님
Xavier 교수님과 나

나의 지도교수님이신 허기홍 교수님께서 조직위원으로 참여하신 SOAP (State Of the Art in Program Analysis) 세션에서, Xavier 교수님께서 기조연설(Keynote)을 발표하셨다.

내가 처음 정적 분석에 대해 관심을 갖고 공부할 때 읽었던 책이 바로 “Introduction to Static Analysis: An Abstract Interpretation Perspective“였다. 그 책의 저자이자 정적 분석 분야의 세계적인 권위자인 Xavier 교수님을 실제로 뵙는 경험은 정말 짜릿하고 감격스러웠다.

1시간 남짓한 발표를 듣고 난 뒤, 이 기회가 아니면 평생 다시 뵐 수 없을지도 모른다는 생각에 용기를 내어 질문을 드리러 찾아갔다. 질문은 평가 벤치마크에 대한 것이었고, 아주 깊은 질문은 아니었지만, 무엇보다도 교수님과 직접 대화를 나눌 수 있었다는 것 자체가 큰 영광이었다. 그리고 실례를 무릅쓰고 인증 사진도 함께 찍었다. 그 사진 한 장만으로도 정적 분석에 대한 내 실력이 조금은 더 성장한 것 같은 기분이 들었다.
이광근 교수님과 저를 찾아보세요

사실, 같은 책의 또 다른 저자이신 이광근 교수님과도 사진을 찍고 싶었지만, 부끄러움에 그러지 못했다. 대신, 지난 2024 한국소프트웨어종합학술대회의 역사워크샵에서 찍은 단체 사진을 첨부하며 아쉬움을 달랜다.


CEA-LIST의 Frédéric Recoules 연구원님
Frédéric 연구원님과 나

사실 BINSEC 도구를 처음 알게 된 건 PLDI가 아니라, 카이스트 전산학부의 초청 강연 안내 메일을 통해서였다. 그 메일을 통해 BINSEC이라는 도구와 이를 개발한 CEA-LIST 연구 그룹에 대해 처음 접했고, 자연스럽게 그들의 연구 주제에 대해서도 관심을 갖게 되었다.

그들의 연구 주제는 내가 평소에도 고민하는 “어떻게 자동으로 버그를 잘 찾을 수 있을지”에 대한 것이였다. (내가 그들의 논문들을 보며 생각한 것이다.) 이번 PLDI에서는 그들에게 직접 이 질문을 던지고 싶어, 학회장 이곳저곳을 둘러보며 튜토리얼 세션에서 봤던 얼굴을 찾아다녔다. 결국 BINSEC 튜토리얼 실습을 진행하시던 Frédéric Recoules 연구원님을 찾아뵐 수 있었다.

“혹시 BINSEC 튜토리얼 워크샵을 진행하지 않으셨나요?”라는 말로 조심스럽게 대화를 시작했고, 도구가 인상 깊었다는 점, 튜토리얼 내용이 정말 유익했다는 점 등 팬심을 가득 담아 전했다.

이후 튜토리얼의 핵심 주제였던 겉실행 (Symbolic Execution)을 시작으로, 자동으로 버그를 잘 찾는 방법에 대해 여러 이야기를 나눴다. 특히 인상 깊었던 대화는 다음과 같았다:

“겉실행이나 퍼징, 정적분석 등 다양한 기술들이 있는데 어떤 기술이 가장 버그를 찾는데 효과적이라고 생각하시나요?”

각 기술마다 분명한 장단점이 있습니다. 정적분석은 안전(Sound)하기 때문에 버그를 놓칠 일은 없지만, 거짓 양성 알람이 너무 많습니다. 반대로 겉실행이나 퍼징은 완전(Complete)하기에 발견된 버그는 확실하지만, 놓치는 버그도 많을 수 있습니다. 그래서 이 각각의 한계를 보완하는 방향으로 연구가 진행되어야 한다고 생각합니다.

이 답변을 들으며, 최근 CEA-LIST에서 발표한 정적 분석 알람의 우선순위를 정하는 연구6가 떠올랐다. 아마도 이런 한계를 극복하려는 시도가 아니었을까 하는 생각이 들었다.

무엇보다도 나와 비슷한 문제의식과 방향성을 가지고 연구하는 사람과 그룹이 있다는 것이 참 신기했고, 또한 내가 가고 있는 연구방향이 틀리지 않았다는 확신도 들었다.


마이크로소프트의 Tahina Ramananandro 연구원님
Tahina 연구원님과 나

PLDI에는 학계뿐만 아니라 산업계에 있는 사람들도 참석한다. 이들은 등록 데스크 옆에 부스를 차려 자사의 기술을 홍보하고 있었는데, 그중 유독 눈에 띄는 기업 부스가 하나 있었다. 대부분의 부스는 책자와 사람만 있었지만, 마이크로소프트 부스는 모니터까지 가져와 자사의 연구를 소개하고 있었다. 어떤 연구인지 몰래 지켜보던 중, 부스에 계시던 Tahina가 손짓하며 이야기를 나누자고 했다. 그렇게 자연스럽게 EverParse7에 대한 설명을 들을 수 있었다.

EverParse는 사용자로부터 메시지 포맷(데이터 타입)에 대한 명세를 입력받아, 이를 기반으로 안전하고 검증된 파서 코드를 자동 생성하는 기술이다. 메시지 파싱 과정에서는 메모리 오버플로우, 길이 필드 미검증 등 다양한 보안 취약점이 발생할 수 있다. 대표적인 사례로, 하트블리드(Heartbleed) 취약점은 TLS 메시지에서 길이 필드 검증이 미흡해 발생한 버퍼 오버플로우로, 수많은 시스템에 영향을 주었다. EverParse는 이러한 문제를 방지하기 위해, 사용자가 C와 유사한 문법으로 작성한 메시지 포맷 명세를 받아 이를 F* 언어로 변환하고, 해당 명세로부터 형식적으로 증명(Formally verified)된 타입 정의와 파서 구현(F* 기반)을 자동 생성한다. 생성된 F* 코드는 메모리 안전성과 같은 속성이 증명되며, 이를 다시 C 코드로 추출함으로써 성능과 보안성을 모두 갖춘 파서 코드를 제공한다.

사실 나는 마이크로소프트가 보안 측면에서 하는 활동이라곤 대규모의 버그 바운티밖에 몰랐다. 자사 제품의 취약점을 제보하면 최대 $100,000까지 보상하는 이 프로그램은, 제품 개발 이후 제3자의 시선으로 버그를 적극적으로 테스트하게 만든다는 점에서 “테스팅” 관점의 접근이다. 반면 EverParse는 “테스팅”이 아니라 “검증”의 관점이다. 이미 만들어진 프로그램의 버그를 찾는 것이 아니라, 처음부터 안전한 프로그램을 만들기 위한 개발 방식이다.

그동안 나는 보안, 특히 취약점 분석이라는 영역에서 “어떻게 하면 버그를 잘 찾을 수 있을까?”에 집중해왔다. 하지만 이는 내가 직접 제품을 만드는 사람이 아니었기에 자연스럽게 가졌던 시선이었다. 이번 경험을 통해 제품을 개발하는 입장에서, 처음부터 안전하게 만드는 방식이 어떻게 구현될 수 있는지 알게 되었고, 견문을 넓힐 수 있었다. 아주 뜻깊은 시간이었다.

이외에도 다양한 연구자들과 교류하며 그들의 연구 분야와 관점을 접할 수 있었고, 덕분에 여러 연구 방향에 대해 다시금 고민해보는 계기가 되었다. 엄청나게 내향적인 사람인 내가 이렇게 네트워킹을 잘(?) 할 수 있었던 이유가 궁금하다면 이 글을 참고하길 바란다.


느낀점들
PLDI에 온 나

영어! 언젠간 잘하고 말 거야
이번 PLDI에서 가장 크게 느낀 점은 “영어를 정말 잘해야겠다”는 것이었다. 사실 한국에서 공부할 때는 영어로 큰 어려움을 느낄 일이 많지 않았다. 영어로 읽고 쓰고 듣는 일은 많지만, 말할 일은 거의 없기 때문이다.

하지만 이번 학회에서는 처음으로, 그것도 일대일이 아닌 다대일 상황에서 영어로 연구 이야기를 나누려다 보니 여간 골치가 아팠다. 네트워킹 중에 내가 궁금한 주제나 하고 싶은 이야기는 미리 준비해 가서 어느 정도 수월했지만, 예상치 못한 질문이나 갑작스러운 대화 요청에는 제대로 대응하기가 어려웠다. 특히 PLMW 멘토링 워크샵에서 조별 활동을 하며 사방에서 쏟아지는 영어 대화에 순간적으로 당황했고, 그때 처음으로 “영어 울렁증”이라는 게 어떤 느낌인지 실감했다.

돌이켜보면, 내가 영어를 좀 더 잘했더라면 훨씬 깊이 있고 다양한 이야기를 나눌 수 있었을 텐데 하는 아쉬움이 컸다. 그래서 이번 PLDI를 계기로 잠시 쉬고 있던 전화 영어를 다시 시작해, 글로벌한 연구자로 한 걸음 더 성장해보고자 한다.

안전한 사이버 세상을 만들기 위해 필요한 것은 무엇일까?
언젠가부터 내 꿈은 안전한 사이버 세상을 만드는 것이었다. 그 방법으로 나는 프로그램의 오류를 잘 찾아내는 일에 주목했다. 이를 위해 고등학생 때는 직접 손으로 오류를 찾는 방법에 대해 공부하고, 대학생 때는 이를 자동으로 찾아보려고 시도해보고, 지금은 이론적 배경을 바탕으로 최신 연구들을 활용해 효율적으로 잘 찾기위해 노력하고 있다.

이번 PLDI에 참석하며 느낀 가장 큰 깨달음은, 이 목표를 이루는 방법이 단순히 테스팅에 국한될 필요는 없다는 것이었다. 예를 들어, 마이크로소프트의 EverParse는 정형 검증을 통해 처음부터 안전한 프로그램을 만드는 방법을 제시하고 있었다.

소프트웨어 개발 전 과정에서 오류를 빠르게 발견할수록 수정 비용이 줄어든다는 것은 널리 알려진 사실이다. 이번 학회에서는 정형 검증에 대한 최신 연구뿐만 아니라, 이러한 기술이 실제 산업계에서도 활발히 활용되고 있다는 점을 직접 확인할 수 있었다. 이 경험을 통해 나 역시 테스팅이라는 한 방법에만 의존하지 말고, 더 다양한 접근을 통해 안전한 사이버 세상을 만드는 데 기여할 방법을 모색해야겠다는 생각을 하게 되었다.

이러한 관심을 토대로 Dafny라는 검증 언어에 대해서 공부해보려고 한다. 직접 프로그램 검증을 경험해본다면, 내 꿈을 위해 나아가야할 방향성과 이를 이루기 위한 방법이 더 다양해지고 구체화될 것이라고 확신한다. 마침 이번 2025년 가을학기에 열리는 CS424: 프로그램 논증 수업에서 이와 관련된 재미있는 과제가 추가된다고 하니, 관심있는 학생들은 수강하길 추천한다.

마치며
PLDI에 온 Prosys 연구실

나는 사람은 새로운 경험을 통해 크게 성장한다고 믿는다. 이번 PLDI는 짧다면 짧은 5일간의 일정이었지만, 그 안에 정말 많은 것을 배우고 경험할 수 있었던 소중한 기회였다. 이러한 기회를 주시고 아낌없이 지원해주신 허기홍 교수님과 학교에 깊이 감사드린다. 본문에는 다 담지 못했지만, PLDI에서 컴파일러 지향성 퍼징8에 대한 멋진 연구를 발표하신 봉준님께도 진심으로 고생 많으셨다고 전하고 싶다. 정말 멋지고 훌륭한 발표였다.

이번 경험을 잊지 않으며, 더 나은 연구자로 성장하기 위해 늘 노력하겠다.

각주

[1] Frédéric Recoules, Sébastien Bardin. “BINSEC: Adapting Symbolic Execution for Binary-level Security” PLDI Workshops and Tutorials (2025)
[2] Yuantian Ding et al. “A Concurrent Approach to String Transformation Synthesis” PLDI (2025)
[3] Woosuk Lee. “Combining the top-down propagation and bottom-up enumeration for inductive program synthesis” POPL (2021)
[4] Filipe Marques et al. “Automated Exploit Generation for Node.js Packages” PLDI (2025)
[5] Kimaya Bedarkar et al. “RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers” PLDI (2025)
[6] Guilhem Lacombe et al. “Attacker Control and Bug Prioritization” USENIX Security (2025)
[7] Tahina Ramananandro et al. “EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats” USENIX Security (2019)
[8] Jaeseong Kwon et al. “Optimization-Directed Fuzzing for Continuous Translation Validation” PLDI (2025)

You May Also Enjoy