Hostname: page-component-586b7cd67f-2brh9 Total loading time: 0 Render date: 2024-11-22T06:59:18.476Z Has data issue: false hasContentIssue false
  • English
  • Français

Non-disclosure for distributed mobile code

Published online by Cambridge University Press:  27 October 2011

ANA ALMEIDA MATOS  and
JAN CEDERQUIST
ANA ALMEIDA MATOS
Affiliation:
SQIG-Instituto de Telecomunicações and Instituto Superior Técnico de Lisboa, Portugal Email: [email protected]; [email protected]
JAN CEDERQUIST
Affiliation:
SQIG-Instituto de Telecomunicações and Instituto Superior Técnico de Lisboa, Portugal Email: [email protected]; [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

With the emergence of the new possibilities offered by global computing, new security issues follow from the fact that these possibilities can be equally exploited by parties with malicious intentions. Many attacks arise at the application level, and can be tackled by means of programming language techniques. For instance, confidentiality can be violated during the execution of programs that reveal secret information. This kind of program behaviour can be avoided by information flow analyses that detect the encoding of illegal flows.

This paper studies information flows that occur in distributed programs with code mobility from a language-based security perspective. New forms of security leaks that are introduced by code mobility, which we call migration leaks, are presented and compared with well-known forms of illegal flow. We propose an information flow property that is adequate for networks consisting of a generalisation of the non-disclosure policy. We design a type and effect system for enforcing it on an expressive distributed calculus, and explain a soundness proof methodology in detail.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 21 , Special Issue 6: Programming Language Interference and Dependence , December 2011 , pp. 1111 - 1181
Copyright
Copyright © Cambridge University Press 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Almeida Matos, A. (2005) Non-disclosure for distributed mobile code. In: Ramanujam, R. and Sen, S. (eds.) FSTTCS'05: 25th International Conference on Foundations of Software Technology and Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science 3821 177–188.CrossRefGoogle Scholar
Almeida Matos, A. (2006) Typing secure information flow: declassification and mobility, Ph.D. thesis, École Nationale Supérieure des Mines de Paris.Google Scholar
Almeida Matos, A. (2009) Flow-policy awareness for distributed mobile code. In: Bravetti, M. and Zavattaro, G. (eds.) Proceedings of CONCUR 2009 – Concurrency Theory 20th International Conference. Springer-Verlag Lecture Notes in Computer Science 5710 53–68.Google Scholar
Almeida Matos, A. and Boudol, G. (2009) On declassification and the non-disclosure policy. Journal of Computer Security 17 (5)549–597.Google Scholar
Almeida Matos, A., Boudol, G. and Castellani, I. (2007) Typing noninterference for reactive programs. The Journal of Logic and Algebraic Programming 72 (2)124–156. (Special Issue on Programming Language Interference and Dependence.)CrossRefGoogle Scholar
Bell, D. E. and La Padula, L. J. (1976) Secure computer system: Unified exposition and multics interpretation, Technical Report MTR-2997, The MITRE Corporation.Google Scholar
Boudol, G. (2004) ULM: A core programming model for global computing. In: Schmidt, D. A. (ed.) ESOP'04: 13th European Symposium on Programming. Springer-Verlag Lecture Notes in Computer Science 2986 234–248.Google Scholar
Boudol, G. (2005 a) A generic membrane model. In: Priami, C. and Quaglia, P. (eds.) GC'04: IST/FET International Workshop on Global Computing. Springer-Verlag Lecture Notes in Computer Science 3267 208–222.Google Scholar
Boudol, G. (2005 b) On typing information flow. In: Hung, D. V. and Wirsing, M. (eds.) ICTAC'05: Second International Colloquium on Theoretical Aspects of Computing. Springer-Verlag Lecture Notes in Computer Science 3722 366–380.Google Scholar
Boudol, G. and Castellani, I. (2002) Noninterference for concurrent programs and thread systems. Theoretical Computer Science 281 (1–2)109–130.Google Scholar
Bugliesi, M., Castagna, G. and Crafa, S. (2001) Boxed ambients. In: Kobayashi, N. and Pierce, B. C. (eds.) TACS'01: 4th International Symposium on Theoretical Aspects of Computer Software. Springer-Verlag Lecture Notes in Computer Science 2215 38–63.Google Scholar
Bugliesi, M., Castagna, G. and Crafa, S. (2004) Access control for mobile agents: The calculus of boxed ambients. ACM Trans. Program. Lang. Syst. 26 (1)57–124.Google Scholar
Cardelli, L. and Gordon, A. D. (2000) Mobile ambients. Theoretical Computer Science 240 (1)177–213.CrossRefGoogle Scholar
Cohen, E. (1977) Information transmission in computational systems. In: SOSP'77: sixth ACM Symposium on Operating Systems Principles, ACM Press 133–139.Google Scholar
Crafa, S., Bugliesia, M. and Castagna, G. (2002) Information flow security for boxed ambients. In: Sassone, V. (ed.) F-WAN'02: Workshop on Foundations of Wide Area Network Computing. Electronic Notes in Theoretical Computer Science 66 76–97.CrossRefGoogle Scholar
Dal Zilio, S. (2001) Mobile processes: A commented bibliography. In: Cassez, F., Jard, C., Rozoy, B. and Ryan, M. D. (eds.) MOVEP'00: 4th Summer School on Modeling and Verification of Parallel Processes. Springer-Verlag Lecture Notes in Computer Science 2067.Google Scholar
Denning, D. E. (1976) A lattice model of secure information flow. Communications of the ACM 19 (5)236–243.Google Scholar
Focardi, R. and Gorrieri, R. (1995) A classification of security properties for process algebras. Journal of Computer Security 3 (1)5–33.CrossRefGoogle Scholar
Goguen, J. A. and Meseguer, J. (1982) Security policies and security models. In: Proceedings of the 1982 IEEE Symposium on Security and Privacy, IEEE Computer Society 11–20.CrossRefGoogle Scholar
Hennessy, M. and Riely, J. (2002) Information flow vs. resource access in the asynchronous pi-calculus. ACM Transactions on Programming Languages and Systems 24 (5)566–591.Google Scholar
Honda, K., Vasconcelos, V. T. and Yoshida, N. (2000) Secure information flow as typed process behaviour. In: Smolka, G. (ed.) ESOP'00: 9th European Symposium on Programming. Springer-Verlag Lecture Notes in Computer Science 1782 180–199.CrossRefGoogle Scholar
Honda, K. and Yoshida, N. (2002) A uniform type structure for secure information flow. In: POPL'02: 29th ACM Symposium on Principles of Programming Languages, ACM Press 81–92.CrossRefGoogle Scholar
Kırlı, D. (2000) Mobile functions and secure information flow. In: Degano, P. (ed.) WITS'00: Workshop on Issues in the Theory of Security.Google Scholar
Lucassen, J. M. and Gifford, D. K. (1988) Polymorphic effect systems. In: POPL'88: 15th ACM symposium on Principles of programming languages, ACM Press 47–57.Google Scholar
Mantel, H. and Sabelfeld, A. (2003) A unifying approach to the security of distributed and multi-threaded programs. Journal of Computer Security 11 (4)615–676.Google Scholar
Milner, R., Tofte, M., Harper, R. and MacQueen, D. (1997) The definition of Standard ML, revised edition, MIT Press.CrossRefGoogle Scholar
Myers, A. C. (1999) JFlow: Practical mostly-static information flow control. In: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, ACM Press 228–241.CrossRefGoogle Scholar
Myers, A. C. and Liskov, B. (1998) Complete, safe information flow with decentralized labels. In: 19th IEEE Computer Society Symposium on Security and Privacy, IEEE Computer Society 186–197.Google Scholar
Myers, A. C. and Liskov, B. (2000) Protecting privacy using the decentralized label model. ACM Transactions on Software Engineering and Methodology 9 (4)410–442.Google Scholar
Sabelfeld, A. (2001) The impact of synchronisation on secure information flow in concurrent programs. In: Bjørner, D., Broy, M. and Zamulin, A. V., (eds.) PSI'01: 4th International Andrei Ershov Memorial Conference on Perspectives of System Informatics. Springer-Verlag Lecture Notes in Computer Science 2244 225–239.Google Scholar
Sabelfeld, A. and Mantel, H. (2002) Securing communication in a concurrent language. In: Hermenegildo, M. V. and Puebla, G. (eds.) SAS'02: 9th International Symposium on Static Analysis. Springer-Verlag Lecture Notes in Computer Science 2477 376–394.Google Scholar
Sabelfeld, A. and Myers, A. (2004) A model for delimited information release. In: International Symposium on Software Security (ISSS'03). Springer-Verlag Lecture Notes in Computer Science 3233.Google Scholar
Sabelfeld, A. and Myers, A. C. (2003) Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21 (1)5–19.CrossRefGoogle Scholar
Sabelfeld, A. and Sands, D. (2000) Probabilistic noninterference for multi-threaded programs. In: CSFW'00: 13th IEEE Computer Security Foundations Workshop, IEEE Computer Society 200–215.Google Scholar
Sabelfeld, A. and Sands, D. (2005) Dimensions and principles of declassification. In: CSFW'05: 18th IEEE Computer Security Foundations Workshop, IEEE Computer Society 255–269.Google Scholar
Sekiguchi, T. and Yonezawa, A. (1997) A calculus with code mobility. In: FMOODS'97: IFIP TC6 WG6.1 international workshop on Formal methods for open object-based distributed systems, Chapman and Hall 21–36.Google Scholar
Smith, G. (2001) A new type system for secure information flow. In: CSFW'01: 14th IEEE Computer Security Foundations Workshop, IEEE Computer Society 115–125.Google Scholar
Volpano, D. M., Smith, G. and Irvine, C. E. (1996) A sound type system for secure flow analysis. Journal of Computer Security 4 (2–3)167–188.CrossRefGoogle Scholar
Wright, A. K. and Felleisen, M. (1994) A syntactic approach to type soundness. Information and Computation 115 (1)38–94.Google Scholar