Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings
Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings
复制标题
验证、模型检查和摘要解释 - 第 24 届国际会议，VMCAI 2023，美国马萨诸塞州波士顿，2023 年 1 月 16-17 日，会议记录
DOI：
10.1007/978-3-031-24950-1_4
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Berthier N
中科院分区：
文献类型：
--
作者：
Berthier N
在用于信息流控制的可靠的面向对象程序分析领域中，很少有方法采用堆的流敏感抽象来实现隐式流的精确建模。为了应对这一挑战，我们提出了一种新的符号抽象方法，用于在类Java程序中对堆进行建模。我们使用一个无存储的表示，参数化的家庭之间的关系的参考，提供不同程度的精度，根据用户的喜好。这使我们能够自动推断多态信息流警卫的方法，通过一个符号有限状态系统的可达性分析。我们用三个不同的关系族实例化堆抽象。我们证明了我们的方法的合理性，并通过使用theIFSpecbenchmarks和现实生活中的应用程序与每个实例化堆域获得的精度和可扩展性进行比较。
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 theIFSpecbenchmarks and real-life applications.