×

zbMATH — the first resource for mathematics

From flow logic to static type systems for coordination languages. (English) Zbl 1192.68126
Summary: Coordination languages are often used to describe open-ended systems. This makes it challenging to develop tools for guaranteeing the security of the coordinated systems and the correctness of their interaction. Successful approaches to this problem have been based on type systems with dynamic checks; therefore, the correctness properties cannot be statically enforced. By contrast, static analysis approaches based on Flow Logic usually guarantee properties statically. In this paper, we show how the insights from the Flow Logic approach can be used to construct a type system for statically ensuring secure access to tuple spaces and safe process migration for an extension of the language Klaim.

MSC:
68N15 Theory of programming languages
68Q60 Specification and verification (program logics, model checking, etc.)
68M14 Distributed systems
Software:
KLAIM; Linda; Succinct
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Aho, A.; Lam, M.; Sethi, R.; Ullman, J.: Compilers: principles, techniques, and tools, (2006) · Zbl 1155.68020
[2] Bodei, C.; Buchholtz, M.; Degano, P.; Nielson, F.; Nielson, H. R.: Static validation of security protocols, Journal of computer security 13, 347-390 (2005) · Zbl 1272.68225
[3] Bodei, C.; Degano, P.; Nielson, F.; Nielson, H. R.: Static analysis for the \({\pi}\)-calculus with applications to security, Information and computation 168, 68-92 (2001) · Zbl 1007.68118 · doi:10.1006/inco.2000.3020
[4] Braghin, C.; Cortesi, A.; Focardi, R.: Security boundaries in mobile ambients, Computer languages 28, No. 1, 101-127 (2002) · Zbl 1028.68004 · doi:10.1016/S0096-0551(02)00009-7
[5] Buchholz, M.; Nielson, H. R.; Nielson, F.: A calculus for control flow analysis of security protocols, International journal of information security 2, 145-167 (2004)
[6] Bugliesi, M.; Castagna, G.; Crafa, S.: Access control for mobile agents: the calculus of boxed ambients, ACM transactions on programming languages and systems 26, No. 1, 57-124 (2004)
[7] Cardelli, L.; Ghelli, G.; Gordon, A. D.: Ambient groups and mobility types, Lecture notes in computer science 1872, 333-347 (2000) · Zbl 0998.68536
[8] Cardelli, L.; Ghelli, G.; Gordon, A. D.: Types for the ambient calculus, Information and computation 177, No. 2, 160-194 (2002) · Zbl 1093.68060 · doi:10.1006/inco.2001.3121
[9] Castagna, G.; Vitek, J.; Nardelli, F. Zappa: The seal calculus, Information and computation 201, No. 1, 1-54 (2005) · Zbl 1101.68060 · doi:10.1016/j.ic.2004.11.005
[10] De Nicola, R.; Ferrari, G.; Pugliese, R.: KLAIM: A kernel language for agents interaction and mobility, IEEE transactions on software engineering 24, No. 5, 315-330 (1998)
[11] De Nicola, R.; Ferrari, G.; Pugliese, R.; Venneri, B.: Types for access control, Theoretical computer science 240, No. 1, 215-254 (2000) · Zbl 0954.68025 · doi:10.1016/S0304-3975(99)00232-7
[12] Degano, P.; Levi, F.; Bodei, C.: Safe ambients: control flow analysis and security, Lecture notes in computer science 1961, 199-214 (2000) · Zbl 0988.68543
[13] Gelernter, D.: Generative communication in linda, ACM transactions on programming languages and systems 7, No. 1, 80-112 (1985) · Zbl 0559.68030 · doi:10.1145/2363.2433 · www.acm.org
[14] D. Gorla, R. Pugliese, Dynamic management of capabilities in a network aware coordination language, Journal of Logic and Algebraic Programming (in press). An extended abstract appear with title ”Resource Access and Mobility Control with Dynamic Privileges Acquisition” in ICALP’03 · Zbl 1039.68542
[15] Gorla, D.; Pugliese, R.: Enforcing security policies via types, Lecture notes in computer science 2802, 86-100 (2004)
[16] Hansen, R. R.; Probst, C. W.; Nielson, F.: Sandboxing in myklaim, , 174-181 (2006)
[17] Heintze, N.: Control-flow analysis and type systems, Lecture notes in computer science 983, 189-206 (1995)
[18] Hennessy, M.; Riely, J.: Resource access control in systems of mobile agents, Information and computation 173, 82-120 (2002) · Zbl 1009.68081 · doi:10.1006/inco.2001.3089
[19] Laud, P.; Uustalu, T.; Vene, V.: Type systems equivalent to data-flow analyses for imperative languages, Theoretical computer science 364, No. 3, 292-310 (2006) · Zbl 1153.68351 · doi:10.1016/j.tcs.2006.08.013
[20] Levi, F.; Sangiorgi, D.: Mobile safe ambients, ACM transactions on programming languages and systems 25, No. 1, 1-69 (2003)
[21] Lhoussaine, C.; Sassone, V.: A dependently typed ambient calculus, Lecture notes in computer science 2986, 171-187 (2004) · Zbl 1126.68504 · doi:10.1007/b96702
[22] Nanz, S.; Hankin, C.: A framework for security analysis of mobile wireless networks, Theoretical computer science 367, No. 1–2, 203-227 (2006) · Zbl 1153.68322 · doi:10.1016/j.tcs.2006.08.036
[23] Nielson, F.; Hansen, R. R.; Nielson, H. R.: Abstract interpretation of mobile ambients, Science of computer programming 47, 145-175 (2003) · Zbl 1047.68080 · doi:10.1016/S0167-6423(02)00131-4
[24] Nielson, F.; Nielson, H. R.: Types from control flow analysis, Lecture notes in computer science 4444, 293-310 (2007) · Zbl 1149.68360 · doi:10.1007/978-3-540-71322-7_14
[25] Nielson, F.; Nielson, H. R.; Hansen, R. R.: Validating firewalls using flow logics, Theoretical computer science 283, No. 2, 381-418 (2002) · Zbl 1016.68003 · doi:10.1016/S0304-3975(01)00140-2
[26] Nielson, F.; Nielson, H. R.; Sun, H.; Buchholtz, M.; Hansen, R. R.; Pilegaard, H.; Seidl, H.: The succinct solver suite, Lecture notes in computer science 2988, 251-265 (2004) · Zbl 1126.68354
[27] Nielson, F.; Nielson, H. Riis; Hankin, C.: Principles of program analysis, (2005) · Zbl 1069.68534
[28] Nielson, F.; Seidl, H.; Nielson, H. R.: A succinct solver for ALFP, Nordic journal of computing 9, No. 4, 335-372 (2002) · Zbl 1088.68774
[29] Nielson, H. R.; Nielson, F.: Flow logic: A multi-paradigmatic approach to static analysis, Lecture notes in computer science 2566, 223-244 (2002) · Zbl 1026.68029 · link.springer.de
[30] Nielson, H. R.; Nielson, F.; Buchholtz, M.: Security for mobility, Lecture notes in computer science 2946, 207-266 (2004) · Zbl 1202.68173
[31] Palsberg, J.: Equality-based flow analysis versus recursive types, ACM transactions on programming languages and systems 20, No. 6, 1251-1264 (1998)
[32] Palsberg, J.; O’keefe, P.: A type system equivalent to flow analysis, ACM transactions on programming languages and systems 17, No. 4, 576-599 (1995)
[33] Palsberg, J.; Pavlopoulou, C.: From polyvariant flow information to intersection and union types, Journal of functional programming 11, No. 3, 263-317 (2001) · Zbl 0976.68024 · doi:10.1017/S095679680100394X
[34] Nielson, H. Riis; Nielson, F.: Flow logics: A multi-paradigmatic approach to static analysis, Lncs 2566, 223-244 (2002) · Zbl 1026.68029 · link.springer.de
[35] Schneider, F.; Morrisett, G.; Harper, R.: A language-based approach to security, Lncs 2000, 86-101 (2001)
[36] Udzir, N. I.; Wood, A.; Jacob, J.: Coordination with multicapabilities, Science of computer programming 64, No. 2, 205-222 (2007) · Zbl 1178.68083 · doi:10.1016/j.scico.2006.06.005
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.