A Principled Approach to Tracking Information Flow in the Presence of Libraries
A Principled Approach to Tracking Information Flow in the Presence of Libraries
复制标题
图书馆存在下跟踪信息流的原则方法
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
A. Sabelfeld
中科院分区：
文献类型：
--
作者：
Daniel Hedin;Alexander Sjösten;Frank Piessens;A. Sabelfeld
在越来越复杂的编程语言中，程序的信息流控制已经取得了令人鼓舞的进展，跟踪信息从输入源到输出汇的传播。然而，程序通常部署在具有丰富API和强大库的环境中，当这些API和库的代码不可用或以不同语言编写时，对信息流控制构成挑战。
本文提出了一个原则性的方法来跟踪信息流在图书馆的存在。为了达到安全性和精确性之间的平衡，我们提出了一个框架，探索“浅”，基于签名的建模库和“深”，有状态的方法，其中库模型需要手动提供之间的中间地带。我们正式我们的方法的核心语言，扩展它与列表和高阶函数，并建立健全的结果不干涉的安全条件。
There has been encouraging progress on information flow control for programs in increasingly complex programming languages, tracking the propagation of information from input sources to output sinks. Yet, programs are typically deployed in an environment with rich APIs and powerful libraries, posing challenges for information flow control when the code for these APIs and libraries is either unavailable or written in a different language.
This paper presents a principled approach to tracking information flow in the presence of libraries. With the goal to strike the balance between security and precision, we present a framework that explores the middle ground between the "shallow", signature-based modeling of libraries and the "deep", stateful approach, where library models need to be supplied manually. We formalize our approach for a core language, extend it with lists and higher-order functions, and establish soundness results with respect to the security condition of noninterference.