CRII: SaTC: Repairing Code from Inferred Specifications of Information Flow Security

CRII：SaTC：根据信息流安全推断规范修复代码

• 批准号: 1657530
• 负责人: Jean Yang
• 金额: $ 17.5万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-03-01 至 2019-02-28
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1657530&HistoricalAwards=false
• 关键词: CRII; SaTC; Repairing; Code; Inferred

As more software computes using sensitive user data, it increasingly important to ensure that data flows only where it is permitted. Protecting sensitive data often involves reasoning about how sensitive values and policies are interacting with functionality across the program. The need to reason across the code base makes it difficult not only for programmers to implement computations using sensitive data, but also to make existing code adhere to new policies. This project investigates an approach for (1) inferring information flow policies from potentially buggy code and (2) performing program repair to ensure programs adhere to the specified policies. Not only does this approach help identify potential misuses of sensitive information, but it also helps prevent leaks in code from well-intentioned programmers, and provides a mechanism for modifying arbitrary code to satisfy a given policy.Enabling this approach is a policy-agnostic semantic model, developed to disentangle information flow concerns from other functionality. Using policy-agnostic programming, the programmer may implement information flow policies by specifying them alongside sensitive data values, rather than implementing them as conditional access checks across the program. Prior work on Lifty supports policy-agnostic programming using type-driven repair, based on program synthesis for liquid types, which are value-dependent refinement types. Previously, programs could only benefit from policy-agnostic programming if the policies are known, but this is not always the case with existing code. We propose an approach for inferring liquid types from potentially buggy code. The inferred types now make it possible to perform sound repair. Representing the inferred policies as liquid types also facilitates modification of the policies. The proposal describes both a strategy for inferring a set of possible policies, and a solution for choosing which policies to use for repair.

随着越来越多的软件使用敏感的用户数据进行计算，确保数据只在允许的地方流动变得越来越重要。保护敏感数据通常涉及推理敏感值和策略如何与程序中的功能交互。需要跨代码库进行推理，这不仅使程序员难以使用敏感数据实现计算，而且使现有代码遵守新策略。本项目研究一种方法，用于（1）从潜在的错误代码中推断信息流策略，以及（2）执行程序修复以确保程序遵守指定的策略。这种方法不仅有助于识别敏感信息的潜在误用，而且还有助于防止善意程序员泄露代码，并提供一种修改任意代码以满足给定策略的机制。启用这种方法的是一种与策略无关的语义模型，该模型被开发用于将信息流关注点与其他功能区分开来。使用与策略无关的编程，程序员可以通过将信息流策略与敏感数据值一起指定来实现信息流策略，而不是将它们实现为跨程序的条件访问检查。Lifty之前的工作支持使用类型驱动修复的策略无关编程，基于液体类型的程序合成，这是值依赖的细化类型。以前，程序只有在策略已知的情况下才能从策略无关编程中受益，但现有代码并不总是如此。我们提出了一种方法，从潜在的错误代码推断液体类型。推断的类型现在可以执行声音修复。将所推断的策略表示为流动类型还便于策略的修改。该提案描述了一个策略，用于推断一组可能的政策，并选择哪些政策用于修复的解决方案。