Li, XimengXimengLiMantel, HeikoHeikoMantelTasch, MarkusMarkusTasch2022-10-252022-10-252017-11Lecture Notes in Computer Science 10695 LNCS: 45-66 (2017)http://hdl.handle.net/11420/13837We 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.enInformatikConference Paper10.1007/978-3-319-71237-6_3Other