一种新的Java智能卡上字节码校验算法

Java智能卡上的字节码校验是保障Java卡安全的重要手段。但是,由于Java智能卡本身的空间和运算器的限制,传统的字节码校验算法无法在Java智能卡上实现。为了解决此问题,本文在分析了现有方法的特点和不足的基础上提出了一种基于有向分枝图和缓存策略的字节码校验算法。效率分析和实践表明,该算法是一种可以在Java智能卡上实现
现的高效算法。     

基于缓存策略的Java卡字节码校验

作为一种不可靠的可下载Java程序， Java卡的字节码校验是安全的嵌入式系统所不可缺少的一个部分。由于Java卡本身的空间和运算器的限制，传统的字节码校验并不可取。采用非易失性存储器作为主存， RAM中的一部分空间作为缓存器，并且给出一种相应的Cache调度策略算法，尝试实现一种在卡上的Java卡的字节码校验算法，并且证明了该算法具有较好的可移植性和实现性。     

基于混合模式的Java卡字节码优化器

Java卡是一种基于Java语言的智能卡。因为智能卡的空间和处理器速度的约束,一个应用程序在Java卡上运行时面临的最大问题是存储空间的不足和对程序执行时间的严格限制。因此,对下载到卡中的字节码进行优化是十分必要的。本文提出了一种综合使用扩展指令集和分段压缩算法的Java卡字节码优化器的设计方案,通过对字节码文件的优化,可得到占用空间较少且没有降低执行速率的字节码文件。     

一种Java字节码保护技术的研究和实现

分析了Java字节码保护技术的现状,在此基础上提出了一种基于JVMTI的Java字节码保护技术,使得Java字节码的安全级别相当于传统的二进制代码。最后,给出了该技术在Win-dows平台和Linux平台下的实现方案。     

基于随机插入策略的Java混淆器设计与实现

控制流混淆用于混淆程序的运行流程,从而防止对软件的逆向工程,但通常混淆后的程序在代码量以及执行时间方面都有较大增长.提出了随机插入混淆策略,采用分支插入算法和循环条件插入算法相结合,并引入了随机函数以限制代码的插入操作,从而控制代码长度的增长.使用BCEL设计并实现了基于Java字节码的控制流混淆转换工具,能够实现Java字节码的迭代混淆,且混淆结果具有一定的不可再现性.实验结果表明,该策略能够有效地控制混淆转换带来的性能过载,同时能够有效地防止逆向工程攻击.     

过Java的自定义类加载器执行保存在Web服务器上的字节码文件

Java的解释器是通过将Java类的字节码文件装入Java运行环境,然后接受字节码检验器的检验后再运行之.由于Java类文件中使用的字节码格式是有很好的文档基础,对于具有汇编程序设计经验并且拥有一个十六进制编辑器的人来说,要想人工为Java解释器产生一个包含有效而不安全指令的类文件,这是一件非常容易的事情.本文则从安全角度出发,探讨了如何将Java字节码文件预先存入指定的Web服务器中,然后通过自定义的Java类加载器来运行保存在指定的Web服务器中的字节码文件的方法,并对其可行性进行了深入的讨论.     

Java处理器关键技术分析

传统的Java程序利用软件Java虚拟机(Java Virtual Machine,JVM)对Java字节码文件进行解释或二次编译后交由本地CPU执行,其运行速度大大受限,而硬件JVM处理器可直接执行Java字节码,因而大幅提高了Java程序的运行速度,所以硬件JVM处理器是突破Java程序性能瓶颈的最有效方法.本文以Jop Java及picoJava为例,根据Java虚拟机的规范分析了硬件JVM处理器中最重要的流水线结构、堆栈结构及操作的实现方式、指令折叠技术和字节码与微码的映射技术,并提出了改进措施.     

字节型CRC算法分析与实现

循环冗余码校验CRC是计算机网络通信中最常采用的数据校验方法之一,CRC方法能够很好地降低数据传输的误码率。本文分析了CRC算法的原理和CRC算法的校验规则,针对字节型CRC算法,提出一种直观、紧凑、易于理解的表驱动字节型算法描述,给出了严格的数学证明,通过实例详细演绎了算法的实现过程。同时,设计了相关的类汇编语言CRC-ITU算法,简要讨论了使用F(x)/G(x)的直接余式作为监督码的方法。     

基于数据流的脆弱性静态分析

为提高Java软件的安全性,针对Java程序的脆弱性分析问题,提出一种基于数据流的感染分析法,阐述了具体思路和实现步骤.依据该方法实现的分析系统能有效分析出Java字节码程序中存在的XPath注入、SQL注入等脆弱性,结果证明了基于数据流的感染分析法的正确性和可行性.     

面向Java锁机制的字节码自动重构框架

Java语言提供了同步锁、可重入锁和读写锁等几种锁机制,在并行程序设计中不同的数据结构使用这几种锁机制时获得的性能通常是不同的。为了在不同的锁机制之间进行自动转换,进而帮助程序员了解程序的性能,提出了一种面向Java锁机制的字节码自动重构框架,并基于该框架实现了字节码重构工具Lock2Lock。Lock2Lock在Quad中间表示的基础上对字节码进行静态分析,并对分析的结果进行一致性验证,通过Javassist完成字节码的重构。使用红黑树、消费者生产者程序以及SPECjbb2005 3个测试程序对Lock2Lock重构工具进行了测试,结果表明,Lock2Lock可以成功地实现从同步锁到可重入锁或读写锁的重构。     

Bytecode verification on Java smart cards

This article presents a novel approach to the problem of bytecode verification for Java Card applets. By relying on prior off‐card bytecode transformations, we simplify the bytecode verifier and reduce its memory requirements to the point where it can be embedded on a smart card, thus increasing significantly the security of post‐issuance downloading of applets on Java Cards. This article describes the on‐card verification algorithm and the off‐card code transformations, and evaluates experimentally their impact on applet code size. Copyright © 2002 John Wiley & Sons, Ltd.     

Java Card在智能卡开发中的应用

阐述了SUN公司推出的Java card在智能卡开发应用中的实现过程,阐明其构架以及主要的API。提出Java Card的安全性问题,推荐 使用椭圆曲线算法,并在Java Card API中补充设计加密解密部分。     

Lightweight Bytecode Verification

In this paper, we provide a theoretical foundation for and improvements to the existing bytecode verification technology, a critical component of the Java security model, for mobile code used with the Java “micro edition” (J2ME), which is intended for embedded computing devices. In Java, remotely loaded “bytecode” class files are required to be bytecode verified before execution, that is, to undergo a static type analysis that protects the platform's Java run-time system from so-called type confusion attacks such as pointer manipulation. The data flow analysis that performs the verification, however, is beyond the capacity of most embedded devices because of the memory requirements that the typical algorithm will need. We propose to take a proof-carrying code approach to data flow analysis in defining an alternative technique called “lightweight analysis” that uses the notion of a “certificate” to reanalyze a previously analyzed data flow problem, even on poorly resourced platforms. We formally prove that the technique provides the same guarantees as standard bytecode safety verification analysis, in particular that it is “tamper proof” in the sense that the guarantees provided by the analysis cannot be broken by crafting a “false” certificate or by altering the analyzed code. We show how the Java bytecode verifier fits into this framework for an important subset of the Java Virtual Machine; we also show how the resulting “lightweight bytecode verification” technique generalizes and simulates the J2ME verifier (to be expected as Sun's J2ME “K-Virtual machine” verifier was directly based on an early version of this work), as well as Leroy's “on-card bytecode verifier,” which is specifically targeted for Java Cards.     

JCVM异常处理机制

在对Java卡平台异常类层次结构和CAP文件内容深入分析的基础上，结合智能卡运行环境的特点，采用编译后的异常处理表与运行期的Java栈结构相结合的方法，设计并实现了解释执行时Java卡虚拟机中的异常处理机制。实际测试表明系统运行正确。     

The KeY tool

KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an integrated manner. Formal specification is performed using the Object Constraint Language (OCL), which is part of the UML standard. KeY provides support for the authoring and formal analysis of OCL constraints. The target language of KeY based development is Java Card DL, a proper subset of Java for smart card applications and embedded systems. KeY uses a dynamic logic for Java Card DL to express proof obligations, and provides a state-of-the-art theorem prover for interactive and automated verification. Apart from its integration into UML based software development, a characteristic feature of KeY is that formal specification and verification can be introduced incrementally.     

智能卡的研究与发展

综述了智能卡及ＪＡＶＡ卡的相关技术,智能ＩＣ卡由硬件和操作系统组成 ,可理解成一个计算机系统,智能ＩＣ卡有着完善的安全技术体制,安全性是其最大的特点,近年来,Ｊａｖａ技术与智能卡技术的结合产生了Ｊａｖａ卡,Ｊａｖａ卡是一种新型的智能卡,它基于Ｊａｖａ语言和Ｊａｖａ卡虚拟机ＪＣＶＭ（Ｊａｖａ Ｃａｒｄ Ｖｉｒｔｕａｌ Ｍａｃｈｉｎｅ）,是智能卡发展的方向。     

基于Java卡的电子护照设计与实现

为便于各种护照信息的管理,提出一种基于Java卡平台的电子护照设计方案,根据ICAO Doc 9303标准对其具体功能加以实现。同时参照Java卡的特点设计一种通用的Java卡文件包Javacardmesjar,并介绍透明文件和定长记录文件的实现过程。实验结果表明,采用该方案实现的电子护照运行稳定,具有一定应用价值。