Abstract—The security literature offers a multitude of calculi, languages, and systems for information-flow control, each with some set of labels encoding security policies that can be attached to data and computations. The exact form of these labels varies widely, with different systems offering many different combinations of features addressing issues such as confidentiality, integrity, and policy ownership. This variation makes it difficult to compare the expressive power of different information-flow frameworks. To enable such comparisons, we introduce label algebras, act interface for information-flow labels equipped with a notion of authority, and study several notions of embedding between them. The simplest is a straightforward notion of injection between label algebras, but this lacks a clear computational motivation and rejects some reasonable encodings between label models. We obtain a more refined account by defining a space of encodings parameterized by an interpre...
Benoît Montagu, Benjamin C. Pierce, Randy Pol