Article

Statically assuring secrecy for dynamic concurrent processes

Authors:

Rachid Echahed,

Frédéric Prost,

Wendelin SerweAuthors Info & Claims

PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming

Pages 91 - 101

https://doi.org/10.1145/888251.888261

Published: 27 August 2003 Publication History

Abstract

We propose a new algorithm of secrecy analysis in a framework integrating declarative programming and concurrency. The analysis of a program ensures that information can only flow from less sensitive levels toward more sensitive ones. Our algorithm uses a terminating abstract operational semantics which reduces the problem of secrecy to constraint solving within finite lattices. It departs in that from the previous works essentially based on type systems. Furthermore, our proposal is general and tackles a very large class of programs, featuring dynamic process creation, general sequential composition, recursive process calls and high level synchronization.

References

[1]

J. Agat. Transforming out timing leaks. In Proceedings of the 27th ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL 2000), pages 40 -- 53, Boston, Jan. 2000. ACM.]]

Digital Library

[2]

J.-P. Banatre, C. Bryce, and D. L. Metayer. Compile-time detection of information flow in sequential programs. In D. Gollmann, editor, Computer Security, Proceedingd of the 3rd European Symposium on Research in Computer Security (ESORICS 94), volume 875 of Lecture Notes in Computer Science, pages 55 -- 73, Brighton, Nov. 1994. Springer Verlag.]]

Digital Library

[3]

A. Banerjee and D. A. Naumann. Secure information flow and pointer confinement in a java-like language. In Proceedings of the $15th IEEE Computer Security Foundations Workshop, Cape Breton, 2002.]]

Digital Library

[4]

D. E. Bell and L. J. LaPadula. Secure computer systems: Mathematical foundations. Technical Report ESD-TR-73-278 (Vol. I -- III), MITRE Corporation, Bedford, Apr. 1974.]]

[5]

G. Boudol and I. Castellani. Noninterference for concurrent programs and thread systems. Theoretical Computer Science, 281(1):109 -- 130, 2002. Special issue: "Merci, Maurice, A mosaic in honour of Maurice Nivat" (P.-L. Curien, Ed.).]]

Digital Library

[6]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL '77), pages 238 -- 252, Los Angeles, Jan. 1977. ACM.]]

Digital Library

[7]

D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Communications of the ACM, 20(7):504 -- 513, July 1977.]]

Digital Library

[8]

N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, chapter 6, pages 243 -- 320. Elsevier, Amsterdam, 1990.]]

Digital Library

[9]

A. Di Pierro, C. Hankin, and H. Wiklicky. Probabilistic confinement in a declarative framework. Electronic Notes in Theoretical Computer Science, 48, 2001.]]

[10]

A. Di Pierro, C. Hankin, and H. Wiklicky. Approximate non-interference. In Proceedings of the 15th IEEE Computer Security Foundations Workshop, Cape Breton, June 2002.]]

Digital Library

[11]

R. Echahed and W. Serwe. Combining mobile processes and declarative programming. In J. Lloyd et al., editors, Proceedings of the 1st International Conference on Computational Logic (CL 2000), volume 1861 of Lecture Notes in Artificial Intelligence, pages 300 -- 314, London, July 2000. Springer Verlag.]]

Digital Library

[12]

R. Echahed and W. Serwe. Integrating action definitions into concurrent declarative programming. Electronic Notes in Theoretical Computer Science, 64, Sept. 2002. special issue: selected papers of the International Workshop on Functional and (Constraint) Logic Programming (WFLP 2001).]]

[13]

R. Focardi, R. Gorrieri, and F. Martinelli. Non interference for the analysis of cryptographic protocols. In U. Montanari, J. D. P. Rolim, and E. Welzl, editors, Proceeding of the 27th International Colloquium on Automata, Languages and Programming (ICALP 2000), volume 1853 of Lecture Notes in Computer Science, pages 354 -- 372, Geneva, July 2000. Springer Verlag.]]

Digital Library

[14]

W. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science. Springer Verlag, 2000.]]

Digital Library

[15]

J. W. Gray, III. Probabilistic interference. In Proceedings of the 1990 IEEE Symposium on Security and Privacy, pages 170 -- 179, Oakland, May 1990. IEEE Computer Society Press.]]

[16]

A. C. Myers. JFlow: Practical mostly-static information flow control. In Proceedings of the 26th ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL '99), pages 228 -- 241, San Antonio, Jan. 1999.]]

Digital Library

[17]

F. Prost. A static calculus of dependencies for the λ-cube. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science (LICS '2000), pages 267 -- 276, Santa Barbara, 2000. IEEE Computer Society Press.]]

Digital Library

[18]

A. Sabelfeld. The impact of synchronisation on secure information flow in concurrent programs. In D. Bjorner, M. Broy, and A. V. Zamulin, editors, Perspectives of System Informatics, Proceedings of the 4th International Andrei Ershov Memorial Conference (PSI 2001), volume 2244 of Lecture Notes in Computer Science, pages 225 -- 239, Akademgorodok, July 2001. Springer Verlag.]]

Digital Library

[19]

A. Sabelfeld and H. Mantel. Static confidentiality enforcement for distributed programs. In M. V. Hermenegildo and G. Puebla, editors, Proceedings of the 9th International Symposium on Static Analysis (SAS 2002), volume 2477 of Lecture Notes in Computer Science, pages 376 -- 394, Madrid, Sept. 2002. Springer Verlag.]]

Digital Library

[20]

A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE Journal on Selected Areas in Communications, special issue on Design and Analysis Techniques for Security Assurance, 2002. to appear.]]

[21]

A. Sabelfeld and D. Sands. Probabilistic noninterference for multi-threaded programs. In Proceedings of the 13th IEEE Computer Security Foundations Workshop, pages 200 -- 214, Cambridge, July 2000.]]

Digital Library

[22]

W. Serwe. On Concurrent Functional-Logic Programming. these de doctorat, Institut National Polytechnique de Grenoble, Mar. 2002.]]

[23]

G. Smith. A new type system for secure information flow. In Proceedings of the 14th IEEE Computer Security Foundations Workshop, pages 115 -- 125, Cape Breton, June 2001. IEEE Computer Society Press.]]

Digital Library

[24]

G. Smith. Weak probabilistic bisimulation for secure information flow. In Proceedings of the Workshop on Issues in the Theory of Security (WITS '02), Portland, Jan. 2002.]]

[25]

G. Smith and D. M. Volpano. Secure information flow in a multi-threaded imperative language. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '98), pages 355 -- 364, San Diego, Jan. 1998.]]

Digital Library

[26]

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

Digital Library

[27]

D. M. Volpano and G. Smith. Probabilistic noninterference in a concurrent language. Journal of Computer Security, 7(2, 3):231 -- 253, Nov. 1999.]]

Digital Library

[28]

N. Yoshida, K. Honda, and M. Berger. Linearity and bisimulation. In M. Nielsen and U. Engberg, editors, Proceedings of the 5th International Conference on Foundations of Software Science and Computer Structures (FoSSaCs 2002), volume 2303 of Lecture Notes in Computer Science, pages 417 -- 434. Springer Verlag, Apr. 2002.]]

Digital Library

[29]

M. Zanotti. Security typings by abstract interpretation. In M. V. Hermenegildo and G. Puebla, editors, Proceedings of the 9th International Symposium on Static Analysis (SAS 2002), volume 2477 of Lecture Notes in Computer Science, pages 360 -- 375, Madrid, Sept. 2002. Springer Verlag.]]

Digital Library

Cited By

Prost F(2011)Enforcing Dynamic Interference Policy2011 IEEE Third Int'l Conference on Privacy, Security, Risk and Trust and 2011 IEEE Third Int'l Conference on Social Computing10.1109/PASSAT/SocialCom.2011.17(1111-1118)Online publication date: Oct-2011
https://doi.org/10.1109/PASSAT/SocialCom.2011.17
Echahed RProst FBarahona PFelty A(2005)Security policy in a declarative styleProceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming10.1145/1069774.1069789(153-163)Online publication date: 11-Jul-2005
https://dl.acm.org/doi/10.1145/1069774.1069789
Echahed RProst FMeadows C(2005)Handling declared information leakageProceedings of the 2005 workshop on Issues in the theory of security10.1145/1045405.1045406(1-4)Online publication date: 10-Jan-2005
https://dl.acm.org/doi/10.1145/1045405.1045406

Index Terms

Statically assuring secrecy for dynamic concurrent processes

Recommendations

Formal Reasoning about Concurrent Assembly Code with Reentrant Locks
TASE '09: Proceedings of the 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering

This paper focuses on the problem of reasoning about concurrent assembly code with reentrant locks. Our verification technique is based on concurrent separation logic (CSL). In CSL, locks are treated as non-reentrant locks and each lock is associated ...
Safety of Deferred Update in Transactional Memory
ICDCS '13: Proceedings of the 2013 IEEE 33rd International Conference on Distributed Computing Systems

Transactional memory allows the user to declare sequences of instructions as speculative transactions that can either commit or abort. If a transaction commits, it appears to be executed sequentially, so that the committed transactions constitute a ...
Freedom from Deadlock of Safe Locking Policies

The usual method for preserving the consistency of a database when accessed (read and updated) concurrently by several transactions, is by locking the transactions according to some locking policy; a locking policy that guarantees the preservation of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PPDP '03: Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming

August 2003

292 pages

ISBN:1581137052

DOI:10.1145/888251

Conference Chair:
Konstantinos Sagonas
Uppsala University, SW
,
Program Chair:
Dale Miller
INRIA/Futurs & Ecole Polytechnique, France

Copyright © 2003 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: 27 August 2003

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

PPDP03

Sponsor:

PPDP03: 5th International Conference on Principles and Practice of Declarative Programming 2003

August 27 - 29, 2003

Uppsala, Sweden

Acceptance Rates

PPDP '03 Paper Acceptance Rate 24 of 48 submissions, 50%;

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
179
Total Downloads

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

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Prost F(2011)Enforcing Dynamic Interference Policy2011 IEEE Third Int'l Conference on Privacy, Security, Risk and Trust and 2011 IEEE Third Int'l Conference on Social Computing10.1109/PASSAT/SocialCom.2011.17(1111-1118)Online publication date: Oct-2011
https://doi.org/10.1109/PASSAT/SocialCom.2011.17
Echahed RProst FBarahona PFelty A(2005)Security policy in a declarative styleProceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming10.1145/1069774.1069789(153-163)Online publication date: 11-Jul-2005
https://dl.acm.org/doi/10.1145/1069774.1069789
Echahed RProst FMeadows C(2005)Handling declared information leakageProceedings of the 2005 workshop on Issues in the theory of security10.1145/1045405.1045406(1-4)Online publication date: 10-Jan-2005
https://dl.acm.org/doi/10.1145/1045405.1045406

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