Type-Based Declassification for Free

Minh Ngo; David A. Naumann; Tamara Rezk

doi:10.1007/978-3-030-63406-3_11

Type-Based Declassification for Free

Minh Ngo
, David A. Naumann
, Tamara Rezk

Department of Computer Science

Stevens Institute of Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Proceedings
Editors	Shang-Wei Lin, Zhe Hou, Brendan Mahoney
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	181-197
Number of pages	17
ISBN (Print)	9783030634056
DOIs	https://doi.org/10.1007/978-3-030-63406-3_11
State	Published - 2020
Event	22nd International Conference on Formal Engineering Methods, ICFEM 2020 - Singapore, Singapore Duration: Mar 1 2020 → Mar 3 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12531 LNCS

Conference

Conference	22nd International Conference on Formal Engineering Methods, ICFEM 2020
Country/Territory	Singapore
City	Singapore
Period	3/1/20 → 3/3/20

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-030-63406-3_11

Cite this

Ngo, M., Naumann, D. A., & Rezk, T. (2020). Type-Based Declassification for Free. In S.-W. Lin, Z. Hou, & B. Mahoney (Eds.), Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Proceedings (pp. 181-197). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12531 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-63406-3_11

Ngo, Minh ; Naumann, David A. ; Rezk, Tamara. / Type-Based Declassification for Free. Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Proceedings. editor / Shang-Wei Lin ; Zhe Hou ; Brendan Mahoney. Springer Science and Business Media Deutschland GmbH, 2020. pp. 181-197 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{85c72e95f29b4b6689aceb6fd4bd4cb6,

title = "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{\textquoteright} abstraction theorem.",

author = "Minh Ngo and Naumann, \{David A.\} and Tamara Rezk",

note = "Publisher Copyright: {\textcopyright} 2020, Springer Nature Switzerland AG.; 22nd International Conference on Formal Engineering Methods, ICFEM 2020 ; Conference date: 01-03-2020 Through 03-03-2020",

year = "2020",

doi = "10.1007/978-3-030-63406-3\_11",

language = "English",

isbn = "9783030634056",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "181--197",

editor = "Shang-Wei Lin and Zhe Hou and Brendan Mahoney",

booktitle = "Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Proceedings",

}

Ngo, M, Naumann, DA & Rezk, T 2020, Type-Based Declassification for Free. in S-W Lin, Z Hou & B Mahoney (eds), Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12531 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 181-197, 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, 3/1/20. https://doi.org/10.1007/978-3-030-63406-3_11

Type-Based Declassification for Free. / Ngo, Minh; Naumann, David A.; Rezk, Tamara.
Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Proceedings. ed. / Shang-Wei Lin; Zhe Hou; Brendan Mahoney. Springer Science and Business Media Deutschland GmbH, 2020. p. 181-197 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12531 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Type-Based Declassification for Free

AU - Ngo, Minh

AU - Naumann, David A.

AU - Rezk, Tamara

PY - 2020

Y1 - 2020

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

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

UR - https://www.scopus.com/pages/publications/85098256771

UR - https://www.scopus.com/pages/publications/85098256771#tab=citedBy

U2 - 10.1007/978-3-030-63406-3_11

DO - 10.1007/978-3-030-63406-3_11

M3 - Conference contribution

SN - 9783030634056

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 181

EP - 197

BT - Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Proceedings

A2 - Lin, Shang-Wei

A2 - Hou, Zhe

A2 - Mahoney, Brendan

PB - Springer Science and Business Media Deutschland GmbH

T2 - 22nd International Conference on Formal Engineering Methods, ICFEM 2020

Y2 - 1 March 2020 through 3 March 2020

ER -

Ngo M, Naumann DA, Rezk T. Type-Based Declassification for Free. In Lin SW, Hou Z, Mahoney B, editors, Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Proceedings. Springer Science and Business Media Deutschland GmbH. 2020. p. 181-197. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-63406-3_11

Type-Based Declassification for Free

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this