Fully Automatic Logic-Based Information Flow Analysis

在这个项目中，我们将开发一种全自动的基于逻辑的方法，用于面向对象程序（特别是Java）的信息流分析。基于语言的信息流安全分析允许通过观察程序的不同运行来确保没有秘密可以被了解。目前的信息流分析要么是全自动的，但高度近似和不精确。因此，他们将许多实际上安全的程序归类为不安全的。这些方法中的大多数也仅限于小型的、学术性的玩具语言。•或者它们是精确的分析，但需要大量、耗时和昂贵的用户交互。在这个项目中，我们设想了用真实世界编程语言（Java）编写的程序的演绎信息流分析，它是完全自动化的，并且比以前的自动方法接受更大的安全程序类。分析性能的提高将通过以下方式实现：1。我们将把我们的方法建立在一般的程序逻辑和符号执行的基础上。采用基于逻辑的方法的优点是可以实现对程序语言语义的忠实和精确的建模，而无需先验的简化或抽象。其他方法从一个粗略的抽象开始，必须通过几个细化步骤进行迭代，直到达到必要的精度。为了完全自动化并避免任何类型的用户交互，我们将开发一种符号状态抽象技术。这种技术允许我们完全自动地处理程序结构，如循环（否则需要用户交互）。所提出的技术将抽象符号状态，而不是程序本身。抽象只在必要时（按需）执行，并限制在状态的那些部分，这些部分可能通过循环等方式进行修改。对于符号状态的其余部分，我们保持精确。这是由一些安全信息流属性的形式化补充，例如不干扰和分隔的信息发布，专门针对我们的方法量身定制。此外，我们将自动生成不安全程序的漏洞，以支持开发人员理解当前的信息流策略违反。我们的方法是基于符号执行的，它可以作为自动测试生成的基础。我们将使用这一事实将测试用例生成推广到开发利用生成。

In this project we will develop a fully automatic logic-based approach for information-flow analysis of object-oriented programs (specifically, Java).Language-based information-flow security analysis allows to ensure that no secrets can be learned by observing different runs of a program.Current information-flow analyses are either• fully automatic, but highly approximate and imprecise. Hence, they classify many actually secure programs as insecure. Most of these approaches are also limited to small, academic toy languages.• or they are precise analyses, but require significant, time-consuming, and expensive userinteraction.In this project we envision a deductive information-flow analysis for programs written in a real-word programming language (Java), which is fully automatic and accepts a significantly larger class of secure programs than previous automatic approaches.This increase of the analysis performance will be achieved as follows:1. We will base our approach on a general program logic and symbolic execution. The advantage of taking a logic-based approach is to achieve a faithful and precise modeling of the program language semantics without a priori simplifications or abstractions. Other approaches start with a coarse abstraction and have to iterate through several refinement steps until they reach the necessary precision.2. To be fully automatic and to avoid any kind of user interaction, we will develop a technique for symbolic state abstraction. This technique allows us to handle program constructs such as loops—which would otherwise require user-interaction—fully automatic. The proposed technique will abstract the symbolic state but not the program itself. The abstraction is performed only if necessary (on-demand) and restricted to those parts of the state, which are possibly modified by, e.g., a loop. For the remaining part of the symbolic state we stay precise.This is complemented by formalisations of a number of secure information-flow properties such as non-interference and delimited information release, specifically tailored towards our approach.In addition we will automatically generate exploits for insecure programs to support the developer in understanding the present information-flow policy violation. Our approach is based on symbolic execution, which can serve as a basis for automatic test generation. We will use this fact to generalize test case generation to exploit generation.