요약 Android는 서로 다른 애플리케이션(app)의 활동을 동일한 활동 스택(activity stack) 안에 유지함으로써 원활한 사용자 경험을 지원한다. 이러한 긴밀한 앱 간 통신은 Android 프레임워크에서 필수적이지만, 강력한 앱 간 통신에는 취약점이 존재하며, 그로 인해 악의적인 활동을 피해 앱의 활동 스택에 주입하여 사용자 상호작용 흐름을 가로챌 수 있다. 본 논문에서는 간단한 악성코드를 이용한 활동 주입 공격을 시연하고, 연산 의미론(operational semantics)을 사용하여 활동 활성화 메커니즘을 형식적으로 명세한다. 연산 의미론에 기반하여, Android 앱을 분석하여 활동 주입 공격을 탐지하는 정적 분석 도구를 개발한다. 우리의 도구는 실제 환경의 Android 앱을 평균 6초 내에 분석할 만큼 충분히 빠르며, 실험 결과 129,756개의 실제 Android 앱 중 1761개가 다른 앱의 태스크(tasks)에 자신의 활동을 주입하는 것으로 확인되었다. 또한, signature-based activity access control(SAAC)이라 명명한 방어 메커니즘을 제안하며, 이는 활동 주입 공격을 완전히 차단한다. 해당 방어 메커니즘은 현재의 Android 멀티태스킹 기능을 그대로 유지할 수 있을 만큼 일반적이며, 복잡한 활동 활성화 연산 의미론에 독립적으로 동작할 만큼 충분히 단순하여 활동 활성화 시간을 눈에 띄게 증가시키지 않는다. SAAC에 대한 형식 의미론을 확장함으로써, SAAC이 어떠한 오탐(false alarm)도 없이 활동 주입 공격을 올바르게 완화함을 증명한다.

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