基于自动机的Java信息流分析

Automata-based information flow analysis for Java

面向Java的信息流分析工作需要修改编译器或实时执行环境,对已有系统兼容性差,且缺乏形式化分析与安全性证明。首先,提出了基于有限状态自动机的Java信息流分析方法,将整个程序变量污点取值空间抽象为自动机状态空间,并将Java字节码指令看做自动机状态转换动作;然后,给出了自动机转换的信息流安全规则,并证明了在该规则下程序执行的无干扰安全性;最后,采用静态污点跟踪指令插入和动态污点跟踪与控制的方法实现了原型系统IF-JVM,既不需要获得Java应用程序源码,也不需要修改Java编译器和实时执行环境,更独立于客户操作系统。实验结果表明,原型系统能正确实现对Java的细粒度的信息流跟踪与控制,性能开销为53. 1%。

Existing Java-oriented information flow analysis works did not compatible with current systems due to the modifying of the compiler or run-time execution environment. At the same time,they also lacked of formal analysis and security proof.First,this paper proposed a formal Java-oriented information flow analysis method based on finite state automata. It abstracted the taint value space of entire program variables into the state space of automata and transferred the Java bytecode instructions into the state transition actions of automata. Then,it gave the information flow security rules of state machine conversion and proved the noninterference security property under these rules. Finally,it implemented the prototype system named IF-JVM by using the static taint track instruction inserting and dynamic taint tracking technologies. IF-JVM was independent of the customer operating system. Neither needed to get the source code of Java application,nor needed to modify the Java compiler or runtime execution environment. The experimental results show that the IF-JVM is an accurate system that tracking and controlling information flow for the Java with the 53. 1% overhead on performance.