Article

A uniform type structure for secure information flow

Authors:

Nobuko YoshidaAuthors Info & Claims

POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 81 - 92

https://doi.org/10.1145/503272.503281

Published: 01 January 2002 Publication History

Abstract

The π-calculus is a formalism of computing in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name passing. This work reports our experience in using a linear/affine typed π-calculus for the analysis and development of type systems of programming languages, focussing on secure information flow analysis. After presenting a basic typed calculus for secrecy, we demonstrate its usage by a sound embedding of the dependency core calculus (DCC) and by the development of a novel type discipline for imperative programs which extends both a secure multi-threaded imperative language by Smith and Volpano and (a call-by-value version of) DCC. In each case, the embedding gives a simple proof of noninterference.

References

[1]

Abadi, M., Secrecy in programming-language semantics, MFPS XV, ENTCS, 20 (April 1999).]]

[2]

Abadi, M., Banerjee, A., Heintze, N. and Riecke, J., A core calculus of dependency, POPL'99, ACM, 1999.]]

Digital Library

[3]

Abramsky, S., Jagadeesan, R. and Malacaria, P., Full Abstraction for PCF, 1994. Info. Comp. 163 (2000), 409-470.]]

Digital Library

[4]

Abramsky, S., Honda, K. and McCusker, G., Fully Abstract Game Semantics %r General Re%rences, LICS'98, 334-344, IEEE, 1998.]]

Digital Library

[5]

Agat, J. Transforming Out Timing Leaks, POPL'O0, 2000, ACM Press.]]

Digital Library

[6]

Berger, M., Honda, K. and Yoshida, N., Sequentiality and tile -Calculus, TLCA01, LNCS 2044, 29-45, Springer, 2001.]]

[7]

Boudol, G., Asynchrony and the pi-calculus, INRIA Research Report 1702, 1992.]]

[8]

Boudol, G. and Castellani, I., Noninterference for Concurrent Programs, ICALPO1, LNCS 2076, 382-395, Springer, 2001.]]

Digital Library

[9]

Denning, D. and Denning, P., Certification of programs for secure information flow. Communication of ACM, ACM, 20:504-513, 1997.]]

Digital Library

[10]

Focardi, R., Gorrieri, R. and Martinelli, F., Non-inter%rence for the analysis of cryptographic protocols. ICALPO0, LNCS 1853, Springer, 2000.]]

Digital Library

[11]

Girard, J.-Y., Linear Logic, TCS, Vol. 50, 1-102, 1987.]]

Digital Library

[12]

Heintze, N. and Riecke, J., The SLam calculus: programming with secrecy and integrity, POPL'98, 365-377, ACM, 1998.]]

Digital Library

[13]

Hennessy, M. and Riely, J., Information flow as resource access in the asynchronous pi-calculus, ICALPO0, LNCS 1853, 415-427, Springer, 2000.]]

Digital Library

[14]

Honda, K., Types for Dyadic Interaction. CONCUR'93, LNCS 715, 509-523, 1993.]]

Digital Library

[15]

Honda, K., Composing Processes, POPL'96, 344-357, ACM, 1996.]]

Digital Library

[16]

Honda, K., Kubo, M. and Vasconcelos, V., Language Primitives and Type Discipline for Structured Communication-Based Programming. ESOP'98, LNCS 1381, 122 138. Springer-Verlag, 1998.]]

Digital Library

[17]

Honda, K. and Tokoro, M. An object calculus asynchronous communication. ECOOP'91, LNCS 512, 133-147, 1991.]]

Digital Library

[18]

Honda, K., Vasconcelos, V. and Yoshida, N., Secure Information Flow as Typed Process Behaviour, ESOP'O0, LNCS 1782, 180 199, 2000.]]

Digital Library

[19]

Honda, K. and Yoshida, N. On Reduction-Based Process Semantics. TCS. 151,437-486, 1995.]]

Digital Library

[20]

Honda, K. and Yoshida, N. Game-theoretic analysis of call-by-value computation. TCS, 221 (1999), 393 456.]]

Digital Library

[21]

Howard, B. T., Inductive, coinductive, and pointed types, ICFP'96, 102 109, ACM, 1996.]]

Digital Library

[22]

The Haskell home page, http://haskell.org.]]

[23]

Hyland, M. and Ong, L., "On Full Abstraction for PCF": I, II and III. Info. Comp. 163 (2000), 285-408.]]

Digital Library

[24]

Kobayashi, N., Pierce, B., and Turner, D., Linear types and re-calculus, POPL'96, 358-371, 1996.]]

Digital Library

[25]

Milner, R., Functions as Processes, MSCS. 2(2):119 141, 1992,]]

[26]

Milner, R., Parrow, J. and Walker, D., A Calculus of Mobile Processes, Info. f3 Cornp. 100(1):1-77, 1992.]]

Digital Library

[27]

Mitchell, J., Foundations for Programming Languages MIT Press, 1996.]]

Digital Library

[28]

Palsberg, J. and 2~rbaek, J., Trust in the A-Calculus. JFP, 7(6):557-591, 1997.]]

Digital Library

[29]

Potter, F. and Conchon, S, Information flow inference for free, ICFPO0, 46-57, ACM, 2000.]]

Digital Library

[30]

Pierce, B and Sangiorgi.D, Typing and subtyping for mobile processes, MSCS 6(5):409-453, 1996.]]

[31]

Ryan, P. and Schneider, S. Process Algebra and Non-interference. CSFW'99, IEEE, 1999.]]

Digital Library

[32]

Sangiorgi, D. re-calculus, internal mobility, and agent-passing calculi. TCS, 167(2):235-271, 1996.]]

Digital Library

[33]

Sabelfield, A. and Sand, D. A per model of secure information flow in sequential programs. ESOP'99, LNCS 1576, Springer, 1999.]]

Digital Library

[34]

Smith, G., A New Type System for Secure Information Flow, CSFW'01, IEEE, 2001.]]

Digital Library

[35]

Smith, G. and Volpano, D., Secure information flow in a multi-threaded imperative language, 355-364, POPL'98, ACM, 1998.]]

Digital Library

[36]

ToKe, M., Type in%rence tbr polymorphic references, Info. f3 Conp., 89:1-34, 1990.]]

Digital Library

[37]

Vasconcelos, V., Typed concurrent objects. ECOOP'9d, LNCS 821, 100-117. Springer, 1994.]]

Digital Library

[38]

Volpano, D., Smith, G. and Irvine, C., A Sound type system for secure, flow analysis, a. Computer Security, 4(2,3):167-187, 1996.]]

Digital Library

[39]

Yoshida, N. Graph Types for Mobile Processes. FST/TCS'16, LNCS 1180, 371-386, Springer, 1996.]]

Digital Library

[40]

Yoshida, N., Berger, M. and Honda, K., Strong Normalisation in the re-Calculus, LICS'01, 311-322, (C1) (C2) (C3) IEEE, 2001.]]

[41]

Yoshida, N., Honda, K. and Berger, M., Linearity and Bisimulation, To appear as MCS technical report, Leicester, 2001.]]

[42]

Zdancewic, S. and Myers, A., Secure Information Flow and CPS, ESOP01, LNCS 2028, 46-62, Springer, 2001.]]

Digital Library

Cited By

Derakhshan FBalzer SJia L(2021)Session Logical Relations for Noninterference2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS52264.2021.9470654(1-14)Online publication date: 29-Jun-2021
https://doi.org/10.1109/LICS52264.2021.9470654
Rafnsson WJia LBauer L(2017)Timing-Sensitive Noninterference through CompositionProceedings of the 6th International Conference on Principles of Security and Trust - Volume 1020410.1007/978-3-662-54455-6_1(3-25)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54455-6_1
Rafnsson WSabelfeld A(2014)Compositional Information-Flow Security for Interactive SystemsProceedings of the 2014 IEEE 27th Computer Security Foundations Symposium10.1109/CSF.2014.27(277-292)Online publication date: 19-Jul-2014
https://dl.acm.org/doi/10.1109/CSF.2014.27
Show More Cited By

A uniform type structure for secure information flow
1. Theory of computation
  1. Semantics and reasoning

Recommendations

A uniform type structure for secure information flow

The π-calculus, a calculus of mobile processes, can compositionally represent dynamics of major programming constructs by decomposing them into name passing. The present work reports our experience in using a linear/affine typed π-calculus for the ...
A uniform type structure for secure information flow

The π-calculus is a formalism of computing in which we can compositionally represent dynamics of major programming constructs by decomposing them into a single communication primitive, the name passing. This work reports our experience in using a linear/...
A Haskell-Embedded DSL for Secure Information-Flow
Formal Methods: Foundations and Applications
Abstract
This paper presents a domain specific language, embedded in Haskell (EDSL), for enforcing the information flow policy Delimited Release. To build this language we use Haskell extensions that will allow some kind of dependently-typed programming.
...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '02: Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 2002

351 pages

ISBN:1581134509

DOI:10.1145/503272

Conference Chair:
John Launchbury
OGI and Galois Connections
,
Program Chair:
John C. Mitchell
Stanford University

ACM SIGPLAN Notices Volume 37, Issue 1
Jan. 2002
342 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/565816
Issue’s Table of Contents

Copyright © 2002 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL02

Sponsor:

POPL02: The 29th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages 2002

January 16 - 18, 2002

Oregon, Portland

Acceptance Rates

POPL '02 Paper Acceptance Rate 28 of 128 submissions, 22%;

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

83
Total Citations
View Citations
554
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Derakhshan FBalzer SJia L(2021)Session Logical Relations for Noninterference2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS52264.2021.9470654(1-14)Online publication date: 29-Jun-2021
https://doi.org/10.1109/LICS52264.2021.9470654
Rafnsson WJia LBauer L(2017)Timing-Sensitive Noninterference through CompositionProceedings of the 6th International Conference on Principles of Security and Trust - Volume 1020410.1007/978-3-662-54455-6_1(3-25)Online publication date: 22-Apr-2017
https://dl.acm.org/doi/10.1007/978-3-662-54455-6_1
Rafnsson WSabelfeld A(2014)Compositional Information-Flow Security for Interactive SystemsProceedings of the 2014 IEEE 27th Computer Security Foundations Symposium10.1109/CSF.2014.27(277-292)Online publication date: 19-Jul-2014
https://dl.acm.org/doi/10.1109/CSF.2014.27
Kobayashi N(2014)From Linear Types to Behavioural Types and Model CheckingConcurrent Objects and Beyond10.1007/978-3-662-44471-9_6(128-143)Online publication date: 2014
https://doi.org/10.1007/978-3-662-44471-9_6
Zdancewic S(2013)A Type System for Robust DeclassificationElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/S1571-0661(03)50014-783(263-277)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.1016/S1571-0661%2803%2950014-7
Hennessy M(2013)The Security Picalculus and Non-interference (Extended Abstract)Electronic Notes in Theoretical Computer Science (ENTCS)10.1016/S1571-0661(03)50006-883(113-129)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.1016/S1571-0661%2803%2950006-8
Duggan DWu Y(2013)Security Correctness for Secure Nested Transactions8th International Symposium on Trustworthy Global Computing - Volume 835810.1007/978-3-319-05119-2_5(64-79)Online publication date: 30-Aug-2013
https://dl.acm.org/doi/10.1007/978-3-319-05119-2_5
Muller SChong S(2012)Towards a practical secure concurrent languageACM SIGPLAN Notices10.1145/2398857.238462147:10(57-74)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2398857.2384621
Muller SChong SLeavens GDwyer M(2012)Towards a practical secure concurrent languageProceedings of the ACM international conference on Object oriented programming systems languages and applications10.1145/2384616.2384621(57-74)Online publication date: 19-Oct-2012
https://dl.acm.org/doi/10.1145/2384616.2384621
Rafnsson WHedin DSabelfeld A(2012)Securing Interactive ProgramsProceedings of the 2012 IEEE 25th Computer Security Foundations Symposium10.1109/CSF.2012.15(293-307)Online publication date: 25-Jun-2012
https://dl.acm.org/doi/10.1109/CSF.2012.15
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents