DIFC programs by automatic instrumentation

DIFC programs by automatic instrumentation
复制标题

DOI:
10.1145/1866307.1866340
复制
发表时间:
2010-10
期刊:
--
影响因子:
--
通讯作者:
William R. Harris;S. Jha;T. Reps
William R. Harris;S. Jha;T. Reps
中科院分区:
其他
文献类型:
--
作者:
William R. Harris;S. Jha;T. Reps

文献摘要

被引文献

相似文献

分散的信息流控制(DIFC)操作系统为应用程序提供了用于其数据的信息流策略的机制。但是,重大障碍使此类操作系统无法获得广泛的采用。一个关键的障碍是,DIFC操作系统仅提供低级机制,以允许应用程序程序员执行其所需的政策。程序员很难确保他们使用这些机制可以执行高级政策,同时又不破坏其应用程序的基本功能。对于将为DIFC操作系统开发新应用程序的程序员以及将现有应用程序将现有应用程序移植到DIFC操作系统的程序员的问题。我们的工作大大减轻了这些任务。我们将其作为自动技术呈现,将其作为没有DIFC代码的程序输入,以及两个策略:一种指定禁止的信息流,一种指定必须允许的流。然后,我们的技术生成了满足这两个政策的新版本的输入程序。为了评估技术,我们用称为游泳的自动工具(为了确保我的意思)实施了技术,并将其应用于一组现实世界中的程序和政策。我们评估的结果表明,该技术足以表达用于现实世界政策的程序,并且可以有效地生产此类程序。因此,它代表了开发具有强大端到端信息流量保证的系统的重要贡献。
Decentralized information flow control (DIFC) operating systems provide applications with mechanisms for enforcing information flow policies for their data. However, significant obstacles keep such operating systems from achieving widespread adoption. One key obstacle is that DIFC operating systems provide only low-level mechanisms for allowing application programmers to enforce their desired policies. It can be difficult for the programmer to ensure that their use of these mechanisms enforces their high-level policies, while at the same time not breaking the underlying functionality of their application. These are issues both for programmers who would develop new applications for a DIFC operating system and for programmers who would port existing applications to a DIFC operating system. Our work significantly eases these tasks. We present as automatic technique that takes as input a program with no DIFC code, and two policies: one that specifies prohibited information flows and one that specifies flows that must be allowed. Our technique then produces a new version of the input program that satisfies the two policies. To evaluate out technique, we implemented it in an automatic tool, called Swim (for Secure What I Mean), and applied it to a set of real-world programs and policies. The results of our evaluation demonstrate that the technique is sufficiently expressive to produce programs for real-world policies, and that it can produce such programs efficiently. It thus represents a significant contribution towards developing systems with strong end-to-end information flow guarantees.