A Dynamic Operational Semantics for JVML

Nadia Belblidia and Mourad Debbabi
Computer Security Laboratory, Concordia Institute for Information Systems Engineering, Concordia University, Montreal, Quebec, Canada.

REFEREED
ARTICLE

PDF Version

Abstract

In this paper¹, we present a dynamic semantics for the Java Virtual Machine Language (JVML). The semantics is specified in an operational style according to the syntactic structure of JVML programs. In order to ascribe meanings to threading, the semantics is made small-step and is structured in two layers: The first layer consists of judgements that capture the semantics of sequential JVML programs in isolation. The second layer consists of judgements that capture the parallel execution of JVML threads. The semantics presented in this paper is a faithful and formal transcription of JVML specification as described in [1]. Besides, we provide full account details for the most technical and tricky aspects of JVML such as multi-threading, synchronization, method invocations, exception handling, object creation, object’s fields manipulation, stack manipulation, local variable access, modifiers, etc. The presented semantics is, to the best of our knowledge, the first dynamic semantics of JVML that provides semantics for that many features within the same framework.

Footnote

¹ For static loading it is buildtime that happens immediately, and runtime that is subsequent.

Note: Due to the typographical sophistication of this article, no HTML version is available. Please use the PDF version.

About the authors

		Nadia Belblidia is a Ph.D. student at Concordia Institute for Information Systems Engineering (CIISE), Concordia University, Montreal, Quebec, Canada. She is a member of the Computer Security Laboratory (CSL) at CIISE. She is pursuing a Ph.D. thesis on an aspect oriented approach for security hardening. She can be reached at na_bel@ece.concordia.ca.
		Mourad Debbabi is a Full Professor and the Associate Director of the Concordia Institute for Information Systems Engineering at Concordia University. He is also a Concordia Research Chair Tier I in Information Systems Security. He holds Ph.D. and M.Sc. degrees in computer science from Paris-XI Orsay, University, France. He published more than 100 research papers in international journals and conferences on computer security, formal semantics, mobile and embedded platforms, Java technology security and acceleration, cryptographic protocol specification, design and analysis, malicious code detection, programming languages, type theory and specification and verification of safety-critical systems. In the past, he served as Senior Scientist at the Panasonic Information and Network Technologies Laboratory, Princeton, New Jersey, USA; Associate Professor at the Computer Science Department of Laval University, Quebec, Canada; Senior Scientist at General Electric Corporate Research Center, New York, USA; Research Associate at the Computer Science Department of Stanford University, California, USA; and Permanent Researcher at the Bull Corporate Research Center, Paris, France. Nowadays, he is leading two major projects on cyber forensics and open source security.

Cite this article as follows:Nadia Belblidia and Mourad Debbabi: "A Dynamic Operational Semantics for JVML", in Journal of Object Technology, vol. 6, no. 3, March-February 2007, pp. 71-100 http://www.jot.fm/issues/issue_2007_03/article2