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

Standard

A Dependently Typed Library for Static Information-Flow Control in IDRIS. / Gregersen, Simon Oddershede; Thomsen, Søren Eller; Askarov, Aslan.

Principles 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. ed. / Flemming Nielson; David Sands. Cham : Springer, 2019. p. 51-75 (Lecture Notes in Computer Science, Vol. 11426).

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

Harvard

Gregersen, SO, Thomsen, SE & Askarov, A 2019, A Dependently Typed Library for Static Information-Flow Control in IDRIS. in F Nielson & D Sands (eds), Principles 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. Springer, Cham, Lecture Notes in Computer Science, vol. 11426, pp. 51-75, 8th International Conference on Principles of Security and Trust , Prag, Czech Republic, 11/04/2019. https://doi.org/10.1007/978-3-030-17138-4_3

APA

Gregersen, S. O., Thomsen, S. E., & Askarov, A. (2019). A Dependently Typed Library for Static Information-Flow Control in IDRIS. In F. Nielson, & D. Sands (Eds.), Principles 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 (pp. 51-75). Springer. Lecture Notes in Computer Science Vol. 11426 https://doi.org/10.1007/978-3-030-17138-4_3

CBE

Gregersen SO, Thomsen SE, Askarov A. 2019. A Dependently Typed Library for Static Information-Flow Control in IDRIS. Nielson F, Sands D, editors. In Principles 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. Cham: Springer. pp. 51-75. (Lecture Notes in Computer Science, Vol. 11426). https://doi.org/10.1007/978-3-030-17138-4_3

MLA

Gregersen, Simon Oddershede, Søren Eller Thomsen, and Aslan Askarov "A Dependently Typed Library for Static Information-Flow Control in IDRIS". and Nielson, Flemming Sands, David (editors). Principles 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. Cham: Springer. (Lecture Notes in Computer Science, Vol. 11426). 2019, 51-75. https://doi.org/10.1007/978-3-030-17138-4_3

Vancouver

Gregersen SO, Thomsen SE, Askarov A. A Dependently Typed Library for Static Information-Flow Control in IDRIS. In Nielson F, Sands D, editors, Principles 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. Cham: Springer. 2019. p. 51-75. (Lecture Notes in Computer Science, Vol. 11426). https://doi.org/10.1007/978-3-030-17138-4_3

Author

Gregersen, Simon Oddershede ; Thomsen, Søren Eller ; Askarov, Aslan. / A Dependently Typed Library for Static Information-Flow Control in IDRIS. Principles 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. editor / Flemming Nielson ; David Sands. Cham : Springer, 2019. pp. 51-75 (Lecture Notes in Computer Science, Vol. 11426).

Bibtex

@inproceedings{509b4f64791c453c81eea05ab73f2c4b,
title = "A Dependently Typed Library for Static Information-Flow Control in IDRIS",
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.",
keywords = "Dependent types, Idris, Information-flow control",
author = "Gregersen, {Simon Oddershede} and Thomsen, {S{\o}ren Eller} and Aslan Askarov",
year = "2019",
doi = "10.1007/978-3-030-17138-4_3",
language = "English",
isbn = "978-3-030-17137-7",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "51--75",
editor = "Nielson, {Flemming } and Sands, {David }",
booktitle = "Principles of Security and Trust",
note = "8th International Conference on Principles of Security and Trust ; Conference date: 11-04-2019 Through 11-04-2019",
url = "https://www.etaps.org/2019/post",

}

RIS

TY - GEN

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

AU - Gregersen, Simon Oddershede

AU - Thomsen, Søren Eller

AU - Askarov, Aslan

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - Dependent types

KW - Idris

KW - Information-flow control

U2 - 10.1007/978-3-030-17138-4_3

DO - 10.1007/978-3-030-17138-4_3

M3 - Article in proceedings

SN - 978-3-030-17137-7

T3 - Lecture Notes in Computer Science

SP - 51

EP - 75

BT - Principles of Security and Trust

A2 - Nielson, Flemming

A2 - Sands, David

PB - Springer

CY - Cham

T2 - 8th International Conference on Principles of Security and Trust

Y2 - 11 April 2019 through 11 April 2019

ER -