Noninterference in a predicative polymorphic calculus for access control

• A denotational semantics based on Henkin models is given for a predicative polymorphic calculus of access control.
• Noninterference as a basic semantic notion of security is semantically defined.
• It is proven that the language is type-sound in the sense that every welltyped program of the language satisfies noninterference.

Polymorphic programming languages have been adapted for constructing distributed access control systems, where a program represents a proof of eligibility according to a given policy. As a security requirement, it is typically stated that the programs of such languages should satisfy noninterference. However, this property has not been defined and proven semantically. In this paper, we first propose a semantics based on Henkin models for a predicative polymorphic access control language based on lambda-calculus. A formal semantic definition of noninterference is then proposed through logical relations. We prove a type soundness theorem which states that any well-typed program of our language meets the noninterference property defined in this paper. In this way, it is guaranteed that access requests from an entity do not interfere with those from unrelated or more trusted entities.