A Space-Aware Bytecode Verifier for Java']Java Cards

被引:0
|
作者
Bernardeschi, Cinzia [1 ]
Lettieri, Giuseppe [1 ]
Martini, Luca [1 ]
Masci, Paolo [1 ]
机构
[1] Univ Pisa, Dipartimento Ingn Informaz, Pisa, Italy
关键词
Embedded systems; data-flow analysis; type correctness;
D O I
10.1016/j.entcs.2005.02.027
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
The bytecode verification is a key point of the security chain of the Java Platform. This feature is optional in many embedded devices since the memory requirements of the verification process are too high. In this paper we propose a verification algorithm that remarkably reduces the use of the memory by performing the verification during multiple specialized passes. The algorithm reduces the type encoding space by operating on different abstractions of the domain of types. The results of the experiments show that this bytecode verification can be performed directly on small memory systems.
引用
收藏
页码:237 / 254
页数:18
相关论文
共 50 条
  • [1] A space-aware bytecode verifier for java cards
    Bernardeschi, Cinzia
    Lettieri, Giuseppe
    Martini, Luca
    Masci, Paolo
    [J]. Electron. Notes Theor. Comput. Sci., 1 SPEC. ISS. (237-254):
  • [2] Research on On-card Bytecode Verifier for Java']Java Cards
    Wang, Tongyang
    Yu, Pengfei
    Wu, Jun-jun
    Ma, Xin-long
    [J]. JOURNAL OF COMPUTERS, 2009, 4 (06) : 502 - 509
  • [3] Modeling the Java']Java Bytecode Verifier
    Reynolds, Mark C.
    [J]. SCIENCE OF COMPUTER PROGRAMMING, 2013, 78 (03) : 327 - 342
  • [4] A formal framework for the Java']Java bytecode language and verifier
    Freund, SN
    Mitchell, JC
    [J]. ACM SIGPLAN NOTICES, 1999, 34 (10) : 147 - 166
  • [5] A type system for the Java']Java bytecode language and verifier
    Freund, SN
    Mitchell, JC
    [J]. JOURNAL OF AUTOMATED REASONING, 2003, 30 (3-4) : 271 - 321
  • [6] Bytecode verification on Java']Java smart cards
    Leroy, X
    [J]. SOFTWARE-PRACTICE & EXPERIENCE, 2002, 32 (04): : 319 - 340
  • [7] An Abstract Interpretation Approach for Enhancing the Java']Java Bytecode Verifier
    Barbuti, Roberto
    De Francesco, Nicoletta
    Tesei, Luca
    [J]. COMPUTER JOURNAL, 2010, 53 (06): : 679 - 700
  • [8] On the implementation of a stand-alone Java']Java™ Bytecode Verifier
    Painchaud, F
    Debbabi, M
    [J]. IEEE 9TH INTERNATIONAL WORKSHOPS ON ENABLING TECHNOLOGIES: INFRASTRUCTURE FOR COLLABORATIVE ENTERPRISES, PROCEEDINGS, 2000, : 189 - 194
  • [9] A certified lightweight non-interference Java']Java bytecode verifier
    Barthe, Gilles
    Pichardie, David
    Rezk, Tamara
    [J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2013, 23 (05) : 1032 - 1081
  • [10] Proving the soundness of a Java']Java bytecode verifier specification in Isabelle/HOL
    Pusch, C
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1999, 1579 : 89 - 103