Polymorphic Relaxed Noninterference

No ratings

Presented at IEEESecDev 2019 by

Information-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 ofrelaxed noninterference, where security labels are either functionsor types. The labels-as-types approach to relaxed noninterferencesupports expressive declassification policies, including recursiveones, via a simple subtyping-based ordering, and provides alocal, modular reasoning principle. In this work, we extend thisexpressive declassification approach in order to support polymorphic declassification. First, we identify the need for boundedpolymorphism through concrete examples. We then formalizepolymorphic relaxed noninterference in a typed object-orientedcalculus, using a step-indexed logical relation to prove that allwell-typed terms are secure. Finally, we address the case ofprimitive types, which requires a form of ad-hoc polymorphism.Therefore, this work addresses practical hurdles to providingcontrolled and expressive declassification for the construction ofinformation-flow secure systems.