Taming Message-Passing Communication in Compositional Reasoning About Confidentiality

DOI10.1007/978-3-319-71237-6_3MaRDI QIDQ5055995zbMATH OpenOpenAlexFDO

Authors Ximeng Li, Heiko Mantel, Markus Tasch

Publication date 9 December 2022

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-71237-6_3

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Rely-guarantee based reasoning for message-passing programs
• scientific article; zbMATH DE number 1948408
• Timing-Sensitive Noninterference through Composition
• Combining Different Proof Techniques for Verifying Information Flow Security
• Modular reasoning for message-passing programs

Cites work

• Disjunctive Information Flow for Communicating Processes
• Distributed systems. Principles and paradigms.
• scientific article; zbMATH DE number 1670564 (Why is no real title available?)
• scientific article; zbMATH DE number 3776831 (Why is no real title available?)
• scientific article; zbMATH DE number 1538026 (Why is no real title available?)
• scientific article; zbMATH DE number 1884409 (Why is no real title available?)
• On flow-sensitive security types
• Proving the Correctness of Multiprocess Programs
• Session types for access and information flow control
• Type-based information flow analysis for the \(\pi\)-calculus
• Using dynamic pushdown networks to automate a modular information-flow analysis

Cited in

(5)

• Causing communication closure: safe program composition with reliable non-FIFO channels
• Modular reasoning for message-passing programs
• Combining Different Proof Techniques for Verifying Information Flow Security
• Rely-guarantee based reasoning for message-passing programs
• Towards Secrecy for Rewriting in Weakly Adhesive Categories

This page was built for publication: Taming Message-Passing Communication in Compositional Reasoning About Confidentiality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055995)