Information flow enforcement in monadic libraries
Information flow enforcement in monadic libraries
复制标题
单元图书馆中的信息流实施
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
Frank Piessens
中科院分区：
文献类型：
--
作者：
Dominique Devriese;Frank Piessens
在各种场景下，都需要将某个API暴露给不完全信任的客户端程序。如果客户端程序需要访问敏感数据，可以使用信息流策略来强制保密。这是一项普遍而有力的政策，已被广泛研究和实施。
先前的工作已经展示了如何以库的形式以轻量级方式实施信息流策略实施。然而，这些方法都受到许多限制。通常，策略及其实施并未与底层 API 完全分离，并且 API 的用户会暴露于经过强烈且非自然修改的接口。有些方法仅限于功能性 API，难以处理 I/O 和可变状态变量等命令性功能。此外，这项先前的工作使用经典的静态信息流实施技术，并且没有考虑更新的动态信息流实施技术。
在本文中，我们展示了可以以模块化且合理通用的方式在命令式一元 API 上强制执行信息流策略，而对提供给 API 用户的接口影响很小。本文的主要思想是，我们在 monad 转换器中实现策略执行，而底层的 monadic API 仍然不知情且未修改。该策略是通过解除底层 monad 操作来指定的。
我们通过介绍三种重要的信息流执行技术的实现来展示我们方法的通用性，包括纯动态、纯静态和混合技术。其中两种技术需要使用 Monad 类型类的泛化，但对 API 接口的影响仍然有限。我们通过草图证明我们的静态技术的实现忠实于原始演示，表明我们的技术适合形式推理。最后，我们讨论我们的方法的基本局限性以及它如何适应一般信息流执行理论。
In various scenarios, there is a need to expose a certain API to client programs which are not fully trusted. In cases where the client programs need access to sensitive data, confidentiality can be enforced using an information flow policy. This is a general and powerful type of policy that has been widely studied and implemented.
Previous work has shown how information flow policy enforcement can be implemented in a lightweight fashion in the form of a library. However, these approaches all suffer from a number of limitations. Often, the policy and its enforcement are not cleanly separated from the underlying API, and the user of the API is exposed to a strongly and unnaturally modified interface. Some of the approaches are limited to functional APIs and have difficulty handling imperative features like I/O and mutable state variables. In addition, this previous work uses classic static information flow enforcement techniques, and does not consider more recent dynamic information flow enforcement techniques.
In this paper, we show that information flow policies can be enforced on imperative-style monadic APIs in a modular and reasonably general way with only a minor impact on the interface provided to API users. The main idea of this paper is that we implement the policy enforcement in a monad transformer while the underlying monadic API remains unaware and unmodifoed. The policy is specified through the lifting of underlying monad operations.
We show the generality of our approach by presenting implementations of three important information flow enforcement techniques, including a purely dynamic, a purely static and a hybrid technique. Two of the techniques require the use of a generalisation of the Monad type class, but impact on the API interface stays limited. We show that our technique lends itself to formal reasoning by sketching a proof that our implementation of the static technique is faithful to the original presentation. Finally, we discuss fundamental limitations of our approach and how it fits in general information flow enforcement theory.