Article

A Simple View of Type-Secure Information Flow in the "-Calculus

Author:

François PottierAuthors Info & Claims

CSFW '02: Proceedings of the 15th IEEE workshop on Computer Security Foundations

Page 320

Published: 24 June 2002 Publication History

Abstract

One way of enforcing an information flow control policy is to use a static type system capable of guaranteeing a noninterference property. Noninterference requires that two processes with distinct "high"-level components, but common "low"-level structure, cannot be distinguished by "low"-level observers. We state this property in terms of a rather strict notion of process equivalence, namely weak barbed reduction congruence.Because noninterference is not a safety property, it is often regarded as more difficult to establish than a conventional type safety result. This paper aims to provide an elementary noninterference roof in the setting of the calculus. This is done by reducing the problem to subject reduction "a safety property" for a nonstandard, but fairly natural, extension of the calculus, baptized the ( )-calculus.

References

[1]

M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke. A core calculus of dependency. In Conference Record of the 26th ACM Symposium on Principles of Prognmming Languages , pages 147-160, San Antonio, Texas, Jan. 1999. ACM Press. URL: http://www.soe.ucsc.edu/~abadi/ Papers/flowpopl.ps.

Digital Library

[2]

M. Abadi, B. Lampson, and J.-J. Lévy. Analysis and caching of dependencies. In Proceedings of the 1996 ACM SIGPLAN International Conference on Functional Programming , pages 83-91, Philadelphia, Pennsylvania, May 1996. ACM Press. URL: http://www.soe.ucsc.edu/~abadi/ Papers/make-preprint.ps.

Digital Library

[3]

D. E. Bell and L. J. LaPadula. Secure computer systems: Unified exposition and Multics interpretation. Technical Report MTR-2997, The MITRE Corp., Bedford, Massachusetts, July 1975. URL: http://www.mitre.org/ resources/centers/infosec/infosec.html.

[4]

C. Bodei, P. Degano, F. Nielson, and H. R. Nielson. Static analysis of processes for no read-up and no write-down. In W. Thomas, editor, Proceedings of FoSSaCS'99 , volume 1578 of Lecture Notes in Computer Science , pages 120-134. Springer, Mar. 1999. URL: http://www.di.unipi.it/ ~chiara/publ-40/BDNN99.ps.

Digital Library

[5]

G. Boudol and I. Castellani. Non-interference for concurrent programs and thread systems. To appear. URL: ftp://ftp-sop.inria.fr/mimosa/personnel/ gbo/non-interf-threads.ps.gz, Sept. 2001.

[6]

D. E. Denning. Cryptography and Data Security . Addison-Wesley, Reading, Massachusetts, 1982.

Digital Library

[7]

R. Focardi and R. Gorrieri. A classification of security properties for process algebras. Journal of Computer Security , 3(1):5-33, 1995. URL:http://www.cs.unibo.it/ ~gorrieri/Papers/jcsfinal.ps.gz.

Digital Library

[8]

M. Hennessy. The security picalculus and noninterference. Technical Report 2000:05, University of Sussex, Nov. 2000. URL: ftp://ftp.cogs.susx.ac.uk/ pub/reports/compsci/cs052000.ps.z.

[9]

M. Hennessy and J. Riely. Information flow vs. resource access in the asynchronous pi-calculus. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming , Lecture Notes in Computer Science. Springer-Verlag, July 2000. URL: http://www.depaul. edu/~jriely/papers/00icalp.ps.gz.

Digital Library

[10]

M. Hepburn and D. Wright. Trust in the pi-calculus. In Third International Conference on Principles and Practice of Declarative Programming (PPDP'01) , Sept. 2001.

Digital Library

[11]

K. Honda, V. Vasconcelos, and N. Yoshida. Secure information flow as typed process behaviour. In G. Smolka, editor, Proceedings of the 2000 European Symposium on Programming (ESOP '00) , volume 1782 of Lecture Notes in Computer Science , pages 180-199. Springer Verlag, Mar. 2000. URL: ftp://ftp.des.qmw.ae.uk/1fp/kohei/ siftp-esop00.ps.gz.

Digital Library

[12]

K. Honda and N. Yoshida. A uniform type structure for secure information flow. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL'02) , pages 81-92, Portland, Oregon, Jan. 2002. URL: http://www.mcs.le.ae.uk/~nyoshida/paper/ ifa1.ps.gz.

Digital Library

[13]

A. Igarashi and N. Kobayashi. Type reconstruction for linear ¿-calculus with I/O subtyping. Information & Computation , 161:1-44, Aug. 2000. URL: http://www.graeo.c.u-tokyo.ac.jp/~igarashi/ papers/LinearPi.ps.gz.

Digital Library

[14]

N. Kobayashi, B. C. Pierce, and D. N. Turner. Linearity and the Pi-Calculus. ACM Transactions on Programming Languages and Systems , 21(5):914-947, Sept. 1999. URL: http://www.acm.org/pubs/citations/ journals/toplas/1999-21-5/p914-kobayashi/.

Digital Library

[15]

J. McLean. A general theory of composition for trace sets closed under selective interleaving functions. In Proceedings of the 1994 IEEE Symposium on Research in Security and Privacy . IEEE Press, 1994. URL: http://chacs.nrl.navy.mil/ publications/CHACS/1994/1994mclean-sp.ps.

Digital Library

[16]

R. Milner. The polyadic ¿-calculus: a tutorial. Technical Report ECS-LFCS-91-180, Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh, Oct. 1991. URL: ftp://ftp.cl. cam.ac.uk/users/rm135/ppi.ps.Z.

[17]

R. Milner and D. Sangiorgi. Barbed bisimulation. In W. Kuich, editor, International Colloquium on Automata, Languages and Programming , volume 623 of Lecture Notes in Computer Science , pages 685-695, Vienna, Austria, July 1992. Springer-Verlag. URL: ftp://ftp-sop.inria.fr/ meije/theorie-par/davides/bn.ps.gz.

Digital Library

[18]

B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. In Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science , pages 376-385, June 1993. URL:http://www.cis.upenn.edu/~bepierce/ papers/pi-lies.ps.

[19]

F. Pottier. A simple view of type-secure information flow in the ¿-calculus. Full version. URL: http://pauillac.inria.fr/~fpottier/publis/ fpottier-csfw15-long.ps.gz, Feb. 2002.

Digital Library

[20]

F. Pottier and S. Conchon. Information flow inference for free. In Proceedings of the the 5th ACM SIGPLAN International Conference on Functional Programming (ICFP'00) , pages 46-57, Montreal, Canada, Sept. 2000. ACM Press. URL: http://pauillac.inria.fr/~fpottier/ publis/fpottier-conchon-icfp00.ps.gz.

Digital Library

[21]

F. Pottier and V. Simonet. Information flow inference for ML. In Proceedings of the 29th ACM Symposium on Principles of Programming Languages (POPL'02) , pages 319-330, Portland, Oregon, Jan. 2002. ACM Press. URL: http://pauillac.inria.fr/~fpottier/ publis/fpottier-simonet-pop102.ps.gz.

Digital Library

[22]

P. Sewell and J. Vitek. Secure composition of untrusted code: Wrappers and causality types. In Proceedings of the 13th Computer Security Foundations Workshop . IEEE Computer Society Press, July 2000. URL: http://www.cl. cam.ac.uk/users/pes20/wraptypes.ps.gz.

Digital Library

[23]

G. Smith and D. Volpano. Secure information flow in a multi-threaded imperative language. In Conference Record of the 25th ACM Symposium on Principles of Programming Languages , pages 355-364, Jan. 1998. URL: http://www.cs.nps.navy.mil/people/ faculty/volpano/papers/pop198.ps.Z.

Digital Library

[24]

G. S. Smith. A new type system for secure information flow. In Proc. 14th IEEE Computer Security Foundations Workshop , pages 115-125, Cape Breton, Nova Scotia, June 2001. URL: http://www.es.fiu.edu/~smithg/ papers/csfw01.ps.gz.

Digital Library

[25]

N. Yoshida. Graph types for monadic mobile processes. In V. Chandru and V. Vinay, editors, Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science , volume 1180 of Lecture Notes in Computer Science , pages 371-386. Springer-Verlag, 1996. URL: http://www.mcs.le.ac. uk/~nyoshida/paper/graphl_short.ps.gz.

Digital Library

[26]

N. Yoshida, K. Honda, and M. Berger. Linearity and bisimulation. Technical Report MSC-2001/48, University of Leicester, Dec. 2001. URL: http://www.mcs.le.ac.uk/ ~nyoshida/paper/lb.ps.gz.

[27]

N. Yoshida, K. Honda, and M. Berger. Linearity and bisimulation. In Proceedings of 5th International Conference of Foundations of Software Science and Computer Structures (FoSSaCs 2002) , Lecture Notes in Computer Science. Springer Verlag, Apr. 2002. URL: http://www.mcs.le. ac.uk/~nyoshida/paper/fossacs_ca_final.ps.gz.

Digital Library

[28]

S. Zdancewic and A. C. Myers. Secure information flow and CPS. In D. Sands, editor, Proceedings of the 2001 European Symposium on Programming (ESOP'01) , Lecture Notes in Computer Science, Genova, Italy, Apr. 2001. Springer Verlag. URL: http://www.cs.cornell.edu/ zdance/lincont.ps.

Digital Library

Cited By

Derakhshan FBalzer SJia LGorla D(2021)Session logical relations for noninterferenceProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470654(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/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
Vassena MRusso AMurray TStefan D(2016)On Formalizing Information-Flow Control LibrariesProceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security10.1145/2993600.2993608(15-28)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2993600.2993608
Show More Cited By

A Simple View of Type-Secure Information Flow in the "-Calculus
1. Security and privacy
  1. Systems security

Recommendations

A Multi-type Calculus for Inquisitive Logic
Proceedings of the 23rd International Workshop on Logic, Language, Information, and Computation - Volume 9803

In this paper, we define a multi-type calculus for inquisitive logic, which is sound, complete and enjoys Belnap-style cut-elimination and subformula property. Inquisitive logic is the logic of inquisitive semantics, a semantic framework developed by ...
Run-time principals in information-flow type systems

Information-flow type systems are a promising approach for enforcing strong end-to-end confidentiality and integrity policies. Such policies, however, are usually specified in terms of static information—data is labeled high or low security at compile ...
A sequent calculus for type theory
CSL'06: Proceedings of the 20th international conference on Computer Science Logic

Based on natural deduction, Pure Type Systems (PTS) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent Calculi (PTSC) by enriching a sequent calculus due to Herbelin, adapted ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CSFW '02: Proceedings of the 15th IEEE workshop on Computer Security Foundations

June 2002

ISBN:0769516890

Copyright © Copyright (c) 2002 Institute of Electrical and Electronics Engineers, Inc. All rights reserved.

Publisher

IEEE Computer Society

United States

Publication History

Published: 24 June 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

23
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Derakhshan FBalzer SJia LGorla D(2021)Session logical relations for noninterferenceProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470654(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/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
Vassena MRusso AMurray TStefan D(2016)On Formalizing Information-Flow Control LibrariesProceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security10.1145/2993600.2993608(15-28)Online publication date: 24-Oct-2016
https://dl.acm.org/doi/10.1145/2993600.2993608
Pettai MLaud P(2013)Dynamics and Secure Information Flow for a Higher-Order Pi-CalculusProceedings of the 18th Nordic Conference on Secure IT Systems - Volume 820810.1007/978-3-642-41488-6_7(100-115)Online publication date: 18-Oct-2013
https://dl.acm.org/doi/10.1007/978-3-642-41488-6_7
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
Buiras PLevy AStefan DRusso AMazières D(2013)A Library for Removing Cache-Based Attacks in Concurrent Information Flow Systems8th International Symposium on Trustworthy Global Computing - Volume 835810.1007/978-3-319-05119-2_12(199-216)Online publication date: 30-Aug-2013
https://dl.acm.org/doi/10.1007/978-3-319-05119-2_12
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
Stefan DRusso ABuiras PLevy AMitchell JMaziéres D(2012)Addressing covert termination and timing channels in concurrent information flow systemsACM SIGPLAN Notices10.1145/2398856.236455747:9(201-214)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2398856.2364557
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
Stefan DRusso ABuiras PLevy AMitchell JMaziéres DThiemann PFindler R(2012)Addressing covert termination and timing channels in concurrent information flow systemsProceedings of the 17th ACM SIGPLAN international conference on Functional programming10.1145/2364527.2364557(201-214)Online publication date: 9-Sep-2012
https://dl.acm.org/doi/10.1145/2364527.2364557
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents