자바 네이티브 인터페이스(Java Native Interface, JNI)는 자바 애플리케이션이 네이티브 라이브러리에 접근할 수 있는 방법을 제공하지만, 올바른 JNI 프로그램을 개발하는 것은 어렵다. 네이티브 코드를 활용함으로써 JNI는 자바 개발자가 효율적인 애플리케이션을 구현하고 C 및 C++와 같은 다른 프로그래밍 언어로 작성된 코드를 재사용할 수 있게 한다. 또한 핵심 자바 라이브러리는 이미 그래픽 사용자 인터페이스와 같은 시스템 기능을 제공하기 위해 JNI를 사용한다. 그 결과, 많은 주류 자바 가상 머신(Java Virtual Machine, JVM)들이 JNI를 지원한다. 그러나 서로 다른 프로그래밍 언어 간의 복잡한 상호운용 의미론 때문에 올바른 JNI 프로그램을 구현하는 것은 간단하지 않다. 더 나아가 성능 오버헤드로 인해 JVM은 기본적으로 잘못된 JNI 상호운용을 검증하지 않으며, -Xcheck:jni 옵션과 디버그 기능이 활성화될 때에만 이를 검증한다. 따라서 JNI 프로그램의 정확성은 JVM의 -Xcheck:jni 옵션에 의해 제공되는 점검에 크게 의존한다. 다만, 해당 기능이 제공하는 점검의 품질에 대해서는 여전히 의문이 남아 있다. -Xcheck:jni 옵션이 검증하지 못하는 성질(properties)이 존재하는가? 그렇다면, 그러한 검증 부재로 인해 어떤 잠재적 문제가 발생할 수 있는가? 우리가 아는 한, 이러한 질문을 심도 있게 탐구한 연구는 없다. 본 논문에서는 JNI 명세에서의 특정 코너 케이스(corner cases)로 설명되지 않은(unspecified) 경우를 사용하여, 주류 JVM에서 -Xcheck:jni 옵션의 검증 품질과 그 영향력을 경험적으로 연구한다. 명세에서 정의되지 않은 이러한 경우는 그 의미론이 명세에 규정되어 있지 않기 때문에 예기치 않은 런타임 동작을 초래할 수 있다. 체계적인 연구를 위해, 우리는 JUSTGEN이라는 반자동 접근법을 제안하여 명세로부터 미정의(unspecified) 경우를 식별하고 테스트 프로그램을 생성한다. JUSTGEN은 도메인 특화 언어(domain specific language, DSL)로 작성된 JNI 명세를 입력으로 받아 SMT 솔버를 사용하여 미정의 경우를 자동으로 탐색한다. 이어서 미정의 경우의 동작을 유발하는 테스트 프로그램을 생성한다. 생성된 테스트를 사용하여 -Xcheck:jni 옵션의 검증 능력을 경험적으로 평가한다. 실험 결과, JNI 디버그 기능은 JVM에서 수천 개의 미정의(unspecified) 경우를 검증하지 못하며, 그로 인해 자바 타입 시스템 위반과 메모리 손상과 같은 치명적인 런타임 오류가 발생할 수 있음을 보여준다. 우리는 해당 JVM 벤더에 보고되지 않은(unvalidated) 792개의 미정의 사례를 보고하였다. 그중 563개 사례는 수정되었고, 나머지 사례는 가까운 시일 내에 수정될 예정이다. 본 경험적 연구를 바탕으로, JNI 명세는 누락된 경우들의 의미론을 명확히 규정해야 하며, 디버그 기능은 완전하게 지원되어야 한다고 믿는다.

*본 초록은 AI를 통해 원문을 번역한 내용입니다. 정확한 내용은 하기 원문에서 확인해주세요.