pith. sign in

arxiv: 1907.08251 · v1 · pith:LFEABWJWnew · submitted 2019-07-18 · 💻 cs.PL · cs.LO

Responsibility Analysis by Abstract Interpretation

Chaoqiang Deng , Patrick Cousot This is my paper

Pith reviewed 2026-05-24 19:03 UTC · model grok-4.3

classification 💻 cs.PL cs.LO
keywords responsibility analysisabstract interpretationevent trace semanticsprogram securitycausality analysisdependency analysis
0
0 comments X

The pith

An entity is responsible for a program behavior if it makes the first free input choice that guarantees the behavior will occur.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper defines responsibility for a given program behavior through the abstraction of its event trace semantics. Responsibility attaches to an entity exactly when that entity can freely select an input value and the selection is the earliest one that forces the behavior to happen in every possible continuation. This definition is intended to be sound while delivering greater precision than dependency analysis, taint analysis, or slicing, and it explicitly includes what an observer can know about the choices. The goal is to support static identification of accountable entities, especially for security tasks where classical causality models fall short on program structure.

Core claim

An entity ER is responsible for behavior B if and only if ER is free to choose its input value, and such a choice is the first one that ensures the occurrence of B in the forthcoming execution. The definition rests on an abstraction of the program's event trace semantics that preserves the necessary ordering and choice information.

What carries the argument

Abstraction of event trace semantics, which encodes execution sequences so that the first free choice guaranteeing a later behavior can be identified statically.

If this is right

  • Static responsibility analysis becomes possible for security properties without running the program.
  • The method distinguishes responsible entities more sharply than dependency analysis, taint analysis, or program slicing.
  • Observer knowledge about possible choices is incorporated directly into the responsibility judgment.
  • The same framework can be applied outside security to any domain modeled by discrete event traces.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The definition could be lifted to runtime monitoring by checking live traces against the same first-guarantee condition.
  • It suggests a way to compare responsibility across different program versions or refactorings by re-running the abstraction.
  • Similar trace-abstraction ideas might clarify accountability in distributed systems where messages play the role of input choices.

Load-bearing premise

The chosen abstraction of event trace semantics keeps enough ordering and choice detail for the responsibility definition to remain sound and more precise than dependency or causality methods.

What would settle it

A concrete program in which the analysis identifies one entity as responsible, yet an exhaustive enumeration of its traces shows that a different entity made an earlier choice that already guaranteed the same behavior.

Figures

Figures reproduced from arXiv: 1907.08251 by Chaoqiang Deng, Patrick Cousot.

Figure 1
Figure 1. Figure 1: Access Control Program Example [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Framework of Responsibility Analysis for Example [PITH_FULL_IMAGE:figures/full_fig_p006_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Trace Semantics and Properties of Example [PITH_FULL_IMAGE:figures/full_fig_p009_3.png] view at source ↗
Figure 5
Figure 5. Figure 5: Lattice of Behaviors As discussed in section 3.5, the responsibility analysis consists of four steps. For the sake of simplicity, we consider only the omniscient observer here. (1) Taking each assignment as an event, each maximal trace in this program is of length 3, and the program’s maximal trace semantics consists of in￾finite number of such traces. E.g. balance=0 . n=5 . balance=-5 denotes a maximal ex… view at source ↗
Figure 6
Figure 6. Figure 6: Lattice of Behaviors regarding Information Leakage [PITH_FULL_IMAGE:figures/full_fig_p017_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Floyd-Hoare automaton for Example 12, 13, 14, and 15 reachable concrete state satisfying I( ` ) from which there are two concrete execu￾tions which will definitely reach a terminal state satisfying Pb for one and P¬b for the other. >Max means that this is a possibility but not a certitude. We start with marking every terminal node in the Floyd-Hoare automaton with either Pb or P¬b and marking every other n… view at source ↗
Figure 8
Figure 8. Figure 8: Floyd-Hoare automaton for Example 16 [PITH_FULL_IMAGE:figures/full_fig_p032_8.png] view at source ↗
read the original abstract

Given a behavior of interest in the program, statically determining the corresponding responsible entity is a task of critical importance, especially in program security. Classical static analysis techniques (e.g. dependency analysis, taint analysis, slicing, etc.) assist programmers in narrowing down the scope of responsibility, but none of them can explicitly identify the responsible entity. Meanwhile, the causality analysis is generally not pertinent for analyzing programs, and the structural equations model (SEM) of actual causality misses some information inherent in programs, making its analysis on programs imprecise. In this paper, a novel definition of responsibility based on the abstraction of event trace semantics is proposed, which can be applied in program security and other scientific fields. Briefly speaking, an entity ER is responsible for behavior B, if and only if ER is free to choose its input value, and such a choice is the first one that ensures the occurrence of B in the forthcoming execution. Compared to current analysis methods, the responsibility analysis is more precise. In addition, our definition of responsibility takes into account the cognizance of the observer, which, to the best of our knowledge, is a new innovative idea in program analysis.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 0 minor

Summary. The paper proposes a novel definition of responsibility for program behaviors based on abstraction of event-trace semantics. An entity ER is responsible for behavior B iff ER is free to choose its input value and that choice is the first one ensuring B occurs in all forthcoming executions. The approach is claimed to be more precise than dependency/taint/slicing analyses or structural equation models of causality, and to incorporate the observer's cognizance.

Significance. If the abstraction is shown to soundly preserve ordering and the universal 'ensures' quantification, the definition could yield a strictly more precise static responsibility analysis for security applications than classical dependency or causality methods, while the inclusion of observer cognizance is a potentially useful extension.

major comments (2)
  1. [Abstract] Abstract (and introduction): the responsibility definition requires that the event-trace abstraction preserves both temporal ordering of choices and the universal quantification implicit in 'ensures' (B holds on every possible continuation). The manuscript supplies neither the concrete trace semantics nor the abstract domain/operators, so it is impossible to verify that the computed 'first ensuring choice' coincides with the concrete semantics or is strictly more precise than dependency/causality analyses.
  2. [Abstract] The claim that the definition 'takes into account the cognizance of the observer' is introduced without a formalization of how observer knowledge is encoded in the abstraction or how it affects the 'first ensuring choice' computation; this is load-bearing for the novelty claim relative to existing analyses.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and constructive feedback. We address the major comments point by point below, agreeing that additional formal details are needed to support the claims.

read point-by-point responses

  1. Referee: [Abstract] Abstract (and introduction): the responsibility definition requires that the event-trace abstraction preserves both temporal ordering of choices and the universal quantification implicit in 'ensures' (B holds on every possible continuation). The manuscript supplies neither the concrete trace semantics nor the abstract domain/operators, so it is impossible to verify that the computed 'first ensuring choice' coincides with the concrete semantics or is strictly more precise than dependency/causality analyses.

    Authors: We agree that the current version of the manuscript does not supply the concrete event-trace semantics or the abstract domain and operators. This makes independent verification of the preservation properties and the precision claims difficult. In the revised manuscript we will add a dedicated section presenting the concrete trace semantics, the abstract domain, the abstraction and concretization functions, and a proof sketch that the abstraction preserves temporal ordering of choices together with the universal quantification in 'ensures'. This addition will also make the comparison with dependency, taint, slicing and SEM-based causality analyses explicit. revision: yes

  2. Referee: [Abstract] The claim that the definition 'takes into account the cognizance of the observer' is introduced without a formalization of how observer knowledge is encoded in the abstraction or how it affects the 'first ensuring choice' computation; this is load-bearing for the novelty claim relative to existing analyses.

    Authors: We concur that the observer-cognizance aspect must be formalized to substantiate the novelty claim. The revised manuscript will contain an explicit definition of observer knowledge as a component of the abstract state, together with the rules showing how this component restricts the set of possible continuations when computing the 'first ensuring choice'. The formalization will be integrated into the responsibility definition and used in the precision arguments. revision: yes

Circularity Check

0 steps flagged

Novel responsibility definition introduced as fresh construction on event-trace abstraction

full rationale

The paper states its central contribution directly as a definition: 'an entity ER is responsible for behavior B, if and only if ER is free to choose its input value, and such a choice is the first one that ensures the occurrence of B in the forthcoming execution.' This is presented as a novel proposal based on abstraction of event trace semantics and does not reduce by construction to any fitted input, self-citation chain, or prior result within the text. No equations equate the responsibility predicate to its own inputs, and the abstraction step is not shown to be tautological. Standard self-citations to abstract-interpretation foundations are present but not load-bearing for the responsibility definition itself, which remains an independent definitional step.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The claim rests on the domain assumption that event-trace semantics can be abstracted to yield a responsibility notion that is both precise and cognizant of the observer; no free parameters or invented entities are visible in the abstract.

axioms (1)
  • domain assumption Event trace semantics of programs can be abstracted without loss of the information needed to define responsibility
    The definition is obtained by abstracting event trace semantics.

pith-pipeline@v0.9.0 · 5722 in / 1078 out tokens · 23370 ms · 2026-05-24T19:03:29.652300+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

51 extracted references · 51 canonical work pages

  1. [1]

    In: POPL

    Abadi, M., Banerjee, A., Heintze, N., Riecke, J.G.: A core calculus of dependency. In: POPL. pp. 147–160. ACM (1999)

    work page 1999

  2. [2]

    In: PLDI

    Agrawal, H., Horgan, J.R.: Dynamic program slicing. In: PLDI. pp. 246–256. ACM (1990)

    work page 1990

  3. [3]

    PACMPL 1(ICFP), 21:1–21:29 (2017)

    Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.: A relational logic for higher-order programs. PACMPL 1(ICFP), 21:1–21:29 (2017)

    work page 2017

  4. [4]

    In: POPL

    Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: localizing errors in counterexample traces. In: POPL. pp. 97–105. ACM (2003)

    work page 2003

  5. [5]

    Oxford University Press (2009)

    Beebee, H., Hitchcock, C., Menzie, P.: The Oxford Handbook of Causation. Oxford University Press (2009)

    work page 2009

  6. [6]

    Formal Methods in System Design 40(1), 20–40 (2012)

    Beer, I., Ben-David, S., Chockler, H., Orni, A., Trefler, R.J.: Explaining counterex- amples using causality. Formal Methods in System Design 40(1), 20–40 (2012)

    work page 2012

  7. [7]

    In: IJCAI

    Chen, B., Pearl, J., Bareinboim, E.: Incorporating knowledge into structural equa- tion models using auxiliary variables. In: IJCAI. pp. 3577–3583. IJCAI/AAAI Press (2016)

    work page 2016

  8. [8]

    Mathe- matical Structures in Computer Science 21(6), 1301–1337 (2011)

    Cheney, J., Ahmed, A., Acar, U.A.: Provenance as dependency analysis. Mathe- matical Structures in Computer Science 21(6), 1301–1337 (2011)

    work page 2011

  9. [9]

    Chockler, H., Halpern, J.Y.: Responsibility and blame: A structural-model ap- proach. J. Artif. Intell. Res. 22, 93–115 (2004)

    work page 2004

  10. [10]

    Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? ACM Trans. Comput. Log. 9(3), 20:1–20:26 (2008)

    work page 2008

  11. [11]

    Studies in Systems, Decision and Control 22, Springer (2015)

    Christopher, W.J.: Structural Equation Models, From Paths to Networks. Studies in Systems, Decision and Control 22, Springer (2015)

    work page 2015

  12. [12]

    In: POPL

    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL. pp. 238–252. ACM (1977)

    work page 1977

  13. [13]

    In: POPL

    Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL. pp. 269–282. ACM Press (1979) 20 C. Deng, P. Cousot

    work page 1979

  14. [14]

    Cousot, P., Cousot, R.: Abstract interpretation and application to logic programs. J. Log. Program. 13(2&3), 103–179 (1992)

    work page 1992

  15. [15]

    In: PLDI

    Dillig, I., Dillig, T., Aiken, A.: Automated error diagnosis using abductive infer- ence. In: PLDI. pp. 181–192. ACM (2012)

    work page 2012

  16. [16]

    In: USENIX Security Symposium

    Frankle, J., Park, S., Shaar, D., Goldwasser, S., Weitzner, D.J.: Practical account- ability of secret processes. In: USENIX Security Symposium. pp. 657–674. USENIX Association (2018)

    work page 2018

  17. [17]

    In: IEEE Sym- posium on Security and Privacy

    Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Sym- posium on Security and Privacy. pp. 11–20. IEEE Computer Society (1982)

    work page 1982

  18. [18]

    Greitschus, M., Dietsch, D., Podelski, A.: Loop invariants from counterexamples. In: SAS. Lecture Notes in Computer Science, vol. 10422, pp. 128–147. Springer (2017)

    work page 2017

  19. [19]

    Griesmayer, A., Staber, S., Bloem, R.: Automated fault localization for C pro- grams. Electr. Notes Theor. Comput. Sci. 174(4), 95–111 (2007)

    work page 2007

  20. [20]

    STTT 8(3), 229–247 (2006)

    Groce, A., Chaki, S., Kroening, D., Strichman, O.: Error explanation with distance metrics. STTT 8(3), 229–247 (2006)

    work page 2006

  21. [21]

    Halpern, J.Y., Pearl, J.: Causes and explanations: A structural-model approach: Part 1: Causes. In: UAI. pp. 194–202. Morgan Kaufmann (2001)

    work page 2001

  22. [22]

    part i: Causes

    Halpern, J.Y., Pearl, J.: Causes and explanations: A structural-model approach. part i: Causes. The British journal for the philosophy of science 56(4), 843–887 (2005)

    work page 2005

  23. [23]

    In: ICSE

    Hangal, S., Lam, M.S.: Tracking down software bugs using automatic anomaly detection. In: ICSE. pp. 291–301. ACM (2002)

    work page 2002

  24. [24]

    Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: CAV. Lecture Notes in Computer Science, vol. 8044, pp. 36–52. Springer (2013)

    work page 2013

  25. [25]

    London: A

    Hume, D.: An enquiry concerning human understanding. London: A. Millar (1748), http://www.davidhume.org/texts/ehu.html

    work page

  26. [26]

    In: ESORICS

    Jagadeesan, R., Jeffrey, A., Pitcher, C., Riely, J.: Towards a theory of accountability and audit. In: ESORICS. Lecture Notes in Computer Science, vol. 5789, pp. 152–

    work page

  27. [27]

    In: TACAS

    Jin, H., Ravi, K., Somenzi, F.: Fate and free will in error traces. In: TACAS. Lecture Notes in Computer Science, vol. 2280, pp. 445–459. Springer (2002)

    work page 2002

  28. [28]

    In: PLDI

    Jose, M., Majumdar, R.: Cause clue clauses: error localization using maximum satisfiability. In: PLDI. pp. 437–446. ACM (2011)

    work page 2011

  29. [29]

    In: SIGSOFT FSE

    King, D., Jaeger, T., Jha, S., Seshia, S.A.: Effective blame for information-flow violations. In: SIGSOFT FSE. pp. 250–260. ACM (2008)

    work page 2008

  30. [30]

    Information & Software Technology 40(11-12), 647–659 (1998)

    Korel, B., Rilling, J.: Dynamic program slicing methods. Information & Software Technology 40(11-12), 647–659 (1998)

    work page 1998

  31. [31]

    The journal of philosophy 70(17), 556–567 (1973)

    Lewis, D.: Causation. The journal of philosophy 70(17), 556–567 (1973)

    work page 1973

  32. [32]

    In: Zalta, E.N

    Menzies, P.: Counterfactual theories of causation. In: Zalta, E.N. (ed.) The Stan- ford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, winter 2017 edn. (2017)

    work page 2017

  33. [33]

    Cambridge University Press, 2nd edn

    Pearl, J.: Causality: Models, Reasoning and Inference. Cambridge University Press, 2nd edn. (2013)

    work page 2013

  34. [34]

    In: ECOOP

    Pistoia, M., Flynn, R.J., Koved, L., Sreedhar, V.C.: Interprocedural analysis for privileged code placement and tainted variable detection. In: ECOOP. Lecture Notes in Computer Science, vol. 3586, pp. 362–386. Springer (2005)

    work page 2005

  35. [35]

    Plotkin, G.D.: A structural approach to operational semantics. J. Log. Algebr. Program. 60-61, 17–139 (2004) Responsibility Analysis by Abstract Interpretation 21

    work page 2004

  36. [36]

    In: ESEC/SIGSOFT FSE

    Qi, D., Roychoudhury, A., Liang, Z., Vaswani, K.: Darwin: an approach for debug- ging evolving programs. In: ESEC/SIGSOFT FSE. pp. 33–42. ACM (2009)

    work page 2009

  37. [37]

    In: TACAS

    Ravi, K., Somenzi, F.: Minimal assignments for bounded model checking. In: TACAS. Lecture Notes in Computer Science, vol. 2988, pp. 31–45. Springer (2004)

    work page 2004

  38. [38]

    Renieris, M., Reiss, S.P.: Fault localization with nearest neighbor queries. In: ASE. pp. 30–39. IEEE Computer Society (2003)

    work page 2003

  39. [39]

    Rival, X.: Understanding the origin of alarms in astr´ ee. In: SAS. Lecture Notes in Computer Science, vol. 3672, pp. 303–319. Springer (2005)

    work page 2005

  40. [40]

    Oxford Monographs in International Law, Oxford University Press (2012)

    van Sliedregt, E.: Individual Criminal Responsibility in International Law. Oxford Monographs in International Law, Oxford University Press (2012)

    work page 2012

  41. [41]

    In: VMCAI

    Urban, C., Min´ e, A.: Proving guarantee and recurrence temporal properties by abstract interpretation. In: VMCAI. Lecture Notes in Computer Science, vol. 8931, pp. 190–208. Springer (2015)

    work page 2015

  42. [42]

    In: ESOP

    Urban, C., M¨ uller, P.: An abstract interpretation framework for input data usage. In: ESOP. Lecture Notes in Computer Science, vol. 10801, pp. 683–710. Springer (2018)

    work page 2018

  43. [43]

    Urban, C., Ueltschi, S., M¨ uller, P.: Abstract interpretation of CTL properties. In: SAS. Lecture Notes in Computer Science, vol. 11002, pp. 402–422. Springer (2018)

    work page 2018

  44. [44]

    In: ICSE

    Weiser, M.: Program slicing. In: ICSE. pp. 439–449. IEEE Computer Society (1981)

    work page 1981

  45. [45]

    IEEE Trans

    Weiser, M.: Program slicing. IEEE Trans. Software Eng. 10(4), 352–357 (1984)

    work page 1984

  46. [46]

    Weitzner, D.J., Abelson, H., Berners-Lee, T., Feigenbaum, J., Hendler, J.A., Suss- man, G.J.: Information accountability. Commun. ACM 51(6), 82–87 (2008) A Appended Proofs A.1 Proof of Galois Isomorphism (1) ⟨℘(S Max), ⊆⟩ − − − − − − − − −→ − →← ← − − − − − − − − − − αPredJS MaxK γPredJS MaxK ⟨¯αPredJS MaxK(℘(S Max)), ⊆⟩ Proof. First, we prove that αPredJ...

    work page 2008

  47. [47]

    This implies that ∀τe ∈ S Pref

    τ ̸∈ Pref(P). This implies that ∀τe ∈ S Pref. τe ̸∈ Pref(P), which further implies that ∀τe ∈ S Pref. τe ̸∈αPredJS MaxK(P). Since τ ∈ S Pref \S Max, there must exist at least one e such that τe ∈ S Pref ∧τe ̸∈αPredJS MaxK(P)

    work page

  48. [48]

    Take e = σ′ |τ|, then τe ∈ S Pref ∧ τe ⪯ σ′ ∧σ′ ̸∈ P holds, which implies τe ∈ S Pref ∧ τe ̸∈αPredJS MaxK(P)

    There is a maximal trace σ′ ∈ S Max such that τ ≺ σ′ ∧σ′ ̸∈ P . Take e = σ′ |τ|, then τe ∈ S Pref ∧ τe ⪯ σ′ ∧σ′ ̸∈ P holds, which implies τe ∈ S Pref ∧ τe ̸∈αPredJS MaxK(P). Both two cases find that ∃τe ∈ S Pref.τ e ̸∈αPredJS MaxK(P), which contradicts with the assumption ∀τe ∈ S Pref. τe ∈αPredJS MaxK(P). Corollary 3. For any cognizance C, we have · ⋃ e∈E...

    work page

  49. [49]

    By the definition of I in (2), we know that σ ̸∈ αPredJS MaxK(P) and ∀σe ∈ S Pref

    assume I(S Max, LMax,σ ) ⊋ ·∪{I(S Max, LMax,σ e) | σe ∈ S Pref } = P. By the definition of I in (2), we know that σ ̸∈ αPredJS MaxK(P) and ∀σe ∈ S Pref. σe ∈αPredJS MaxK(P), which is impossible by lemma. 6. Thus, by contradiction, I(S Max, LMax,σ ) = ·∪{I(S Max, LMax,σ e) |σe ∈ S Pref }. Lemma 7. Given the semantics S Max, the lattice LMax of system behavi...

    work page

  50. [50]

    Then the iteration marks similarly the nodes ℓa 3 and ℓb

    = P¬b. Then the iteration marks similarly the nodes ℓa 3 and ℓb

    work page

  51. [51]

    Should that eventuality analysis fail, the mark would be ⊤Max

    The nodes ℓ2 and ℓ1 are marked Pb/P¬b if the eventuality analyzer provides a guarantee that Pb and P¬b will definitely be reachable. Should that eventuality analysis fail, the mark would be ⊤Max. ⊓ ⊔ B.7 Abstract Responsibility Analysis For an abstract behavior B of interest, the responsibility analysis searches each of the paths that satisfy the abstracti...

    work page