Correctness of Java']Java Card method lookup via logical relations

被引：0
|
作者：
Denney, E
Jensen, T
机构：
[1] CNRS, IRISA, F-35042 Rennes, France
[2] Univ Edinburgh, Math Reasoning Grp, Div Informat, Edinburgh EH1 1HN, Midlothian, Scotland
来源：
THEORETICAL COMPUTER SCIENCE | 2002年 / 283卷 / 02期
关键词：
compiler correctness; optimisation; operational semantics; !text type='Java']Java[!/text; smart cards;
D O I：
10.1016/S0304-3975(01)00138-4
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This article presents a formalisation of the bytecode optimisation of Sun's Java Card language from the class file to CAP file format as a set of constraints between the two formats, and defines and proves its correctness. Java Card bytecode is formalised using an abstract operational semantics, which can then be instantiated into the two formats. The optimisation is given as a logical relation such that the instantiated semantics are observably equal. (C) 2002 Elsevier Science B.V. All rights reserved.
引用
收藏
页码：305 / 331
页数：27
相关论文
共 50 条
  • [1] Correctness of Java']Java Card method lookup via logical relations
    Denney, E
    Jensen, T
    [J]. PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2000, 1782 : 104 - 118
  • [2] Guaranteeing Correctness Properties of a Java']Java Card Applet
    Fredlund, Lars-Ake
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 113 : 217 - 233
  • [3] Logical Attacks on Secured Containers of the Java']Java Card Platform
    Volokitin, Sergei
    Poll, Erik
    [J]. SMART CARD RESEARCH AND ADVANCED APPLICATIONS, CARDIS 2016, 2017, 10146 : 122 - 136
  • [4] A constructive approach to correctness, exemplified by a generator for certified Java']Java Card applets
    Coglio, Alessandro
    Green, Cordell
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, EXPERIMENTS, 2008, 4171 : 57 - 63
  • [5] Attacks on Java']Java Card 3.0 Combining Fault and Logical Attacks
    Barbu, Guillaume
    Thiebeauld, Hugues
    Guerin, Vincent
    [J]. SMART CARD RESEARCH AND ADVANCED APPLICATION, PROCEEDINGS, 2010, 6035 : 148 - 163
  • [6] 8-bit Java']Java: the Java']Java card
    Grehan, R
    [J]. COMPUTER DESIGN, 1997, 36 (05): : 80 - 80
  • [7] Formalizing the safety of Java']Java, the Java']Java virtual machine, and Java']Java card
    Hartel, PH
    Moreau, L
    [J]. ACM COMPUTING SURVEYS, 2001, 33 (04) : 517 - 558
  • [8] Automation of Java']Java Card component development using the B method
    Deharbe, David
    Gomes, Bruno Gurgel
    Moreira, Anamaria Martins
    [J]. ICECCS 2006: 11TH IEEE INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS, PROCEEDINGS, 2006, : 259 - +
  • [9] BSmart: A Tool for the Development of Java']Java Card Applications with the B Method
    Deharbe, D.
    Gomes, B. E. G.
    Moreira, A. M.
    [J]. ABSTRACT STATE MACHINES, B AND Z, PROCEEDINGS, 2008, 5238 : 351 - 352
  • [10] Embedded Eavesdropping on Java']Java Card
    Barbu, Guillaume
    Giraud, Christophe
    Guerin, Vincent
    [J]. INFORMATION SECURITY AND PRIVACY RESEARCH, 2012, 376 : 37 - 48
12345