Abstract
Bytecode verification is a key security function in several architectures for mobile and embedded code, including Java, JavaCard, and .NET. Over the last few years, its formal correctness has been studied extensively by academia and industry, using general purpose theorem provers. Yet a recent roadmap on smartcard research [1], and a recent survey of the field of Java verification [11], point to a severe lack of methodologies, techniques and tools to help such formal endeavours. In earlier work, we have developed, and partly automated, a methodology to establish the correctness of static analyses similar to bytecode verification. The purpose of this paper is to complete the automation process by certifying the different dataflow analyses involved in bytecode verification, using the Coq proof assistant. It enables us to derive automatically, from a reference virtual machine that performs verification at run-time, and satisfies minimal requirements, a provably correct bytecode verifier.
Chapter PDF
References
Roadmap for European Research on Smartcard Technologies. See, http://www.ercim.org/reset
Andronick, J., Chetali, B., Ly, O.: Using Coq to Verify Java Card Applet Isolation Properties. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 335–351. Springer, Heidelberg (2003)
Barthe, G., Courtieu, P., Dufay, G., Melo de Sousa, S.: Tool-Assisted Specification and Verification of the JavaCard Platform. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 41–59. Springer, Heidelberg (2002)
Barthe, G., Dufay, G., Jakubiec, L., Serpette, B., Melo de Sousa, S.: A Formal Executable Semantics of the JavaCard Platform. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 302–319. Springer, Heidelberg (2001)
Betarte, G., Chetali, B., Giménez, E., Loiseaux, C., Ly, O.: Formal Modeling and Verification of the Java Card Security Architecture: from Static Checkings to Embedded Applet Execution. In: Proceedings of ESMART 2002 (2002)
Chrzaszcz, J.: Implementing Modules in the Coq System. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 270–286. Springer, Heidelberg (2003)
Coglio, A.: Simple Verification Technique for Complex Java Bytecode Subroutines. In: Proceedings of FTFJP 2002 (2002)
Coq Development Team. The Coq Proof Assistant User’s Guide. Version 7.4 (February 2003)
Freund, S.N., Mitchell, J.C.: A Type System for the Java Bytecode Language and Verifier. Journal of Automated Reasoning 30(3-4), 271–321 (2003)
Gordon, A.D., Syme, D.: Typing a multi-language intermediate code. In: Proceedings of POPL 2001, pp. 248–260. ACM Press, New York (2001)
Hartel, P., Moreau, L.: Formalizing the Safety of Java, the Java Virtual Machine and Java Card. ACM Computing Surveys 33(4), 517–558 (2001)
Henrio, L., Serpette, B.: A parameterized polyvariant bytecode verifier. In: Filliatre, J.-C. (ed.) Proceedings of JFLA 2003 (2003)
Kildall, G.A.: A unified approach to global program optimization. In: Proceedings of POPL 1973, pp. 194–206. ACM Press, New York (1973)
Klein, G., Nipkow, T.: Verified bytecode verifiers. Theoretical Computer Science 298(3), 583–626 (2002)
Klein, G., Wildmoser, M.: Verified bytecode subroutines. Journal of Automated Reasoning 30(3-4), 363–398 (2003)
Lanet, J.-L., Requet, A.: Formal Proof of Smart Card Applets Correctness. In: Quisquater, J.-J., Schneier, B. (eds.) CARDIS 1998. LNCS, vol. 1820, pp. 85–97. Springer, Heidelberg (2000)
Leroy, X.: Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning 30(3-4), 235–269 (2003)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Rose, E., Rose, K.H.: Lightweight bytecode verification. In: Workshop Formal Underpinnings of the Java Paradigm, OOPSLA 1998 (October 1998)
Shankar, N., Owre, S., Rushby, J.M.: The PVS Proof Checker: A Reference Manual. Computer Science Laboratory, SRI International (February 1993). Supplemented with the PVS2 Quick Reference Manual (1997)
Syme, D., Gordon, A.D.: Automating type soundness proofs via decision procedures and guided reductions. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 418–434. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barthe, G., Dufay, G. (2004). A Tool-Assisted Framework for Certified Bytecode Verification. In: Wermelinger, M., Margaria-Steffen, T. (eds) Fundamental Approaches to Software Engineering. FASE 2004. Lecture Notes in Computer Science, vol 2984. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24721-0_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-24721-0_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21305-5
Online ISBN: 978-3-540-24721-0
eBook Packages: Springer Book Archive