Options
Taming message-passing communication in compositional reasoning about confidentiality
Publikationstyp
Conference Paper
Date Issued
2017-11
Sprache
English
Author(s)
First published in
Number in series
10695 LNCS
Start Page
45
End Page
66
Citation
Lecture Notes in Computer Science 10695 LNCS: 45-66 (2017)
Contribution to Conference
Publisher DOI
Scopus ID
Publisher
Springer International Publishing AG
We propose a solution for verifying the information-flow security of distributed programs in a compositional manner. Our focus is on the treatment of message passing in such a verification, and our goal is to boost the precision of modular reasoning using rely-guarantee-style reasoning. Enabling a more precise treatment of message passing required the identification of novel concepts that capture assumptions about how a process’s environment interacts. Our technical contributions include a process-local security condition that allows one to exploit such assumptions when analyzing individual processes, a security type system that is sensitive in the content as well as in the availability of messages, and a soundness proof for our security type system. Our results complement existing solutions for rely-guarantee-style reasoning about information-flow security that focused on multi-threading and shared memory.
DDC Class
004: Informatik