论文标题
符号抽象堆的多态性信息流式推理（扩展版）
Symbolic Abstract Heaps for Polymorphic Information-flow Guard Inference (Extended Version)
论文作者
论文摘要
在以对象为导向的程序分析的信息流控制的领域中，很少有方法采用了堆的流敏化抽象，从而可以对隐式流进行精确的建模。为了应对这一挑战，我们推进了一种新的符号抽象方法，用于在类似Java的程序中建模堆。我们使用的无商店表示，该表示与参考文献之间的一个关系家族进行了参数化，以根据用户偏好提供各种级别的精度。这使我们能够通过对符号有限状态系统的共透性分析来自动推断出多态性信息流程。我们将堆抽象实例化与三个不同的关系家族。我们通过使用IFSPEC基准和现实生活应用程序，证明了方法的合理性，并比较了每个实例化堆域获得的精度和可伸缩性。
In the realm of sound object-oriented program analyses for information-flow control, very few approaches adopt flow-sensitive abstractions of the heap that enable a precise modeling of implicit flows. To tackle this challenge, we advance a new symbolic abstraction approach for modeling the heap in Java-like programs. We use a store-less representation that is parameterized with a family of relations among references to offer various levels of precision based on user preferences. This enables us to automatically infer polymorphic information-flow guards for methods via a co-reachability analysis of a symbolic finite-state system. We instantiate the heap abstraction with three different families of relations. We prove the soundness of our approach and compare the precision and scalability obtained with each instantiated heap domain by using the IFSpec benchmarks and real-life applications.
