Fully Automatic Logic-Based Information Flow Analysis

全自动基于逻辑的信息流分析

• 批准号: 228021792
• 负责人: Dr. Richard Bubel
• 金额: --
• 依托单位: Fachgebiet Software Engineering
• 依托单位国家: 德国
• 项目类别: Priority Programmes
• 财政年份: 2012
• 资助国家: 德国
• 起止时间: 2011-12-31 至 2015-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/228021792?language=en
• 关键词: Fully; Automatic; Logic; Based; Information

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.

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