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 条
  • [31] Machine-Checked Proof-Theory for Propositional Modal Logics
    Dawson, Jeremy E.
    Gore, Rajeev
    Wu, Jesse
    ADVANCES IN PROOF THEORY, 2016, 28 : 173 - 243
  • [32] Efficient construction of machine-checked symbolic protocol security proofs
    Meier, Simon
    Cremers, Cas
    Basin, David
    JOURNAL OF COMPUTER SECURITY, 2013, 21 (01) : 41 - 87
  • [33] Machine-checked proofs for electronic voting: privacy and verifiability for Belenios
    Cortier, Veronique
    Dragan, Constantin Catalin
    Dupressoir, Francois
    Warinschi, Bogdan
    IEEE 31ST COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2018), 2018, : 298 - 312
  • [34] Machine-Checked Proofs of Accountability: How to sElect Who is to Blame
    Dragan, Constantin Catalin
    Dupressoir, Francois
    Gjosteen, Kristian
    Haines, Thomas
    Ronne, Peter B.
    Solberg, Morten Rotvold
    COMPUTER SECURITY - ESORICS 2023, PT III, 2024, 14346 : 471 - 491
  • [35] A machine-checked soundness proof for an efficient verification condition generator
    Vogels, Frédéric
    Jacobs, Bart
    Piessens, Frank
    Proceedings of the ACM Symposium on Applied Computing, 2010, : 2517 - 2522
  • [36] A Machine-Checked Proof of Security for AWS Key Management Service
    Almeida, Jose Bacelar
    Barbosa, Manuel
    Barthe, Gilles
    Campagna, Matthew
    Cohen, Ernie
    Gregoire, Benjamin
    Pereira, Vitor
    Portela, Bernardo
    Strub, Pierre-Yves
    Tasiran, Serdar
    PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19), 2019, : 63 - 78
  • [37] On a Machine-Checked Proof for Fraction Arithmetic over a GCD Domain
    Meshveliani, S. D.
    PROGRAMMING AND COMPUTER SOFTWARE, 2020, 46 (02) : 110 - 119
  • [38] On a Machine-Checked Proof for Fraction Arithmetic over a GCD Domain
    S. D. Meshveliani
    Programming and Computer Software, 2020, 46 : 110 - 119
  • [39] A Certificate Infrastructure for Machine-Checked Proofs of Conditional Information Flow
    Amtoft, Torben
    Dodds, Josiah
    Zhang, Zhi
    Appel, Andrew
    Beringer, Lennart
    Hatcliff, John
    Ou, Xinming
    Cousino, Andrew
    PRINCIPLES OF SECURITY AND TRUST, POST 2012, 2012, 7215 : 369 - 389
  • [40] A Provably-Correct Micro-Dalvik Bytecode Verifier
    Jiang Nan
    He Yanxiang
    Zhang Xiaotong
    Liu Rui
    Shen Yunfei
    INTERNATIONAL JOURNAL OF SECURITY AND ITS APPLICATIONS, 2016, 10 (09): : 193 - 210
12345