一句话:提出基于抽象解释的责任分析,用迹语义抽象定义责任,并给出可靠的抽象分析框架。
该文研究程序静态分析中如何自动判定与给定行为对应的责任实体(根因)。作者基于迹语义的抽象提出新的责任定义,并引入观察者认知因素,较现有依赖与因果分析方法在多个示例上更精确。由于具体迹语义一般不可计算,具体责任分析不可判定。为此,文章提出可靠的抽象责任分析框架:通过带迹划分的向前可达性过近似与向后不可能失败可达性的欠/过近似迭代,构造迹划分自动机,并沿其路径确定潜在责任实体的上下界。抽象分析可能损失精度,但保持可靠性,具体责任实体必在抽象结果中被识别。
Given a behavior of interest, automatically determining the corresponding responsible entity (i.e., the root cause) is a task of critical importance in program static analysis. In this article, a novel definition of responsibility based on the abstraction of trace semantics is proposed, which takes into account the cognizance of observer, which, to the best of our knowledge, is a new innovative idea in program analysis. Compared to current dependency and causality analysis methods, the responsibility analysis is demonstrated to be more precise on various examples.However, the concrete trace semantics used in defining responsibility is uncomputable in general, which makes the corresponding concrete responsibility analysis undecidable. To solve this problem, the article proposes a sound framework of abstract responsibility analysis, which allows a balance between cost and precision. Essentially, the abstract analysis builds a trace partitioning automaton by an iteration of over-approximating forward reachability analysis with trace partitioning and under/over-approximating backward impossible failure accessibility analysis, and determines the bounds of potentially responsible entities along paths in the automaton. Unlike the concrete responsibility analysis that identifies exactly a single action as the responsible entity along every concrete trace, the abstract analysis may lose some precision and find multiple actions potentially responsible along each automaton path. However, the soundness is preserved, and every responsible entity in the concrete is guaranteed to be also found responsible in the abstract.
@article{paperbot1204,
title = {The Systematic Design of Responsibility Analysis by Abstract Interpretation},
author = {Chaoqiang Deng and Patrick Cousot},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {44},
number = {1},
year = {2021},
doi = {10.1145/3484938}
}