×

zbMATH — the first resource for mathematics

Type-based information flow analysis for the \(\pi\)-calculus. (English) Zbl 1081.68061
Summary: We propose a new type system for information flow analysis for the \(\pi\)-calculus. As demonstrated by recent studies, information about whether each communication succeeds is important for precise information flow analysis for concurrent programs. By collecting such information using ideas of our previous type systems for deadlock/livelock-freedom, our type system can perform more precise analysis for certain communication/synchronization patterns (like synchronization using locks) than previous type systems. Our type system treats a wide range of communication/synchronization primitives in a uniform manner, which enabled development of a clear proof of type soundness and a sound and complete type inference algorithm.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
TyPiCal
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.: Secrecy by typing in security protocols. J. Assoc. Comput. Mach. (JACM) 46(5), 749–786 (1999) · Zbl 1064.94542 · doi:10.1145/324133.324266
[2] Abadi, M., Banerjee, A., Heintze, N., Rieck, J.G.: A core calculus of dependency. In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pp. 147–169 (1999)
[3] Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inform. Comput. 148(1), 1–70 (1999) · Zbl 0924.68073 · doi:10.1006/inco.1998.2740
[4] Cardelli, L., Ghelli, G., Gordon, A.D.: Secrecy and group creation. In: Proceedings of CONCUR 2000. Lecture Notes in Computer Science, vol. 1877, pp. 365–379. Springer-Verlag, Berlin Heidelberg New York (2000) · Zbl 0999.68148
[5] Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977) · Zbl 0361.68033 · doi:10.1145/359636.359712
[6] Fournet, C., Gonthier, G.: The reflexive CHAM and the join-calculus. In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pp. 372–385 (1996)
[7] Heintze, N., Riecke, J.: The slam calculus: programming with secrecy and integrity. In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pp. 365–377 (1998)
[8] Hennessy, M., Riely, J.: Information flow vs. resource access in the information asynchronous pi-calculus. In: Proceedings of ICALP 2000. Lecture Notes in Computer Science, vol. 1853, pp. 415–427. Springer-Verlag, Berlin Heidelberg New York (2000) · Zbl 0973.68519
[9] Hennessy, M.: The security picalculus and non-interference. J. Logic Algeb. Program. (in press)A1 · Zbl 1067.68096
[10] Honda, K., Vasconcelos, V., Yoshida, N.: Secure information flow as typed process behaviour. In: Proceedings of European Symposium on Programming (ESOP) 2000. Lecture Notes in Computer Science, vol. 1782, pp. 180–199. Springer-Verlag, Berlin Heidelberg New York (2000) · Zbl 0960.68126
[11] Honda, K., Yoshida, N.: A uniform type structure for secure information flow. In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pp. 81–92 (2002) · Zbl 1323.68375
[12] Igarashi, A., Kobayashi, N.: Type reconstruction for linear pi-calculus with I/O subtyping. Inform. Comput. 161, 1–44 (2000) · Zbl 1046.68620 · doi:10.1006/inco.2000.2872
[13] Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theor. Comput. Sci. 311(1–3), 121–163 (2004) · Zbl 1070.68105 · doi:10.1016/S0304-3975(03)00325-6
[14] Kobayashi, N.: Typical: a type-based static analyzer for the pi-calculus. Tool available at http://www.kb.ecei.tohoku.ac.jp/koba/typical/
[15] Kobayashi, N.: A type system for lock-free processes. Inform. Comput. 177, 122–159 (2002) · Zbl 1093.68065
[16] Kobayashi, N.: Useless-code elimination and program slicing for the pi-calculus. In: Proceedings of The First Asian Symposium on Programming Languages and Systems (APLAS’03). Lecture Notes in Computer Science, vol. 2895, pp. 55–72 (2003) · Zbl 1254.68080
[17] Kobayashi, N., Pierce, B.C., Turner, D.N.: Linearity and the pi-calculus. ACM Trans. Program. Language Syst. 21(5), 914–947 (1999) · doi:10.1145/330249.330251
[18] Kobayashi, N., Saito, S., Sumii, E.: An implicitly-typed deadlock-free process calculus. Technical Report TR00-01, Department of Inforamtion Sciences, University of Tokyo (2000). A summary has appeared in Proceedings of CONCUR 2000, Springer LNCS1877, pp.489-503, 2000 · Zbl 0999.68532
[19] Kobayashi, N., Shirane, K.: Type-based information flow analysis for a low-level language. Comput. Software 20(2), 2–21 (2003). In Japanese.
[20] Kobayashi, N., Yonezawa, A.: Towards foundations for concurrent object-oriented programming – types and language design. Theory Pract. Object Syst. 1(4), 243–268 (1995)
[21] Mayr, E.W.: An algorithm for the general petri net reachability problem. SIAM J. Comput. 13(3), 441–461 (1984) · Zbl 0563.68057 · doi:10.1137/0213029
[22] Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989) · Zbl 0683.68008
[23] Milner, R.: The polyadic \(\pi\)-calculus: a tutorial. In: Bauer, F.L., Brauer, W., Schwichtenberg, H. (eds.) Logic and Algebra of Specification. Springer-Verlag, Berlin Heidelberg New York (1993)
[24] Milner, R.: Communicating and Mobile Systems: the Pi-Calculus. Cambridge University Press, Cambridge (1999) · Zbl 0942.68002
[25] Pierce, B., Sangiorgi, D.: Typing and subtyping for mobile processes. Math. Struct. Comput. Sci. 6(5), 409–454 (1996) · Zbl 0861.68030
[26] Pierce, B.C., Turner, D.N.: Concurrent objects in a process calculus. In: Theory and Practice of Parallel Programming (TPPP), Sendai, Japan, November 1994. Lecture Notes in Computer Science, vol. 907, pp. 187–215. Springer-Verlag, Berlin Heidelberg New York (1995)
[27] Pottier, F.: A simple view of type-secure information flow in the \(\pi\)-calculus. In: Proceedings of the 15th IEEE Computer Security Foundations Workshop, pp. 320–330 (2002)
[28] Pottier, F., Simonet, V.: Information flow inference for ML. In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pp. 319–330 (2002) · Zbl 1323.68148
[29] Sabelfeld, A., Mantel, H.: Static confidentiality enforcement for distributed programs. In: Proceedings of the 9th International Static Analysis Symposium. LNCS, vol. 2477, pp. 376–394. Springer-Verlag, Madrid, Spain (2002) · Zbl 1015.68509
[30] Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001) · Zbl 0981.68116
[31] Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proceedings of ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages, pp. 355–364 (1998)
[32] Sumii, E., Kobayashi, N.: A generalized deadlock-free process calculus. In: Proceedings of Workshop on High-Level Concurrent Language (HLCL’98). ENTCS, vol. 16, No. 3, pp. 55–77 (1998) · Zbl 0917.68065
[33] Volpano, D., Smith, G., Irvine, C.: A sound type system for secure flow analysis. J. Comput. Security 4(3), 167–187 (1996)
[34] Yoshida, N.: Graph types for monadic mobile processes. In: FST/TCS’16. Lecture Notes in Computer Science, vol. 1180, pp. 371–387. Springer-Verlag, Berlin Heidelberg New York (1996)
[35] Zdancewic, S., Myers, A.C.: Secure information flow via linear continuations. Higher-Order Symbol. Comput. 15(2/3), 209–234 (2002) · Zbl 1030.68015 · doi:10.1023/A:1020843229247
[36] Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings of the 16th IEEE Computer Security Foundations Workshop pp. 29–43 (2003)
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.