Security issues are a growing concern in an increasingly connected society. Given the central role played by programming languages in the implementation of information technology systems, introducing such matters early in the specification phase of programs could have a significant impact on their reliability.

To address this problem, the authors introduce relational Hoare type theory (RHTT), a typing framework that combines dependent typing (types may depend on values) with a logic for asserting confidentiality policies in programs. Using languages equipped with this formalism, programmers may specify and check that their programs satisfy sophisticated information flow properties such as authentication, authorization, or declassification. Within RHTT, data is labeled as either high (confidential) or low (public), with the goal of ensuring that programs do not leak any sensitive information. RHTT assertions are relational predicates in which the behaviors of two arbitrary runs of a program can be related, paving the way to the specification of the program’s noninterference property: a low output must not depend on high inputs, thus preventing information leakage. The logic part of RHTT makes reasoning about such properties possible. The overall system has been formally specified, and the authors have machine-checked its soundness, using the Coq theorem prover.

While this abstract, theoretical paper addresses an important issue, the audience is likely limited to researchers well versed in type theory and automated proof assistants. However, even though the material is dense, the authors have done a good job of presenting it in a pedagogical manner.