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 条
  • [31] Trusted code execution in Java']JavaCard
    Mana, Antonio
    Munoz, Antonio
    TRUST, PRIVACY AND SECURITY IN DIGITAL BUSINESS, PROCEEDINGS, 2007, 4657 : 269 - +
  • [32] Privacy requirements implemented with a Java']JavaCard
    el Kalam, AA
    Deswarte, Y
    21ST ANNUAL COMPUTER SECURITY APPLICATIONS CONFERENCE, PROCEEDINGS, 2005, : 479 - 488
  • [33] KST: Executable Formal Semantics of IEC 61131-3 Structured Text for Verification
    Huang, Yanhong
    Bu, Xiangxing
    Zhu, Gang
    Ye, Xin
    Zhu, Xiaoran
    Shi, Jianqi
    IEEE ACCESS, 2019, 7 : 14593 - 14602
  • [34] Java']Java and beyond: Executable content
    Srinivas, K
    Jagannathan, V
    Reddy, RVR
    Karinthi, R
    COMPUTER, 1997, 30 (06) : 49 - 52
  • [35] The KRAKATOA tool for certification of JAVA']JAVA/JAVA']JAVACARD programs annotated in JML
    Marché, C
    Paulin-Mohring, C
    Urbain, X
    JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2004, 58 (1-2): : 89 - 106
  • [36] Towards a full formal specification of the javacard API
    Computing Science Institute, University of Nijmegen, Toernooiveld 1, ED, Nijmegen, Netherlands
    Lect. Notes Comput. Sci., (165-178):
  • [37] An Executable and Testable Semantics for iTasks
    Koopman, Pieter
    Plasmeijer, Rinus
    Achten, Peter
    IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES, 2011, 5836 : 212 - 232
  • [38] Qualified Electronic Signature via SIM Card Using Java']JavaCard 3 Connected Edition Platform
    Breier, Jakub
    Pomothy, Adam
    2014 NINTH INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY AND SECURITY (ARES), 2015, : 349 - 355
  • [39] ExAIS: Executable AI Semantics
    Schutni, Richard
    Sun, Jun
    2022 ACM/IEEE 44TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2022), 2022, : 859 - 870
  • [40] EXECUTABLE SPECIFICATION OF STATIC SEMANTICS
    DESPEYROUX, T
    LECTURE NOTES IN COMPUTER SCIENCE, 1984, 173 : 215 - 233
12345