SMT-Solver 를 사용한 자바바이트코드의 배열 오버플로우 검증

홈 > 연구문헌 > 학술대회 프로시딩 > 한국정보처리학회 학술대회 > 2011년 춘계 학술대회

한글제목(Korean Title)	SMT-Solver 를 사용한 자바바이트코드의 배열 오버플로우 검증
영문제목(English Title)	A Verification of Array Overflow in Java Bytecode using SMT-Solver
저자(Author)	이상협 김제민 박준석 유원희 Sanghyup Lee Jemin Kim Joonseok Park Weonhee Yoo
원문수록처(Citation)	VOL 18 NO. 01 PP. 0261 ~ 0264 (2011. 05)
한글내용 (Korean Abstract)	자바프로그램 검증은 안전하고 정확한 프로그램을 만들기 위한 필수적인 조건이지만 자바언어로 작성된 프로그램은 바이트코드로 작성되어 있는 클래스 파일로 배포되기 때문에 바이트코드에 대한 검증이 필요하다. 하지만 자바 바이트코드는 가독성이 떨어져 중간언어로 변환을 하고 그 중간코드에서 검증에 필요한 조건들을 작성 해야 한다. 이 논문에서는 새로 정의된 중간언어인 BIRS을 통해 컴파일시 검증이 되지 않는 배열 오버플로우에 대한 정적검증을 설명하고 검증 절차에 필요한 명제의 정의와 검증 시 사용되는 SMT-Solver 인 Z3 의 사용법에 대하여 서술하였다.
영문내용 (English Abstract)
키워드(Keyword)
파일첨부	PDF 다운로드