PCC 기반안드로이드앱 신뢰성검증시스템개발 과제완료보고 김진영, 윤용호, 이광근 서울대학교 컴퓨터공학부프로그래밍연구실 SW 무결점연구센터 ( 연구재단선도연구센터 ) 12/15/2011 @ 삼성전자
목표 안드로이드앱신뢰성자동검증시스템 동기 : 안드로이드앱안심마켓 / 생태계구축 기술 : 정적분석 (static analysis) 기술
앱신뢰성문제 (1/2) 안드로이드앱의개인정보누출
앱신뢰성문제 (2/2) 현재는권한명시방식각앱이필요한권한을요청하도록믿고쓰거나, 아니면설치하지않거나문제는인플레 : 과도한권한명시 효력상실정교하지않음 : 실제로어떤정보에접근했는가? 읽기만? 아니면, 누출까지? 민감한정보누출이발생할수있는지를미리분석하면해결
챌린지 실행복잡도의 실제 난독화된 소스 앱 기계어 Dalvik 김진영, 윤용호, 이광근 ScanDal : 안드로이드 앱 신뢰성 검증 시스템
Project ScanDal 기반이론 : 요약해석 (abstract interpretation) 강력 : any property + any language 엔지니어링실제노하우 : 분석비용 vs 분석정확도의발란스앱기계어 (Dalvik) 대상 (not Java, not C)
추적하는민감한정보의흐름경로 민감한정보들은전화번호부, 문자메시지위치정보사진, 영상기기고유번호 (IMEI) 새어나가는구멍은인터넷 URL에담아서서버로직접문자메시지로
ScanDal 성능 앱이름 코드 분석 메모리 검출된 크기 시간 소모 개인정보 (KB) ( 초 ) (MB) 누출상황 Kids Preschool Puzzle 87 6 67 위치정보 Flurry Job Search 167 6 121 위치정보 서버 Kids Shapes 225 9 164 위치정보 Flurry Kids ABC Phonics 134 12 77 위치정보 Flurry Backgrounds HD Wallpapers 109 17 143 기기고유번호 서버 Bible Quotes 138 36 278 위치정보 AdSense ES Task Manager 158 86 433 위치정보 AdSense Multi Touch Paint 198 174 740 위치정보 AdMob Adao File Manager 255 220 1160 위치정보 AdMob (D-Day) The Day Before 293 626 2761 위치정보 AdMob 프리즘 FreeSMS 387 708 1249 휴대폰번호 서버 Shot Gun Free* 95 36 164 위치정보, 휴대폰번호, 기기고유번호 악성서버 Baseball Superstars 2010* 165 61 285 위치정보, 휴대폰번호, 기기고유번호 악성서버 Monkey Jump 2* 169 74 442 위치정보, 휴대폰번호, 기기고유번호 악성서버 Gold Miner* 191 81 481 위치정보, 휴대폰번호, 기기고유번호 악성서버 Mini Army* 480 174 1292 위치정보, 휴대폰번호, 기기고유번호 악성서버 Xing Metro* 253 23049 1784 위치정보, 휴대폰번호, 기기고유번호 악성서버 공식마켓의인기무료앱 + 비공식마켓의변조된앱 * 그중민감한정보의누출이검출된앱민감한정보가흘러나가는곳 AdMob, AdSense : 광고모듈서버 Flurry : 앱사용행태분석모듈서버
민감한정보누출의예 (1/5) 앱 : Google Wallpaper 4.2.2
민감한정보누출의예 (2/5) 앱 : Google Wallpaper 4.2.2
민감한정보누출의예 (3/5) 앱 : Google Wallpaper 4.2.2
민감한정보누출의예 (4/5) 앱 : Google Wallpaper 4.2.2
민감한정보누출의예 (5/5) 앱 : Google Wallpaper 4.2.2
비공식마켓앱 (1/2) 비공식마켓의변조된앱 apk 파일을손쉽게다운로드가능공식마켓의앱과같은기능민감한정보를몰래수집
비공식마켓앱 (2/2) 변조된앱들게임 (Monkey Jump 2, Gold Miner, Mini Army, Baseball Superstars 2010, Shot Gun Free) 생활앱 (Xing Metro) ScanDal로분석결과공식마켓의앱에서는악성서버로의누출없음비공식마켓의앱에서는악성서버로의누출검출
ScanDal 스텝
Dalvik 언어전처리인프라 앱기계어 Dalvik 220여개의명령어같은일을하는서로다른명령어가많음모두에대한의미정의, 분석기설계는낭비분석용 Dalvik Core 정의 + 번역기구축 12개의명령어로충분데이터접근 : move, istype, new, get, put 흐름제어 : call-direct, call-virtual, return, throw, jmpnz, switch, skip 단, 원래의미를보존하도록 move*, const*, unop*, binop*,... move return v move r r r v ; return
엄밀한디자인 요약해석이론기반 앱기계어 (Dalvik) 대상
Dalvik 프로그램정적분석을 어렵게하는특성들과 ScanDal 의대응
Dynamic Method Dispatches 객체지향프로그램 (OOP) 의핵심타입의상속을활용 (Subtype Systems) 타입에따라다른메소드호출우리의분석기는타입정보도분석에포함실제로일어나지않는호출을안전하게제거
Listeners Java 의콜백메소드 (callbacks) 시스템이호출하는메소드 프로그램코드에선직접호출되지않는프로그램외부와의상호작용을담당 우리의분석기는 유저의입력 ( 화면터치, 버튼, 위치변화 ) OS 의상태변화 (WiFi On/Off, 배터리부족 ) Listener 를다루는명령어를핵심언어에추가 Listener 를환경에등록하는 이벤트를기다리다적절한 Listener 를호출하는 이벤트를기다리는명령어를프로그램맨끝에무한루프로
Exceptions Java의예외상황관리방법예외 (Exception) 타입의객체를던짐메소드호출관계와예외객체의타입에따라예외를처리하는부분이달라짐우리의분석기는두가지모두안전하게분석
Reflections 문자열로부터클래스, 객체를만들고함수를호출단순한형태의다단계프로그래밍우리의분석기는대부분의프로그램은 Reflection에문자열상수를이용하므로정확히분석상수가아닌경우도안전하게분석
Libraries Java와 Android의풍부한 Library 개발자에겐편리, 정적분석에는걸림돌무슨일을하는메소드인가? 프로그램코드에는드러나지않는자주쓰이면메소드의실행의미를하드코딩단, 분석하고자하는성질에따라필요한것만자주쓰이지않으면가장안전하게메소드의실행의미를가정하고분석
기술소개 & 기회
정적프로그램분석 (static program analysis) 프로그램의실행성질을실행전에자동으로안전하게어림잡는일반적인방법 응용 : sw 오류검증, sw 관리, sw 테스트, sw 최적화, 등등 다양한레벨 / 목적 / 이름으로존재 : theory pl, se, veri. cmplr 요약해석 abstract interpretation type system, model checking, theorem proving data-flow analysis, etc.
정적프로그램분석 실행전 : 프로그램을실행시키지않고 자동으로 : 프로그램이프로그램을분석 안전하게 : 모든가능성을포섭 어림잡는 : 실제이외의것들이포함됨어림잡지않으면불가능 일반적 : 소스언어와성질에무제한 C, Java, ML, Bluespec, Dalvik, x86, binary, etc. buffer overrun?, memory leak?, unhandled exn? x=y at line 2?, memory use 2K?, terminate?, race? etc. One-on-One : 분석기1개당, 1언어 1성질.
모든정적분석은 3 스텝 1. 연립방정식 을세운다요약된세계에서 (abstract semantic domains) 프로그램의실행다이나믹스에관한 (abstract execution flows) 2. 그방정식을푼다 3. 그해를가지고결론을내린다있는가없는가? 같은가다른가?
다른분야와다르지않은 소프트웨어 기계공학 프로그램 기계디자인 실행 = 컴퓨터 ( 언어정의 ) 작동 = 자연 ( 자연법칙 ) 실행에대한방정식 작동에대한방정식 방정식풀기 방정식풀기 생각대로돌것이다 생각대로작동할것이다 무인비행기에심자 만들어팔자 PL & Logic 이론 물리-화학법칙, XX방정식
기술위치 ( 우물안 )
기술단계 ( 우물밖 )
다시, 목표 안드로이드앱신뢰성자동검증시스템 동기 : 안드로이드앱안심마켓 / 생태계구축 기술 : 정적분석 (static analysis) +α 기술
기회 / 지향 ScanDal/X X = 민감정보누출검증 (ScanDal/privacy) X = 다른악성실행가능성기술 : 정적분석 자동증명기술 Cloud system sw 검증 / 안심생태계공헌 e.g. Xen Hypervisor core 검증기술 : 정적분석 자동증명기술감사합니다