Skip to Main content Skip to Navigation
Conference papers

Type-based Declassification for Free

Abstract : This work provides a study to demonstrate the potential of using off-the-shelf programming languages and their theories to build sound language-based-security tools. Our study focuses on information flow security encompassing declassification policies that allow us to express flexible security policies needed for practical requirements. We translate security policies, with declassification, into an interface for which an unmodified standard typechecker can be applied to a source program---if the program typechecks, it provably satisfies the policy. Our proof reduces security soundness---with declassification---to the mathematical foundation of data abstraction, Reynolds' abstraction theorem.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03141398
Contributor : Tamara Rezk Connect in order to contact the contributor
Submitted on : Monday, February 15, 2021 - 11:36:49 AM
Last modification on : Wednesday, November 3, 2021 - 7:06:14 AM

Links full text

Identifiers

  • HAL Id : hal-03141398, version 1
  • ARXIV : 1905.00922

Citation

Minh Ngo, David A. Naumann, Tamara Rezk. Type-based Declassification for Free. ICFEM'20, Mar 2020, Singapore, Singapore. ⟨hal-03141398⟩

Share

Metrics

Les métriques sont temporairement indisponibles