Formalizing the safety of Java']Java, the Java']Java virtual machine, and Java']Java card

被引：34
|
作者：
Hartel, PH
Moreau, L
机构：
[1] Univ Twente, Dept Comp Sci, NL-7500 AE Enschede, Netherlands
[2] Univ Southampton, Dept Elect & Comp Sci, Southampton SO17 1BJ, Hants, England
来源：
ACM COMPUTING SURVEYS | 2001年 / 33卷 / 04期
关键词：
verification; Common criteria; programming;
D O I：
10.1145/503112.503115
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We review the existing literature on Java safety, emphasizing formal approaches, and the impact of Java safety on small footprint devices such as smartcards. The conclusion is that although a lot of good work has been done, a more concerted effort is needed to build a coherent set of machine-readable formal models of the whole of Java and its implementation. This is a formidable task but we believe it is essential to build trust in Java safety, and thence to achieve ITSEC level 6 or Common Criteria level 7 certification for Java programs.
引用
收藏
页码：517 / 558
页数：42
相关论文
共 50 条
  • [1] Implementation of Java']Java Card Virtual Machine
    Liu, SY
    Mao, ZG
    Ye, YZ
    [J]. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY, 2000, 15 (06) : 591 - 596
  • [2] Program analysis for safety guarantees in a Java']Java virtual machine written in Java']Java
    Maessen, JW
    Sarkar, V
    Grove, D
    [J]. ACM SIGPLAN NOTICES, 2001, : 62 - 65
  • [3] Operational semantics of the Java']Java Card Virtual Machine
    Siveroni, IA
    [J]. JOURNAL OF LOGIC AND ALGEBRAIC PROGRAMMING, 2004, 58 (1-2): : 3 - 25
  • [4] Asynchronous Java']Java accelerator for embedded Java']Java virtual machine
    Liang, Z
    Plosila, J
    Sere, K
    [J]. PROCEEDINGS OF THE IEEE 6TH CIRCUITS AND SYSTEMS SYMPOSIUM ON EMERGING TECHNOLOGIES: FRONTIERS OF MOBILE AND WIRELESS COMMUNICATION, VOLS 1 AND 2, 2004, : 253 - 256
  • [5] Preservation of proof obligations from Java']Java to the Java']Java virtual machine
    Barthe, Gilles
    Gregoire, Benjamin
    Pavlova, Mariela
    [J]. AUTOMATED REASONING, PROCEEDINGS, 2008, 5195 : 83 - +
  • [6] 8-bit Java']Java: the Java']Java card
    Grehan, R
    [J]. COMPUTER DESIGN, 1997, 36 (05): : 80 - 80
  • [7] Managing the life cycle of Java']Java Card applets in other Java']Java virtual machines
    Roland, Michael
    Langer, Josef
    Mayrhofer, Rene
    [J]. INTERNATIONAL JOURNAL OF PERVASIVE COMPUTING AND COMMUNICATIONS, 2014, 10 (03) : 291 - +
  • [8] A secure Java']Java™ Virtual Machine
    van Doom, L
    [J]. USENIX ASSOCIATION PROCEEDINGS OF THE NINTH USENIX SECURITY SYMPOSIUM, 2000, : 19 - 34
  • [9] Defining the Java']Java Virtual Machine as platform for provably correct Java']Java compilation
    Börger, E
    Schulte, W
    [J]. MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 1998, 1998, 1450 : 17 - 35
  • [10] Security Enhanced Java']Java: Mandatory Access Control for the Java']Java Virtual Machine
    Venelle, Benjamin
    Briffaut, Jeremy
    Clevy, Laurent
    Toinard, Christian
    [J]. 2013 IEEE 16TH INTERNATIONAL SYMPOSIUM ON OBJECT/COMPONENT/SERVICE-ORIENTED REAL-TIME DISTRIBUTED COMPUTING (ISORC), 2013,
12345