基于自动机的Java信息流分析与无干扰安全系统

"这篇论文提出了一种基于有限状态自动机的Java信息流分析方法，旨在解决传统信息流分析对已有系统的兼容性问题和缺乏形式化分析的问题。通过将程序变量污点取值空间抽象为自动机状态空间，将Java字节码指令视为状态转换动作，实现了对Java程序的安全分析。此外，论文还设计并实现了原型系统IF-JVM，该系统无需源码、无需修改编译器和执行环境，具有独立于客户操作系统的特性，能够进行细粒度的信息流跟踪与控制，性能开销为53.1%。" 本文是一篇关于Java信息流分析的研究论文，主要关注如何利用有限状态自动机来改进传统的信息流分析技术。传统的信息流分析通常需要修改编译器或运行时环境，这可能对现有的系统兼容性造成影响，同时缺乏形式化的安全分析和证明。为了解决这些问题，作者提出了一个新颖的框架，其核心是将程序中的污点分析（用于追踪敏感信息的流动）与有限状态自动机相结合。 在论文中，首先介绍了将整个程序变量的污点取值空间抽象为有限状态自动机的状态空间的概念。每个状态代表一组可能的污点配置，而Java字节码指令则被视为状态之间的转换动作。这种抽象使得信息流分析能够以一种形式化的方式进行，有利于安全性分析和证明。 接着，论文提出了自动机转换的信息流安全规则。这些规则定义了在特定状态下，哪些字节码指令可以被执行而不破坏信息流安全性。作者进一步证明，在这些规则下，程序的执行是无干扰的，即敏感信息不会不当地泄露给不应接收到它的部分。 为了实现这一理论框架，论文描述了一个名为IF-JVM的原型系统。IF-JVM采用静态污点跟踪指令插入和动态污点跟踪与控制的技术，能够在不修改Java应用程序源码、不改动Java编译器和执行环境的情况下，实现对信息流的细粒度控制。由于IF-JVM独立于客户操作系统，因此具有更好的适应性和通用性。 实验结果显示，IF-JVM能够有效地进行Java程序的信息流跟踪和控制，尽管存在一定的性能开销，约为53.1%，但仍然显示了其在实际应用中的可行性。 该研究工作由吴泽智、陈性元、杜学绘和杨智等人完成，他们分别在解放军信息工程大学密码工程学院和密码科学技术国家重点实验室从事信息流控制、网络与信息安全、操作系统安全以及云计算安全等相关领域的研究。这项工作得到了国家高技术研究发展“863”计划和国家重点研发计划项目的资助。 总结来说，这篇论文提出了一种创新的、基于有限状态自动机的Java信息流分析方法，为提高现有系统的安全性和兼容性提供了新的思路，并通过实际原型系统验证了其有效性。这一研究成果对于理解和改善Java应用程序的安全性，特别是在不改变原有系统架构的前提下，具有重要的理论价值和实践意义。