Information flow security of multi-threaded distributed programs

We study noninterference in the setting of multi-threaded distributed programs in which threads share local memories and multi-threaded processes communicate over an insecure network using encryption primitives to secure messages. We extend a simple imperative language with cryptographic operations which are modelled as special expressions respecting the Dolev-Yao assumptions. Then, we adapt to our setting the notion of patterns proposed by Abadi and Rogaway for modelling the equivalence of cryptographic expressions. Based on this notion, we naturally obtain a definition of strongly secure programs corresponding to the one proposed by Sabelfeld and Sands for programs without cryptography. This is, to the best of our knowledge, the first definition of noninterference in a multi-threaded distributed setting, with insecure channels and cryptography. We prove compositionality of secure programs and we adapt the type system of Sabelfeld and Sands to our setting, proving its correctness.