基于自动机的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.
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.
引文
[1]吴泽智,陈性元,杨智,等.信息流控制研究进展[J].软件学报,2017,28(1):135-159.
[2] Crandall J R,Chong F T. Minos:control data attack prevention orthogonal to memory model[C]//Proc of the 37th International Symposium on Microarchitecture. Washington DC:IEEE Computer Society,2004:221-232.
[3] Kemerlis V P,Portokalidis G,Jee K,et al. Libdft:practical dynamic data flow tracking for commodity systems[J]. ACM SIGPLAN Notices,2012,47(7):121-132.
[4] Krohn M,Yip A,Brodsky M,et al. Information flow control for standard OS abstractions[C]//Proc of ACM SIGOPS Operating Systems Review. New York:ACM Press,2007:321-334.
[5] Schultz D,Liskov B. IFDB:decentralized information flow control for databases[C]//Proc of the 8th ACM European Conference on Computer Systems. New York:ACM Press,2013:43-56.
[6] Enck W,Gilbert P,Chun B G,et al. Taint Droid:an information-flow tracking system for realtime privacy monitoring on smartphones[C]//Proc of the 9th USENIX Symposium on Operating Systems Design and Implementation. Berkeley:USENIX Association,2010:255-270.
[7] Nair S K,Simpson P N D,Crispo B,et al. A virtual machine based information flow control system for policy enforcement[J]. Electronic Notes in Theoretical Computer Science,2008,197(1):3-16.
[8] Roy I,Porter D E,Bond M D,et al. Laminar:practical fine-grained decentralized information flow control[J]. ACM SIGPLAN Notices,2009,44(6):63-74.
[9] Haldar V,Chandra D,Franz M. Dynamic taint propagation for Java[C]//Proc of the 21st Annual Computer Security Applications Conference. Washington DC:IEEE Computer Society,2006:303-311.
[10]Matej V,Binder W,Hauswirth M. ShadowData:shadowing heap objects in Java[C]//Proc of the 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering. New York:ACM Press,2013:17-24.
[11]Chandra D,Franz M. Fine-Grained information flow analysis and enforcement in a Java virtual machine[C]//Proc of the 23rd Annual Computer Security Applications Conference. Piscataway,NJ:IEEE Press,2007:463-475.
[12] Manivannan K,Wimmer C,Franz M. Decentralized information flow control on a bare-metal JVM[C]//Proc of the 6th Annual Workshop on Cyber Security and Information Intelligence Research. New York:ACM Press,2010:64-74.
[13]Myers A C,Liskov B. Protecting privacy using the decentralized label model[J]. ACM Trans on Software Engineering and Methodology,2000,9(4):410-442.
[14]Myers A C. JFlow:practical mostly-static information flow control[C]//Proc of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York:ACM Press,1999:228-241.
[15]Blackburn S M,Garner R,Hoffmann C,et al. The dacapo benchmarks:Java benchmarking development and analysis[C]//Proc of the21st Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems,Languages,and Applications. New York:ACM Press,2006:169-190.
[2] Crandall J R,Chong F T. Minos:control data attack prevention orthogonal to memory model[C]//Proc of the 37th International Symposium on Microarchitecture. Washington DC:IEEE Computer Society,2004:221-232.
[3] Kemerlis V P,Portokalidis G,Jee K,et al. Libdft:practical dynamic data flow tracking for commodity systems[J]. ACM SIGPLAN Notices,2012,47(7):121-132.
[4] Krohn M,Yip A,Brodsky M,et al. Information flow control for standard OS abstractions[C]//Proc of ACM SIGOPS Operating Systems Review. New York:ACM Press,2007:321-334.
[5] Schultz D,Liskov B. IFDB:decentralized information flow control for databases[C]//Proc of the 8th ACM European Conference on Computer Systems. New York:ACM Press,2013:43-56.
[6] Enck W,Gilbert P,Chun B G,et al. Taint Droid:an information-flow tracking system for realtime privacy monitoring on smartphones[C]//Proc of the 9th USENIX Symposium on Operating Systems Design and Implementation. Berkeley:USENIX Association,2010:255-270.
[7] Nair S K,Simpson P N D,Crispo B,et al. A virtual machine based information flow control system for policy enforcement[J]. Electronic Notes in Theoretical Computer Science,2008,197(1):3-16.
[8] Roy I,Porter D E,Bond M D,et al. Laminar:practical fine-grained decentralized information flow control[J]. ACM SIGPLAN Notices,2009,44(6):63-74.
[9] Haldar V,Chandra D,Franz M. Dynamic taint propagation for Java[C]//Proc of the 21st Annual Computer Security Applications Conference. Washington DC:IEEE Computer Society,2006:303-311.
[10]Matej V,Binder W,Hauswirth M. ShadowData:shadowing heap objects in Java[C]//Proc of the 11th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering. New York:ACM Press,2013:17-24.
[11]Chandra D,Franz M. Fine-Grained information flow analysis and enforcement in a Java virtual machine[C]//Proc of the 23rd Annual Computer Security Applications Conference. Piscataway,NJ:IEEE Press,2007:463-475.
[12] Manivannan K,Wimmer C,Franz M. Decentralized information flow control on a bare-metal JVM[C]//Proc of the 6th Annual Workshop on Cyber Security and Information Intelligence Research. New York:ACM Press,2010:64-74.
[13]Myers A C,Liskov B. Protecting privacy using the decentralized label model[J]. ACM Trans on Software Engineering and Methodology,2000,9(4):410-442.
[14]Myers A C. JFlow:practical mostly-static information flow control[C]//Proc of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York:ACM Press,1999:228-241.
[15]Blackburn S M,Garner R,Hoffmann C,et al. The dacapo benchmarks:Java benchmarking development and analysis[C]//Proc of the21st Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems,Languages,and Applications. New York:ACM Press,2006:169-190.