A formal executable semantics of the Java']JavaCard platform

被引：0
|
作者：
Barthe, G [1 ]
Dufay, G
Jakubiec, L
Serpette, B
de Sousa, SM
机构：
[1] INRIA Sophia Antipolis, Sophia Antipolis, France
[2] Univ Aix Marseille 1, Marseille, France
[3] Univ Beira Interior, Covilha, Portugal
来源：
PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS | 2001年 / 2028卷
关键词：
D O I：
暂无
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We present a formal executable specification of two crucial JavaCard platform components, namely the Java Card Virtual Machine (JCVM) and the ByteCode Verifier (BCV). Moreover, we relate both components by giving a proof of correctness of the ByteCode Verifier. Both formalisations and proofs have been machined-checked using the proof assistant Coq.
引用
收藏
页码：302 / 319
页数：18
相关论文
共 50 条
  • [11] Validation of the Java']JavaCard platform with implicit induction techniques
    Barthe, G
    Stratulat, S
    [J]. REWRITING TECNIQUES AND APPLICATIONS, PROCEEDINGS, 2003, 2706 : 337 - 351
  • [12] An executable formal Java']Java Virtual Machine thread model
    Moore, JS
    Porter, GM
    [J]. USENIX ASSOCIATION PROCEEDINGS JAVA(TM) VIRTUAL MACHINE RESEARCH AND TECHNOLOGY SYMPOSIUM, 2001, : 91 - 103
  • [13] Formal semantics of Java']Java expressions and statements
    Zamulin, AV
    [J]. PROGRAMMING AND COMPUTER SOFTWARE, 2003, 29 (05) : 259 - 269
  • [14] Formal Verification of a Java']JavaCard Virtual Machine with Frama-C
    Djoudi, Adel
    Hana, Martin
    Kosmatov, Nikolai
    [J]. FORMAL METHODS, FM 2021, 2021, 13047 : 427 - 444
  • [15] Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny
    Cassez, Franck
    Fuller, Joanne
    Ghale, Milad K.
    Pearce, David J.
    Quiles, Horacio M. A.
    [J]. FORMAL METHODS, FM 2023, 2023, 14000 : 571 - 583
  • [16] Modular, Compositional, and Executable Formal Semantics for LLVM IR
    Zakowski, Yannick
    Beck, Calvin
    Yoon, Irene
    Zaichuk, Ilia
    Zaliva, Vadim
    Zdancewic, Steve
    [J]. PROCEEDINGS OF THE ACM ON PROGRAMMING LANGUAGES-PACMPL, 2021, 5
  • [17] Formal specification and verification of Java']JavaCard's application identifier class
    van den Berg, J
    Jacobs, B
    Poll, E
    [J]. JAVA ON SMART CARDS: PROGRAMMING AND SECURITY, 2001, 2041 : 137 - 150
  • [18] Formal Semantics of Java Expressions and Statements
    A. V. Zamulin
    [J]. Programming and Computer Software, 2003, 29 : 259 - 270
  • [19] Executable requirements specification: Formal semantics of Live Activity Diagrams
    Knicke, Christoph
    Huhn, Michaela
    Lochau, Malte
    [J]. TASE 2008: SECOND IFIP/IEEE INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING, PROCEEDINGS, 2008, : 109 - 112
  • [20] Executable rewriting logic semantics of Orc and formal analysis of Orc programs
    AlTurki, Musab A.
    Meseguer, Jose
    [J]. JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING, 2015, 84 (04) : 505 - 533
12345