A Library for Secure Multi-threaded Information Flow in Haskell
A Library for Secure Multi-threaded Information Flow in Haskell
复制标题
Haskell 中的安全多线程信息流库
DOI：
10.1109/csf.2007.6
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
John Hughes
中科院分区：
文献类型：
--
作者：
Ta;Alejandro Russo;John Hughes
Li和Zdancewic最近提出了一种通过库提供信息流安全性的方法，而不是从头开始生产新语言。他们已经通过使用箭头组合器展示了如何在Haskell中实现此类库。但是，他们的方法仅适用于没有副作用的计算。实际上，他们作为一个悬而未决的问题，需要修改其图书馆以及其中的机制，以考虑这些效果。库中的另一个缺失功能是支持多线程程序。多线程程序中的信息流仍然是一个挑战，并且尚未实施支持。因此，提供信息流安全性的两个主流编译器（JIF和FlowCAML）缺乏对多线程的支持也就不足为奇了。根据文献提出的想法，本文提出了Li和Zdancewic库的扩展，该图书馆在参考操作和多线程程序的存在下提供了信息流安全性。此外，已经实施了在线购物案例研究，以评估所提出的技术。案例研究表明，在实践中利用并发泄漏秘密是可行的和危险的，以及我们的扩展方式如何避免这种情况。据我们所知，这是保证并发计划中信息流安全性的第一个实施工具，也是涉及并发和信息流策略的案例研究的首次实施。
Li and Zdancewic have recently proposed an approach to provide information-flow security via a library rather than producing a new language from the scratch. They have shown how to implement such a library in Haskell by using arrow combinators. However, their approach only works with computations that have no side-effects. In fact, they leave as an open question how their library, and the mechanisms in it, need to be modified to consider these kind of effects. Another absent feature in the library is support for multithreaded programs. Information-flow in multi-threaded programs still remains as a challenge, and no support for that has been implemented yet. It is not surprising, then, that the two main stream compilers that provide information-flow security, Jif and FlowCaml, lack support for multithreading. Following ideas taken from literature, this paper presents an extension to Li and Zdancewic's library that provides information-flow security in presence of reference manipulation and multithreaded programs. Moreover, an online-shopping case study has been implemented to evaluate the proposed techniques. The case study reveals that exploiting concurrency to leak secrets is feasible and dangerous in practice and how our extension helps avoiding that. To the best of our knowledge, this is the first implemented tool to guarantee information-flow security in concurrent programs and the first implementation of a case study that involves concurrency and information-flow policies.