Machine-checked model for Micro-Dalvik virtual machine

被引：0
|
作者：
He, Yan-Xiang [1 ,2 ]
Jiang, Nan [1 ,3 ]
Li, Qing-An [1 ,2 ]
Zhang, Jun [1 ,4 ]
Shen, Fan-Fan [1 ]
机构：
[1] Computer School, Wuhan University, Wuhan,430072, China
[2] State Key Laboratory of Software Engineering, Wuhan University, Wuhan,430072, China
[3] Computer School, Hubei University of Technology, Wuhan,430068, China
[4] Software College, East China Institute of Technology, Nanchang,330013, China
来源：
Ruan Jian Xue Bao/Journal of Software | 2015年 / 26卷 / 02期
关键词：
Computer programming languages - Virtual machine - Theorem proving - Formal specification - Semantics - Network security;
D O I：
10.13328/j.cnki.jos.004787
中图分类号：
学科分类号：
摘要：
This paper introduces Micro-Dalvik, a formalized Dalvik-like VM model to exhibit core features of the register-based architecture. This formal specification describes the instruction set and runtime state, and the runtime behaviors of the instructions as state transitions based on big-step operational semantics. The Micro-Dalvik VM instruction set is more abstract than comparable Dalvik VM to attain clarity of its semantics, but bears no further simplification of the meaning of instructions. Some properties of Micro-Dalvik VM semantics are stated based on this formal specification and sketch of the proofs is provided. This formalization is implemented in the theorem proof assistant Isabelle/HOL. © Copyright 2015, Institute of Software. the Chinese Academy of Sciences, All Rights Reserved.
引用
收藏
页码：364 / 379
相关论文
共 50 条
  • [21] Machine-Checked Sequencer for Critical Embedded Code Generator
    Izerrouken, Nassima
    Pantel, Marc
    Thirioux, Xavier
    FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5885 : 521 - 540
  • [22] Practical Machine-Checked Formalization of Change Impact Analysis
    Palmskog, Karl
    Celik, Ahmet
    Gligoric, Milos
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2020, 2020, 12079 : 137 - 157
  • [23] Automated Machine-Checked Hybrid System Safety Proofs
    Geuvers, Herman
    Koprowski, Adam
    Synek, Dan
    van der Weegen, Eelis
    INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 259 - +
  • [24] Towards a machine-checked Java']Java specification book
    Reus, B
    Hein, T
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 480 - 497
  • [25] Java']Java and the Java']Java Memory Model - A Unified, Machine-Checked Formalisation
    Lochbihler, Andreas
    PROGRAMMING LANGUAGES AND SYSTEMS, 2012, 7211 : 497 - 517
  • [26] Evaluation of Android Dalvik Virtual Machine
    Oh, Hyeong-Seok
    Kim, Beom-Jun
    Choi, Hyung-Kyu
    Moon, Soo-Mook
    PROCEEDINGS OF THE 10TH INTERNATIONAL WORKSHOP ON JAVA TECHNOLOGIES FOR REAL-TIME AND EMBEDDED SYSTEMS, 2012, : 115 - 124
  • [27] A Machine-Checked Direct Proof of the Steiner-Lehmus Theorem
    Kellison, Ariel
    PROCEEDINGS OF THE 11TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS (CPP '22), 2022, : 265 - 273
  • [28] Evaluation of android dalvik virtual machine
    School of Electrical Engineering and Computer Science, Seoul National University, Seoul 151-742, Korea, Republic of
    ACM Int. Conf. Proc. Ser., (115-124):
  • [29] Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS+
    Barbosa, Manuel
    Dupressoir, Francois
    Gregoire, Benjamin
    Hulsing, Andreas
    Meijers, Matthias
    Strub, Pierre-Yves
    ADVANCES IN CRYPTOLOGY - CRYPTO 2023, PT V, 2023, 14085 : 421 - 454
  • [30] WebSpec: Towards Machine-Checked Analysis of Browser Security Mechanisms
    Veronese, Lorenzo
    Farinier, Benjamin
    Bernardo, Pedro
    Tempesta, Mauro
    Squarcina, Marco
    Maffei, Matteo
    2023 IEEE SYMPOSIUM ON SECURITY AND PRIVACY, SP, 2023, : 2761 - 2779
12345