Collaborative Research: SaTC: CORE: Small: Hyperproperty-based Enforcement of Information-flow Security

协作研究：SaTC：核心：小型：基于超产权的信息流安全执行

• 批准号: 2245115
• 负责人: Limin Jia
• 金额: $ 30万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2026-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2245115&HistoricalAwards=false
• 关键词: Collaborative; Research; SaTC; CORE; Small

Enforcing security policies such as secrecy or integrity is crucial for software systems that handle large volumes of users’ sensitive information, where even a short transient violation of these policies may result in leaking or damaging highly sensitive information, compromising safety, or interruption of vital public or social services. Runtime monitoring and enforcement of security policies remains one of the foundational techniques for securing software systems. Many important security policies such as information-flow policies cannot be expressed as properties of individual executions, but can be expressed as properties on multiple execution traces, which are called hyperproperties. Motivated by a rich set of real-world applications, the overarching objective of this project is to develop effective runtime enforcement techniques for hyperproperties that enable strong protection of systems against various types of cyberattacks and information leaks. This project will bring about a paradigm shift in systematic runtime enforcement of information-flow properties, organized within three research thrusts that will develop novel monitor designs, open-source tools, and perform rigorous evaluation. The first thrust will develop black-box and grey-box predictive monitors for enforcing hyperproperties. This thrust will also investigate different input models, in particular, closed systems where the monitor can manipulate the input to the system to enforce a hyperproperty and reactive systems where the monitor cannot interfere with the input, as it is generated by an uncontrollable environment. The second thrust will focus on developing runtime monitors that are compositional. The project will design a composed monitor infrastructure where parts of the system are guarded by different monitors, as modern systems are composed of heterogeneous components from mutually distrusting sources. The third research thrust is dedicated to rigorous evaluation by delving into applications of the researchers' theoretical findings. This effort will apply results from the first two thrusts to implement monitors to enforce information flow properties and nonmalleable information flow on real world applications. The results of this project are expected to have several advantages as compared to the existing methods: they will be more general, as they can deal with a rich fragment of the temporal logic HyperLTL and will be transferable, compositional, and low-overhead.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

执行保密或诚信等安全策略对于处理大量用户敏感信息的软件系统至关重要，即使短暂违反这些政策也可能导致泄漏或损害高度敏感的信息，损害高度敏感的信息，损害安全性或中断重要的公共或社交服务。安全策略的运行时监视和执行仍然是确保软件系统的基础技术之一。许多重要的安全策略（例如信息流策略）不能表示为单个执行的属性，但可以表示为多个执行轨迹上的属性，这些属性称为HyperProperties。该项目的总体目标是由一系列现实世界的应用程序进行的，是为了开发有效的运行时执行技术，以实现超专业，从而使系统能够对各种类型的网络攻击和信息泄漏进行强有力的保护。该项目将带来信息流属性的系统运行时执行范式的范式，这将在三个研究推力中组织起来，这将开发新颖的监视器设计，开源工具并执行严格的评估。第一个推力将开发黑框和灰色盒子预测监测器，以实施超构成。该推力还将研究不同的输入模型，特别是封闭的系统，其中监视器可以操纵系统的输入来强制执行超副处理和反应性系统，在该系统中，监视器无法干扰输入，因为它是由无法控制的环境生成的。第二个推力将集中于开发组成的运行时监视器。该项目将设计一个组成的监视器基础架构，该基础架构由不同的监视器保护，因为现代系统由相互不信任来源的异构组件组成。第三项研究作用是通过研究研究人员理论发现的应用，致力于严格的评估。这项工作将采用前两个推力的结果来实施监视器，以在现实世界应用程序上执行信息流属性和不可偿还的信息流。与现有方法相比，该项目的结果预计将具有多个优势：它们将更加笼统，因为它们可以处理暂时的逻辑超级LTL的丰富片段，并将转移，组成和低空交易。这奖反映了NSF的立法任务，并被认为是通过基金会的智力评估来评估的，并且值得通过评估来评估基金会的优点和广泛的范围。