CoChat
Sign Up
PreprintCited by 0Security and Verification in ComputingLogic, programming, and type systemsAccess Control and Trust

Nonmalleable Information Flow: Technical Report

Open access
Cecchetti, Ethan, Myers, Andrew C., Arden, Owen·2017·arXiv
DOI 10.48550/arxiv.1708.08596arXiv 1708.08596
Open this paper in CoChat — free account

Abstract

Noninterference is a popular semantic security condition because it offers strong end-to-end guarantees, it is inherently compositional, and it can be enforced using a simple security type system. Unfortunately, it is too restrictive for real systems. Mechanisms for downgrading information are needed to capture real-world security requirements, but downgrading eliminates the strong compositional security guarantees of noninterference. We introduce nonmalleable information flow, a new formal security condition that generalizes noninterference to permit controlled downgrading of both confidentiality and integrity. While previous work on robust declassification prevents adversaries from exploiting the downgrading of confidentiality, our key insight is transparent endorsement, a mechanism for downgrading integrity while defending against adversarial exploitation. Robust declassification appeared to break the duality of confidentiality and integrity by making confidentiality depend on integrity, but transparent endorsement makes integrity depend on confidentiality, restoring this duality. We show how to extend a security-typed programming language with transparent endorsement and prove that this static type system enforces nonmalleable information flow, a new security property that subsumes robust declassification and transparent endorsement. Finally, we describe an implementation of this type system in the context of Flame, a flow-limited authorization plugin for the Glasgow Hask…

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

DataCite · 10.48550/arxiv.1708.08596

Cites

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • Non-malleability is the property, absent from dynamic IFC models, that an adversary controlling only low-integrity data cannot trigger a downgrade; Cecchetti et al. [15] formalize it and TMA-NM instantiates it for agent memory.

    “Non-malleability is the property, absent from those dynamic IFC models, that an adversary controlling only low-integrity data cannot trigger a downgrade, which Cecchetti et al. [15] formalize and we instantiate for agent memory.”

    From Securing LLM-Agent Long-Term Memory Against Poisoning: Non-Malleable, Origin-Bound Authority with Machine-Checked Guarantees (2026) · cites this paper as [15]

    The Introduction (p. 2) says adversarial influence over the decision to declassify is dangerous, and §6.6 (p. 19) formalizes nonmalleable information flow. But §6.6 also permits previously downgraded data, including endorsed attacker input, to influence later downgrades, so ‘cannot trigger a downgrade’ is too absolute. The cited passages do not establish that the property is absent specifically from dynamic IFC models; the agent-memory instantiation is the citing authors’ own claim. (LLM, conf=0.85)

    Experimental — accuracy not yet measured

  • We instantiate nonmalleable IFC [15] (robust declassification, transparent endorsement) for LLM-agent memory, to our knowledge the first such instantiation.

    “We instantiate nonmalleable IFC [15] (robust declassification, transparent endorsement) for LLM-agent memory, to our knowledge the first such instantiation.”

    From Securing LLM-Agent Long-Term Memory Against Poisoning: Non-Malleable, Origin-Bound Authority with Machine-Checked Guarantees (2026) · cites this paper as [15]

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

The citation lists haven’t been fetched yet

Research works printed but not linked: 42

  1. [1][1] Mart´ ın Abadi. 2006. Access Control in a Core Calculus of Dependency. In 11 th ACM SIGPLAN Int'l Conf. on Functional Programming . ACM, New York, NY, USA, 263-273. -
  2. [2][2] Mart´ ın Abadi. 2008. Variations in Access Control Logic. In Deontic Logic in Computer Science , Ron van der Meyden and Leendert van der Torre (Eds.). Lecture Notes in Computer Science, Vol. 5076. Springer Berlin Heidelberg, 96-109. -
  3. [3][3] Mart´ ın Abadi, Anindya Banerjee, Nevin Heintze, and Jon Riecke. 1999. A Core Calculus of Dependency. In 26 th ACM Symp. on Principles of Programming Languages (POPL) . 147-160. -
  4. [4][4] Owen Arden, Jed Liu, and Andrew C. Myers. 2015. Flow-Limited Authorization. In 28 th IEEE Symp. on Computer Security Foundations (CSF) . 569-583. -
  5. [5][5] Owen Arden and Andrew C. Myers. 2016. A Calculus for Flow-Limited Authorization. In 29 th IEEE Symp. on Computer Security Foundations (CSF) . 135-147. -
  6. [8][8] Niklas Broberg and David Sands. 2010. Paralocks-Role-Based Information Flow Control and Beyond. In 37 th ACM Symp. on Principles of Programming Languages (POPL) . -
  7. [9][9] Pablo Buiras, Dimitrios Vytiniotis, and Alejandro Russo. 2015. HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell. In 20 th ACM SIGPLAN Int'l Conf. on Functional Programming . ACM, 289-301. -
  8. [10][10] Stephen Chong and Andrew C. Myers. 2006. Decentralized Robustness. In 19 th IEEE Computer Security Foundations Workshop (CSFW) . 242-253. -
  9. [11][11] Stephen Chong and Andrew C. Myers. 2008. End-to-End Enforcement of Erasure and Declassification. In IEEE Symp. on Computer Security Foundations (CSF) . 98-111. -
  10. [12][12] Michael R. Clarkson and Fred B. Schneider. 2008. Hyperproperties. In IEEE Symp. on Computer Security Foundations (CSF) . 51-65. -
  11. [13][13] Dorothy E. Denning. 1976. A Lattice Model of Secure Information Flow. Comm. of the ACM 19, 5 (1976), 236-243. -
  12. [14][14] Danny Dolev, Cynthia Dwork, and Moni Naor. 2003. Nonmalleable Cryptography. SIAM Rev. 45, 4 (2003), 727-784. -
  13. [15][15] Petros Efstathopoulos, Maxwell Krohn, Steve VanDeBogart, Cliff Frey, David Ziegler, Eddie Kohler, David Mazi` eres, Frans Kaashoek, and Robert Morris. 2005. Labels and Event Processes in the Asbestos Operating System. In 20 th ACM Symp. on Operating System Principles (SOSP) . -
  14. [16][16] Michael D. Ernst, Ren´ e Just, Suzanne Millstein, Werner Dietl, Stuart Pernsteiner, Franziska Roesner, Karl Koscher, Paulo Barros, Ravi Bhoraskar, Seungyeop Han, Paul Vines, and Edward X. Wu. 2014. Collaborative Verification of Information Flow for a High-Assurance App Store. In 21 st ACM Conf. on Computer and Communications Security (CCS) . 1092-1104. -
  15. [17][17] David Ferraiolo and Richard Kuhn. 1992. Role-Based Access Controls. In 15th National Computer Security Conference . -
  16. [18][18] Joseph A. Goguen and Jose Meseguer. 1982. Security Policies and Security Models. In IEEE Symp. on Security and Privacy . 11-20. -
  17. [19][19] Limin Jia, Jeffrey A. Vaughan, Karl Mazurak, Jianzhou Zhao, Luke Zarko, Joseph Schorr, and Steve Zdancewic. 2008. Aura: A Programming Language for Authorization and Audit. In 13 th ACM SIGPLAN Int'l Conf. on Functional Programming . -
  18. [21][21] Maxwell Krohn, Alexander Yip, Micah Brodsky, Natan Cliffer, M. Frans Kaashoek, Eddie Kohler, and Robert Morris. 2007. Information Flow Control for Standard OS Abstractions. In 21 st ACM Symp. on Operating System Principles (SOSP) . -
  19. [22][22] Peng Li and Steve Zdancewic. 2006. Encoding information flow in Haskell. In 19 th IEEE Computer Security Foundations Workshop (CSFW) . -
  20. [23][23] Benoˆ ıt Montagu, Benjamin C. Pierce, and Randy Pollack. 2013. A Theory of Information-Flow Labels. In 26 th IEEE Symp. on Computer Security Foundations (CSF) . 3-17. -
  21. [24][24] Andrew C. Myers. 1999. JFlow: Practical Mostly-Static Information Flow Control. In 26 th ACMSymp. on Principles of Programming Languages (POPL) . 228-241. -
  22. [25][25] Andrew C. Myers and Barbara Liskov. 2000. Protecting Privacy using the Decentralized Label Model. ACM Transactions on Software Engineering and Methodology 9, 4 (Oct. 2000), 410-442. -
  23. [26][26] Andrew C. Myers, Andrei Sabelfeld, and Steve Zdancewic. 2006. Enforcing Robust Declassification and Qualified Robustness. Journal of Computer Security 14, 2 (2006), 157-196. -
  24. [27][27] Aleksandar Nanevski, Anindya Banerjee, and Deepak Garg. 2011. Verification of Information Flow and Access Control Policies with Dependent Types. In IEEE Symp. on Security and Privacy . 165-179. -
  25. [28][28] Sylvan Pinsky. 1995. Absorbing Covers and Intransitive Non-Interference. In IEEE Symp. on Security and Privacy . 102-113. -
  26. [29][29] Franc ¸ois Pottier and Sylvain Conchon. 2000. Information Flow Inference for Free. In 5 th ACM SIGPLAN Int'l Conf. on Functional Programming (ICFP '00) . 46-57. -
  27. [30][30] Franc ¸ois Pottier and Vincent Simonet. 2003. Information Flow Inference for ML. ACM Trans. on Programming Languages and Systems 25, 1 (Jan. 2003). -
  28. [31][31] A. W. Roscoe and M. H. Goldsmith. 1999. What is Intransitive Noninterference?. In 12 th IEEE Computer Security Foundations Workshop (CSFW) . 228-238. -
  29. [32][32] Indrajit Roy, Donald E. Porter, Michael D. Bond, Kathryn S. McKinley, and Emmett Witchel. 2009. Laminar: Practical Fine-Grained Decentralized Information Flow Control. In ACMSIGPLAN Conf. on Programming Language Design and Implementation (PLDI) . -
  30. [34][34] Andrei Sabelfeld and Andrew C. Myers. 2003. Language-Based Information-Flow Security. IEEE Journal on Selected Areas in Communications 21, 1 (Jan. 2003), 5-19. -
  31. [35][35] Andrei Sabelfeld and David Sands. 2005. Dimensions and Principles of Declassification. In 18 th IEEE Computer Security Foundations Workshop (CSFW) . 255-269. -
  32. [37][37] Marcelo Sousa and Isil Dillig. 2016. Cartesian Hoare logic for verifying k -safety properties. In SIGPLAN Notices , Vol. 51. ACM, 57-69. -
  33. [38][38] Deian Stefan, Amit Levy, Alejandro Russo, and David Mazi` eres. 2014. Building Secure Systems with LIO. In Haskell Symposium . ACM SIGPLAN. -
  34. [39][39] Nikhil Swamy, Michael Hicks, Stephen Tse, and Steve Zdancewic. 2006. Managing Policy Updates in Security-Typed Languages. In 19 th IEEE Computer Security Foundations Workshop (CSFW) . 202216. -
  35. [41][41] Ron van der Meyden. 2007. What, Indeed, Is Intransitive Noninterference?. In 12 th European Symposium on Research in Computer Security (ESORICS) . 235-250. n P N (atomic principals) x P V (variable names) <!-- formula-not-decoded --> -
  36. [42][42] Lucas Waye, Pablo Buiras, Dan King, Stephen Chong, and Alejandro Russo. 2015. It's My Privilege: Controlling Downgrading in DC-Labels. In Proceedings of the 11th International Workshop on Security and Trust Management . -
  37. [43][43] J. Todd Wittbold and Dale M. Johnson. 1990. Information Flow in Nondeterministic Systems. In IEEE Symp. on Security and Privacy . 144-161. -
  38. [44][44] Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115, 1 (1994), 38-94. -
  39. [45][45] Steve Zdancewic and Andrew C. Myers. 2001. Robust Declassification. In 14 th IEEE Computer Security Foundations Workshop (CSFW) . 15-23. -
  40. [46][46] Steve Zdancewic, Lantian Zheng, Nathaniel Nystrom, and Andrew C. Myers. 2002. Secure Program Partitioning. ACM Trans. on Computer Systems 20, 3 (Aug. 2002), 283-328. -
  41. [47][47] Nickolai Zeldovich, Silas Boyd-Wickizer, Eddie Kohler, and David Mazi` eres. 2006. Making Information Flow Explicit in HiStar. In 7 th USENIX Symp. on Operating Systems Design and Implementation (OSDI) . 263-278. -
  42. [48][48] Lantian Zheng and Andrew C. Myers. 2007. Dynamic Security Labels and Static Information Flow Control. International Journal of Information Security 6, 2-3 (March 2007).

Authors
Cecchetti, E., Myers, A. C., & Arden, O.
ORCID
Venue
arXiv
Publisher
arXiv
Published
2017
ISSN
2331-8422 (ISSN-L)
DOI
10.48550/arxiv.1708.08596
arXiv
1708.08596
OpenAlex
W6891853219
Cited by
0
References
0
Type
posted content
Language
en
Open access
Licence
arxiv.org/licenses/nonexclusive-distrib/1.0/
Locations
arXiv (Cornell University)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Security and Verification in Computing
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Social Sciences › Sociology and Political Science › Access Control and Trust
Keywords
non-interference, information flow security, type systems, static analysis, compositional security, flames

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review