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 条
  • [41] A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq
    van der Weegen, Eelis
    McKinna, James
    TYPES FOR PROOFS AND PROGRAMS, 2009, 5497 : 256 - 271
  • [42] Machine-checked proofs of privacy against malicious boards for Selene & Co
    Dragan, Constantin Catalin
    Dupressoir, Francois
    Estaji, Ehsan
    Gjosteen, Kristian
    HAines, Thomas
    Ryan, Peter Y. A.
    Ronne, Peter B.
    Solberg, Morten Rotvold
    JOURNAL OF COMPUTER SECURITY, 2023, 31 (05) : 469 - 499
  • [43] Source-free, Machine-checked Validation of Native Code in Coq
    Hamlen, Kevin W.
    Fisher, Dakota
    Lundquist, Gilmore R.
    FEAST'19: PROCEEDINGS OF THE 3RD ACM WORKSHOP ON FORMING AN ECOSYSTEM AROUND SOFTWARE TRANSFORMATION, 2019, : 25 - 30
  • [44] Machine-Checked Interpolation Theorems for Substructural Logics Using Display Calculi
    Dawson, Jeremy E.
    Brotherston, James
    Gore, Rajeev
    AUTOMATED REASONING (IJCAR 2016), 2016, 9706 : 452 - 468
  • [45] The research of Dalvik virtual machine on the Andriod platform
    Li, Tingshun
    Jing, Shugang
    Xu, Jiaohui
    Cheng, Yongqiang
    AUTOMATION EQUIPMENT AND SYSTEMS, PTS 1-4, 2012, 468-471 : 2534 - 2537
  • [46] Machine-Checked Natural Semantics for Core Erlang: Exceptions and Side Effects
    Bereczky, Peter
    Horpacsi, Daniel
    Thompson, Simon J.
    PROCEEDINGS OF THE 19TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON ERLANG, ERLANG 2020, 2020, : 1 - 13
  • [47] Strong Invariants for the Efficient Construction of Machine-Checked Protocol Security Proofs
    Meier, Simon
    Cremers, Cas
    Basin, David
    2010 23RD IEEE COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2010, : 231 - 245
  • [48] A machine-checked proof of the optimality of a real-time scheduling policy
    Wilding, M
    COMPUTER AIDED VERIFICATION, 1998, 1427 : 369 - 378
  • [49] A High-Assurance Evaluator for Machine-Checked Secure Multiparty Computation
    Eldefrawy, Karim
    Pereira, Vitor
    PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19), 2019, : 851 - 868
  • [50] Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co
    Dragan, Constantin Catalin
    Dupressoir, Francois
    Estaji, Ehsan
    Gjosteen, Kristian
    Haines, Thomas
    Ryan, Peter Y. A.
    Ronne, Peter B.
    Solberg, Morten Rotvold
    2022 IEEE 35TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2022), 2022, : 335 - 347
12345