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.
CITATION STYLE
Gregersen, S., Thomsen, S. E., & Askarov, A. (2019). A Dependently Typed Library for Static Information-Flow Control in Idris. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11426 LNCS, pp. 51–75). Springer Verlag. https://doi.org/10.1007/978-3-030-17138-4_3
Mendeley helps you to discover research relevant for your work.