Aarhus University Seal / Aarhus Universitets segl

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

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Documents

DOI

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.

Original languageEnglish
Title of host publicationPrinciples of Security and Trust : 8th International Conference, POST 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
EditorsFlemming Nielson, David Sands
Number of pages25
Place of publicationCham
PublisherSpringer
Publication year2019
Pages51-75
ISBN (print)978-3-030-17137-7
DOIs
Publication statusPublished - 2019
Event8th International Conference on Principles of Security and Trust - Prag, Czech Republic
Duration: 11 Apr 201911 Apr 2019
https://www.etaps.org/2019/post

Conference

Conference8th International Conference on Principles of Security and Trust
LandCzech Republic
ByPrag
Periode11/04/201911/04/2019
Internetadresse
SeriesLecture Notes in Computer Science
Volume11426
ISSN0302-9743

    Research areas

  • Dependent types, Idris, Information-flow control

See relations at Aarhus University Citationformats

Download statistics

No data available

ID: 179742116