Deriving an information flow checker and certifying compiler for java

Gilles Barthe, David Naumann, Tamara Rezk

Research output: Chapter in Book/Report/Conference proceedingConference contribution

28 Citations (Scopus)

Abstract

Language-based security provides a means to enforce end-to-end confidentiality and integrity policies in mobile code scenarios, and is increasingly being contemplated by the smart-card and mobile phone industry as a solution to enforce information flow and resource control policies. Two threads of work have emerged in research on language-based security: work that focuses on enforcing security policies for source code, which is tailored towards developers that want to increase confidence in their applications, and work that focuses on efficiently verifying similar policies for byte-code, which is tailored to code consumers that want to protect themselves against hostile applications. These lines of work serve different purposes - and thus have been developed independently - but connecting them is a key step towards the deployment of language-based security in practical applications. This paper introduces a systematic technique to connect source code and bytecode security type systems. The technique is applied to an information flow type system for a fragment of Java with exceptions, thus confronting challenges in both control and data flow tracking.

Original languageEnglish (US)
Title of host publicationProceedings - 2006 IEEE Symposium on Security and Privacy, S+P 2006
Pages230-242
Number of pages13
DOIs
StatePublished - Nov 21 2006
Event2006 IEEE Symposium on Security and Privacy, S and P 2006 - Berkeley, United States
Duration: May 21 2006May 24 2006

Publication series

NameProceedings - IEEE Symposium on Security and Privacy
Volume2006

Other

Other2006 IEEE Symposium on Security and Privacy, S and P 2006
CountryUnited States
CityBerkeley
Period5/21/065/24/06

Fingerprint

Smart cards
Mobile phones
Industry

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Barthe, G., Naumann, D., & Rezk, T. (2006). Deriving an information flow checker and certifying compiler for java. In Proceedings - 2006 IEEE Symposium on Security and Privacy, S+P 2006 (pp. 230-242). [1624014] (Proceedings - IEEE Symposium on Security and Privacy; Vol. 2006). https://doi.org/10.1109/SP.2006.13
Barthe, Gilles ; Naumann, David ; Rezk, Tamara. / Deriving an information flow checker and certifying compiler for java. Proceedings - 2006 IEEE Symposium on Security and Privacy, S+P 2006. 2006. pp. 230-242 (Proceedings - IEEE Symposium on Security and Privacy).
@inproceedings{a69be1d1eaa243c79e00a1096b1d0869,
title = "Deriving an information flow checker and certifying compiler for java",
abstract = "Language-based security provides a means to enforce end-to-end confidentiality and integrity policies in mobile code scenarios, and is increasingly being contemplated by the smart-card and mobile phone industry as a solution to enforce information flow and resource control policies. Two threads of work have emerged in research on language-based security: work that focuses on enforcing security policies for source code, which is tailored towards developers that want to increase confidence in their applications, and work that focuses on efficiently verifying similar policies for byte-code, which is tailored to code consumers that want to protect themselves against hostile applications. These lines of work serve different purposes - and thus have been developed independently - but connecting them is a key step towards the deployment of language-based security in practical applications. This paper introduces a systematic technique to connect source code and bytecode security type systems. The technique is applied to an information flow type system for a fragment of Java with exceptions, thus confronting challenges in both control and data flow tracking.",
author = "Gilles Barthe and David Naumann and Tamara Rezk",
year = "2006",
month = "11",
day = "21",
doi = "https://doi.org/10.1109/SP.2006.13",
language = "English (US)",
isbn = "0769525741",
series = "Proceedings - IEEE Symposium on Security and Privacy",
pages = "230--242",
booktitle = "Proceedings - 2006 IEEE Symposium on Security and Privacy, S+P 2006",

}

Barthe, G, Naumann, D & Rezk, T 2006, Deriving an information flow checker and certifying compiler for java. in Proceedings - 2006 IEEE Symposium on Security and Privacy, S+P 2006., 1624014, Proceedings - IEEE Symposium on Security and Privacy, vol. 2006, pp. 230-242, 2006 IEEE Symposium on Security and Privacy, S and P 2006, Berkeley, United States, 5/21/06. https://doi.org/10.1109/SP.2006.13

Deriving an information flow checker and certifying compiler for java. / Barthe, Gilles; Naumann, David; Rezk, Tamara.

Proceedings - 2006 IEEE Symposium on Security and Privacy, S+P 2006. 2006. p. 230-242 1624014 (Proceedings - IEEE Symposium on Security and Privacy; Vol. 2006).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Deriving an information flow checker and certifying compiler for java

AU - Barthe, Gilles

AU - Naumann, David

AU - Rezk, Tamara

PY - 2006/11/21

Y1 - 2006/11/21

N2 - Language-based security provides a means to enforce end-to-end confidentiality and integrity policies in mobile code scenarios, and is increasingly being contemplated by the smart-card and mobile phone industry as a solution to enforce information flow and resource control policies. Two threads of work have emerged in research on language-based security: work that focuses on enforcing security policies for source code, which is tailored towards developers that want to increase confidence in their applications, and work that focuses on efficiently verifying similar policies for byte-code, which is tailored to code consumers that want to protect themselves against hostile applications. These lines of work serve different purposes - and thus have been developed independently - but connecting them is a key step towards the deployment of language-based security in practical applications. This paper introduces a systematic technique to connect source code and bytecode security type systems. The technique is applied to an information flow type system for a fragment of Java with exceptions, thus confronting challenges in both control and data flow tracking.

AB - Language-based security provides a means to enforce end-to-end confidentiality and integrity policies in mobile code scenarios, and is increasingly being contemplated by the smart-card and mobile phone industry as a solution to enforce information flow and resource control policies. Two threads of work have emerged in research on language-based security: work that focuses on enforcing security policies for source code, which is tailored towards developers that want to increase confidence in their applications, and work that focuses on efficiently verifying similar policies for byte-code, which is tailored to code consumers that want to protect themselves against hostile applications. These lines of work serve different purposes - and thus have been developed independently - but connecting them is a key step towards the deployment of language-based security in practical applications. This paper introduces a systematic technique to connect source code and bytecode security type systems. The technique is applied to an information flow type system for a fragment of Java with exceptions, thus confronting challenges in both control and data flow tracking.

UR - http://www.scopus.com/inward/record.url?scp=33751034907&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=33751034907&partnerID=8YFLogxK

U2 - https://doi.org/10.1109/SP.2006.13

DO - https://doi.org/10.1109/SP.2006.13

M3 - Conference contribution

SN - 0769525741

SN - 9780769525747

T3 - Proceedings - IEEE Symposium on Security and Privacy

SP - 230

EP - 242

BT - Proceedings - 2006 IEEE Symposium on Security and Privacy, S+P 2006

ER -

Barthe G, Naumann D, Rezk T. Deriving an information flow checker and certifying compiler for java. In Proceedings - 2006 IEEE Symposium on Security and Privacy, S+P 2006. 2006. p. 230-242. 1624014. (Proceedings - IEEE Symposium on Security and Privacy). https://doi.org/10.1109/SP.2006.13