자바 바이트코드의 검증을 위한 프레임워크 설계
A Design of Verification Framework for Java Bytecode
0
조회
0
다운로드
2
인용
0
참고문헌
키워드
초록
Java bytecode verification is a critical process to guarantee the safety of transmitted Java applet on the web or contemporary embedded devices. We propose a design of framework which enables to analyze and verify java bytecode. The designed framework translates from a java bytecode into the intermediate representation which can specify a properties of program without using an operand stack. Using the framework is able to produce automatically error specifications that could be occurred in a program and express specifications annotated in intermediate representation by a user. Furthermore we design a verification condition generator which converts from an intermediate representation to a verification condition, a verification engine which verifies verification conditions from verification condition generator, and a result reporter which displays results of verification.
Abstract
Java bytecode verification is a critical process to guarantee the safety of transmitted Java applet on the web or contemporary embedded devices. We propose a design of framework which enables to analyze and verify java bytecode. The designed framework translates from a java bytecode into the intermediate representation which can specify a properties of program without using an operand stack. Using the framework is able to produce automatically error specifications that could be occurred in a program and express specifications annotated in intermediate representation by a user. Furthermore we design a verification condition generator which converts from an intermediate representation to a verification condition, a verification engine which verifies verification conditions from verification condition generator, and a result reporter which displays results of verification.
참고문헌 (19)
- James, P. R, "ESC4: a modern caching ESC for Java", Proceedings of the 8th international workshop on Specification and verification of component-based systems (SAVCBS '09), pp.19~26 (2009), ACM
- Spoto, F, "Julia: A Generic Static Analyser for the Java Bytecode", In Proc. of the 7th Workshop on Formal Techniques for Java-like Programs, FTfJP'2005 (2005)
- Necula, G. C, "Proof-carrying code", In Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '97), pp.106~119, ACM
- Gary T. Leavens, "Tutorial on JML, the java modeling language", In Proceedings of the twenty-second IEEE, 2007, 573~573
- Barthe, G, "JACK: a tool for validation of security and behaviour of Java applications", In Proceedings of the 5th international conference on Formal methods for components and objects (FMCO'06), pp.152~174 (2007), Springer-Verlag
- Barnett, M, "The Spec# Programming System: Challenges and Directions, In Verified Software: Theories, Tools, Experiments, Lecture Notes In Computer Science, Vol. 4171", pp.144~152 (2005), Springer-Verlag
- BoogiePL: A typed procedural language for checking object-oriented programs, "eLine, R", ~, pp.MSR-TR-2005-70 (2005)
- De Moura, L, "Z3: an efficient SMT solver", Proceedings of the Theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems (2008)
- Ahrendt, W, "KeY: a formal method for object-oriented systems", In Proceedings of the 9th IFIP WG 6. 1 international conference on Formal methods for open object-based distributed systems (FMOODS'07), pp.32~43 (2007)
- BoogiePL: A typed procedural language for checking object-oriented programs, "DeLine, R", ~, pp.MSR-TR-2005-70 (2005)
- Aydemir, B., "Nominal Reasoning Techniques in Coq", Electronic Notes in Theoretical Computer Science, 174(5), pp.69~77 (2007)
- Graf, S, "Construction of Abstract State Graphs with PVS", Proceedings of the 9th International Conference on Computer Aided Verification, pp.72~83 (1997)
- Nipkow, T., "Isabelle", HOL, 2002, pp.2283, ~
- Dijkstra, E. W, "Guarded commands, nondeterminacy and formal derivation of programs", Communications of the ACM, 18(8), pp.453~457 (1975)
- Barnett, M, "Weakest-precondition of unstructured programs", Proceedings of the 6th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering (2005)
- Barrett, C, "CVC3", Proceedings of the 19th international conference on Computer aided verification (2007)
- The yices smt solver, "Dutertre, B", ~ (2006)
- 성중안, "정보보호 기능구조 아키텍쳐 설계방법", (사)디지털산업정보학회 논문지, 3(4), pp.65~73 (2007), (사)디지털산업정보학회
- 김제민, "Mini x86 어셈블리어에서 보안 정보 흐름 분석", (사)디지털산업정보학회 논문지, 5(3), pp.87~98 (2009), (사)디지털산업정보학회