A Dependently Typed Library for Static Information-Flow Control in Idris

TL;DR

This paper introduces DepSec, a dependently typed library in Idris that enhances static information-flow control by leveraging dependent types for increased expressiveness and flexible declassification policies.

Contribution

DepSec is the first dependently typed library for static information-flow control in Idris, enabling more expressive and powerful security policies compared to prior libraries.

Findings

DepSec matches a specialized dependent information-flow type system on key examples.

Dependent types increase the expressiveness of static information-flow control.

Novel methods for specifying statically enforced declassification policies using dependent types.

Abstract

Safely integrating third-party code in applications while protecting the confidentiality of information is a long-standing problem. Pure functional programming languages, like Haskell, make it possible to enforce lightweight information-flow control through libraries like MAC by Russo. This work presents DepSec, a MAC inspired, dependently typed library for static information-flow control in Idris. We showcase how adding dependent types increases the expressiveness of state-of-the-art static information-flow control libraries and how DepSec matches a special-purpose dependent information-flow type system on a key example. Finally, we show novel and powerful means of specifying statically enforced declassification policies using dependent types.