Trusted declassification: High-level policy for a security-typed language

Boniface Hicks, Dave King, Patrick Drew McDaniel, Michael Hicks

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

24 Citations (Scopus)

Abstract

Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterference which ensures that high-security data will not be observable on low-security channels. Because noninterference is typically too strong a property, most programs use some form of declassification to selectively leak high security information, e.g. when performing a password check or data encryption. Unfortunately, such a declassification is often expressed as an operation within a given program, rather than as part of a global policy, making reasoning about the security implications of a policy more difficult. In this paper, we propose a simple idea we call trusted declassification in which special declassifier functions are specified as part of the global policy. In particular, individual principals declaratively specify which declassifies they trust so that all information flows implied by the policy can be reasoned about in absence of a particular program. We formalize our approach for a Java-like language and prove a modified form of noninterference which we call noninterference modulo trusted methods. We have implemented our approach as an extension to Jif and provide some of our experience using it to build a secure e-mail client.

Original languageEnglish (US)
Title of host publicationPLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop
Pages65-74
Number of pages10
StatePublished - Jul 20 2006
EventPLAS 2006 - 2006 Programming Languages and Analysis for Security Workshop - Ottawa, ON, Canada
Duration: Jun 10 2006Jun 10 2006

Publication series

NamePLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop
Volume2006

Other

OtherPLAS 2006 - 2006 Programming Languages and Analysis for Security Workshop
CountryCanada
CityOttawa, ON
Period6/10/066/10/06

Fingerprint

Application programs
Cryptography

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Cite this

Hicks, B., King, D., McDaniel, P. D., & Hicks, M. (2006). Trusted declassification: High-level policy for a security-typed language. In PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop (pp. 65-74). (PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop; Vol. 2006).
Hicks, Boniface ; King, Dave ; McDaniel, Patrick Drew ; Hicks, Michael. / Trusted declassification : High-level policy for a security-typed language. PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop. 2006. pp. 65-74 (PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop).
@inproceedings{21c3889ce9e742f4906cafaf43196271,
title = "Trusted declassification: High-level policy for a security-typed language",
abstract = "Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterference which ensures that high-security data will not be observable on low-security channels. Because noninterference is typically too strong a property, most programs use some form of declassification to selectively leak high security information, e.g. when performing a password check or data encryption. Unfortunately, such a declassification is often expressed as an operation within a given program, rather than as part of a global policy, making reasoning about the security implications of a policy more difficult. In this paper, we propose a simple idea we call trusted declassification in which special declassifier functions are specified as part of the global policy. In particular, individual principals declaratively specify which declassifies they trust so that all information flows implied by the policy can be reasoned about in absence of a particular program. We formalize our approach for a Java-like language and prove a modified form of noninterference which we call noninterference modulo trusted methods. We have implemented our approach as an extension to Jif and provide some of our experience using it to build a secure e-mail client.",
author = "Boniface Hicks and Dave King and McDaniel, {Patrick Drew} and Michael Hicks",
year = "2006",
month = "7",
day = "20",
language = "English (US)",
isbn = "1595933743",
series = "PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop",
pages = "65--74",
booktitle = "PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop",

}

Hicks, B, King, D, McDaniel, PD & Hicks, M 2006, Trusted declassification: High-level policy for a security-typed language. in PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop. PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop, vol. 2006, pp. 65-74, PLAS 2006 - 2006 Programming Languages and Analysis for Security Workshop, Ottawa, ON, Canada, 6/10/06.

Trusted declassification : High-level policy for a security-typed language. / Hicks, Boniface; King, Dave; McDaniel, Patrick Drew; Hicks, Michael.

PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop. 2006. p. 65-74 (PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop; Vol. 2006).

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

TY - GEN

T1 - Trusted declassification

T2 - High-level policy for a security-typed language

AU - Hicks, Boniface

AU - King, Dave

AU - McDaniel, Patrick Drew

AU - Hicks, Michael

PY - 2006/7/20

Y1 - 2006/7/20

N2 - Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterference which ensures that high-security data will not be observable on low-security channels. Because noninterference is typically too strong a property, most programs use some form of declassification to selectively leak high security information, e.g. when performing a password check or data encryption. Unfortunately, such a declassification is often expressed as an operation within a given program, rather than as part of a global policy, making reasoning about the security implications of a policy more difficult. In this paper, we propose a simple idea we call trusted declassification in which special declassifier functions are specified as part of the global policy. In particular, individual principals declaratively specify which declassifies they trust so that all information flows implied by the policy can be reasoned about in absence of a particular program. We formalize our approach for a Java-like language and prove a modified form of noninterference which we call noninterference modulo trusted methods. We have implemented our approach as an extension to Jif and provide some of our experience using it to build a secure e-mail client.

AB - Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterference which ensures that high-security data will not be observable on low-security channels. Because noninterference is typically too strong a property, most programs use some form of declassification to selectively leak high security information, e.g. when performing a password check or data encryption. Unfortunately, such a declassification is often expressed as an operation within a given program, rather than as part of a global policy, making reasoning about the security implications of a policy more difficult. In this paper, we propose a simple idea we call trusted declassification in which special declassifier functions are specified as part of the global policy. In particular, individual principals declaratively specify which declassifies they trust so that all information flows implied by the policy can be reasoned about in absence of a particular program. We formalize our approach for a Java-like language and prove a modified form of noninterference which we call noninterference modulo trusted methods. We have implemented our approach as an extension to Jif and provide some of our experience using it to build a secure e-mail client.

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

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

M3 - Conference contribution

AN - SCOPUS:33745957768

SN - 1595933743

SN - 9781595933744

T3 - PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop

SP - 65

EP - 74

BT - PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop

ER -

Hicks B, King D, McDaniel PD, Hicks M. Trusted declassification: High-level policy for a security-typed language. In PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop. 2006. p. 65-74. (PLAS 2006 - Proceedings of the 2006 Programming Languages and Analysis for Security Workshop).