Note on a simple type system for non-interference

TL;DR

This paper proposes a simple type system for CCS with value passing that models noninterference by viewing channels as information carriers, allowing secret emissions to be safe while input may cause leakage.

Contribution

It introduces a novel noninterference notion for process calculi that aligns with programming language concepts by treating channels as information carriers.

Findings

Channels as information carriers enable safe secret emissions.

Input actions may cause information leakage, reflecting realistic security concerns.

The type system effectively distinguishes safe and unsafe information flows.

Abstract

We consider CCS with value passing and elaborate a notion of noninterference for the process calculi, which matches closely that of the programming language. The idea is to view channels as information carriers rather than as "events", so that emitting a secret on output channel can be considered safe, while inputting a secret may lead to some kind of leakage. This is in contrast with the standard notion of noninterference for the process calculi where any causal dependency of low-level action from any high-level action is forbidden.