Polymorphic Relaxed Noninterference

International audienceInformation-flow security typing statically preservesconfidentiality by enforcing noninterference. To address the practical need of selective and flexible declassification of confidentialinformation, several approaches have developed a notion of relaxed non interference, where security labels are either functionsor types. The labels-as-types approach to relaxed non interference supports expressive declassification policies, including recursiveones, via a simple subtyping-based ordering, and provides alocal, modular reasoning principle. In this work, we extend this expressive declassification approach in order to support polymorphic declassification. First, we identify the need for bounded polymorphism through concrete examples. We then formalize polymorphic relaxed non interference in a typed object-oriented calculus, using a step-indexed logical relation to prove that allwell-typed terms are secure. Finally, we address the case of primitive types, which requires a form of ad-hoc polymorphism.Therefore, this work addresses practical hurdles to providing controlled and expressive declassification for the construction of information-flow secure system