×

Combining behavioural types with security analysis. (English) Zbl 1330.68045

Summary: Today’s software systems are highly distributed and interconnected, and they increasingly rely on communication to achieve their goals; due to their societal importance, security and trustworthiness are crucial aspects for the correctness of these systems. Behavioural types, which extend data types by describing also the structured behaviour of programs, are a widely studied approach to the enforcement of correctness properties in communicating systems. This paper offers a unified overview of proposals based on behavioural types which are aimed at the analysis of security properties.

MSC:

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Abadi, M.; Cardelli, L.; Pierce, B.; Plotkin, G., Dynamic typing in a statically typed language, ACM Trans. Program. Lang. Syst., 13, 2, 237-268 (1991)
[2] Ancona, D.; Bono, V.; Bravetti, M.; Castagna, G.; Campos, J.; Deniélou, P.-M.; Gay, S.; Gesbert, N.; Giachino, E.; Hu, R.; Johnsen, E. B.; Martins, F.; Mascardi, V.; Montesi, F.; Ng, N.; Neykova, R.; Padovani, L.; Vasconcelos, V.; Yoshida, N., Behavioral types in programming languages (2014)
[3] Baltazar, P.; Caires, L.; Vasconcelos, V. T.; Vieira, H. T., A type system for flexible role assignment in multiparty communicating systems, (TGC 2012. TGC 2012, LNCS, vol. 8191 (2013), Springer), 82-96
[4] Baltazar, P.; Mostrous, D.; Vasconcelos, V. T., Linearly refined session types, (LINEARITY 2012. LINEARITY 2012, EPTCS, vol. 101 (2012)), 38-49 · Zbl 1459.68135
[5] Barbanera, F.; de’Liguoro, U., Two notions of sub-behaviour for session-based client/server systems, (Proc. PPDP (2010)), 155-164
[6] Barnes, J., High Integrity Software: The SPARK Approach to Safety and Security (2003), Addison-Wesley
[7] Bartoletti, M.; Cimoli, T.; Pinna, G. M.; Zunino, R., Contracts as games on event structures, J. Log. Alg. Meth. Prog. (2015), in press
[8] Bartoletti, M.; Cimoli, T.; Zunino, R., A theory of agreements and protection, (POST 2013. POST 2013, LNCS, vol. 7796 (2013), Springer), 186-205 · Zbl 1390.68066
[9] Bartoletti, M.; Murgia, M.; Scalas, A.; Zunino, R., Modelling and verifying contract-oriented systems in Maude, (WRLA 2014. WRLA 2014, LNCS, vol. 8663 (2014), Springer), 130-146 · Zbl 1366.68197
[10] Bartoletti, M.; Scalas, A.; Tuosto, E.; Zunino, R., Honesty by typing, (FMOODS/FORTE 2013. FMOODS/FORTE 2013, LNCS, vol. 7892 (2013), Springer), 305-320
[11] Bartoletti, M.; Tuosto, E.; Zunino, R., Contract-oriented computing in \(CO_2\), Sci. Ann. Comput. Sci., 22, 1, 5-60 (2012) · Zbl 1424.68097
[12] Bartoletti, M.; Tuosto, E.; Zunino, R., On the realizability of contracts in dishonest systems, (COORDINATION 2012. COORDINATION 2012, LNCS, vol. 7274 (2012), Springer), 245-260 · Zbl 1366.68198
[13] Bettini, L.; Coppo, M.; D’Antoni, L.; Luca, M. D.; Dezani-Ciancaglini, M.; Yoshida, N., Global progress in dynamically interleaved multiparty sessions, (CONCUR 2008. CONCUR 2008, LNCS, vol. 5201 (2008), Springer), 418-433 · Zbl 1160.68456
[14] Bhargavan, K.; Corin, R.; Deniélou, P.-M.; Fournet, C.; Leifer, J. J., Cryptographic protocol synthesis and verification for multiparty sessions, (CSF 2009 (2009), IEEE), 124-140
[15] Bocchi, L.; Chen, T.; Demangeon, R.; Honda, K.; Yoshida, N., Monitoring networks through multiparty session types, (FMOODS/FORTE 2013. FMOODS/FORTE 2013, LNCS, vol. 7892 (2013), Springer), 50-65
[16] Bocchi, L.; Honda, K.; Tuosto, E.; Yoshida, N., A theory of design-by-contract for distributed multiparty interactions, (CONCUR 2010. CONCUR 2010, LNCS, vol. 6269 (2010), Springer), 162-176 · Zbl 1287.68121
[17] Bonelli, E.; Compagnoni, A. B.; Gunter, E. L., Correspondence assertions for process synchronization in concurrent communications, J. Funct. Program., 15, 2, 219-247 (2005) · Zbl 1077.68605
[18] Boreale, M.; Bruni, R.; Caires, L.; De Nicola, R.; Lanese, I.; Loreti, M.; Martins, F.; Montanari, U.; Ravara, A.; Sangiorgi, D.; Vasconcelos, V. T.; Zavattaro, G., SCC: a service centered calculus, (WS-FM 2006. WS-FM 2006, LNCS, vol. 4184 (2006), Springer), 38-57
[19] Bossi, A.; Focardi, R.; Piazza, C.; Rossi, S., Verifying persistent security properties, Comput. Lang. Syst. Struct., 30, 3-4, 231-258 (2004) · Zbl 1072.68065
[20] Bruni, R.; Mezzina, L. G., Types and deadlock freedom in a calculus of services, sessions and pipelines, (AMAST 2008. AMAST 2008, LNCS, vol. 5140 (2008), Springer), 100-115 · Zbl 1170.68428
[21] Caires, L.; Pfenning, F., Session types as intuitionistic linear propositions, (CONCUR 2010. CONCUR 2010, LNCS, vol. 6269 (2010), Springer), 222-236 · Zbl 1287.68125
[22] Capecchi, S.; Castellani, I.; Dezani-Ciancaglini, M., Typing access control and secure information flow in sessions, Inf. Comput., 238, 68-105 (2014) · Zbl 1360.68207
[23] Capecchi, S.; Castellani, I.; Dezani-Ciancaglini, M., Information flow safety in multiparty sessions, Math. Struct. Comput. Sci., 1-43 (2015)
[24] Capecchi, S.; Castellani, I.; Dezani-Ciancaglini, M.; Rezk, T., Session types for access and information flow control, (CONCUR 2010. CONCUR 2010, LNCS, vol. 6269 (2010), Springer), 237-252 · Zbl 1287.68126
[25] Castellani, I.; Dezani-Ciancaglini, M.; Pérez, J. A., Self-adaptation and secure information flow in multiparty structured communications: a unified perspective, (BEAT 2014. BEAT 2014, EPTCS, vol. 162 (2014)), 9-18
[26] Chen, T.-C.; Bocchi, L.; Deniélou, P.-M.; Honda, K.; Yoshida, N., Asynchronous distributed monitoring for multiparty session enforcement, (TGC 2011. TGC 2011, LNCS, vol. 7173 (2012), Springer), 25-45
[27] Chong, S.; Myers, A. C.; Vikram, K.; Zheng, L., Jif Reference Manual (2009), Cornell University
[28] Corin, R.; Deniélou, P.-M., A protocol compiler for secure sessions in ML, (TGC 2007. TGC 2007, LNCS, vol. 4912 (2007), Springer), 276-293
[29] Corin, R.; Deniélou, P.-M.; Fournet, C.; Bhargavan, K.; Leifer, J. J., Secure implementations for typed session abstractions, (CSF 2007 (2007), IEEE), 170-186
[30] Corin, R.; Deniélou, P.-M.; Fournet, C.; Bhargavan, K.; Leifer, J. J., A secure compiler for session abstractions, J. Comput. Secur., 16, 5, 573-636 (2008)
[31] Crafa, S.; Rossi, S., A theory of noninterference for the pi-calculus, (TGC 2005. TGC 2005, LNCS, vol. 3705 (2005), Springer), 2-18 · Zbl 1151.68523
[32] Deniélou, P.; Yoshida, N., Multiparty session types meet communicating automata, (ESOP 2012. ESOP 2012, LNCS, vol. 7211 (2012), Springer), 194-213 · Zbl 1352.68182
[33] Denning, D. E.; Denning, P. J., Certification of programs for secure information flow, Commun. ACM, 20, 7, 504-513 (1977) · Zbl 0361.68033
[34] Dezani-Ciancaglini, M.; Drossopoulou, S.; Mostrous, D.; Yoshida, N., Objects and session types, Inf. Comput., 207, 5, 595-641 (2009) · Zbl 1183.68358
[35] Dezani-Ciancaglini, M.; Ghilezan, S.; Jaksic, S.; Pantovic, J., Types for role-based access control of dynamic web data, (WFLP 2010. WFLP 2010, LNCS, vol. 6559 (2010), Springer), 1-29 · Zbl 1327.68169
[36] Dezani-Ciancaglini, M.; Ghilezan, S.; Pantovic, J., Security types for dynamic web data, (TGC 2006. TGC 2006, LNCS, vol. 4661 (2006), Springer), 263-280 · Zbl 1211.68267
[37] Dezani-Ciancaglini, M.; Ghilezan, S.; Pantovic, J.; Varacca, D., Security types for dynamic web data, Theor. Comput. Sci., 402, 2-3, 156-171 (2008) · Zbl 1146.68014
[38] Disney, T.; Flanagan, C., Gradual information flow typing, (STOP 2011 (2011))
[39] Fähndrich, M.; Aiken, M.; Hawblitzel, C.; Hodson, O.; Hunt, G. C.; Larus, J. R.; Levi, S., Language support for fast and reliable message-based communication in singularity OS, (EuroSys 2006 (2006), ACM), 177-190
[40] Fennell, L.; Thiemann, P., The blame theorem for a linear lambda calculus with type dynamic, (TFP 2012. TFP 2012, LNCS, vol. 7829 (2012), Springer), 37-52
[41] Fennell, L.; Thiemann, P., Gradual security typing with references, (CSF 2013 (2013), IEEE), 224-239
[42] Fennell, L.; Thiemann, P., Gradual typing for annotated type systems, (ESOP 2014. ESOP 2014, LNCS, vol. 8410 (2014), Springer), 47-66 · Zbl 1405.68093
[43] (Focardi, R.; Gorrieri, R., Foundations of Security Analysis and Design, Tutorial Lectures. Foundations of Security Analysis and Design, Tutorial Lectures, LNCS, vol. 2171 (2001), Springer) · Zbl 0974.00025
[44] Gardner, P.; Maffeis, S., Modelling dynamic web data, Theor. Comput. Sci., 342, 1, 104-131 (2005) · Zbl 1077.68004
[45] Garg, D.; Pfenning, F., A proof-carrying file system, (S&P 2010 (2010), IEEE), 349-364
[46] Gay, S. J.; Hole, M., Subtyping for session types in the pi calculus, Acta Inform., 42, 2-3, 191-225 (2005) · Zbl 1079.68065
[47] Ghilezan, S.; Jaksic, S.; Pantovic, J.; Dezani-Ciancaglini, M., Types and roles for web security, Trans. Adv. Res., 8, 2, 16-21 (2012)
[48] Ghilezan, S.; Jaksic, S.; Pantovic, J.; Pérez, J. A.; Vieira, H. T., Dynamic role authorization in multiparty conversations, (BEAT 2014. BEAT 2014, EPTCS, vol. 162 (2014)), 1-8
[49] Girard, J.-Y., Linear logic, Theor. Comput. Sci., 50, 1-102 (1987) · Zbl 0625.03037
[50] Goguen, J. A.; Meseguer, J., Security policies and security models, (IEEE Symp. Sec. and Priv. (1982)), 11-20
[51] Gordon, A. D.; Jeffrey, A., Typing correspondence assertions for communication protocols, Theor. Comput. Sci., 300, 1-3, 379-409 (2003) · Zbl 1023.68006
[52] Harper, R.; Honsell, F.; Plotkin, G., A framework for defining logics, J. ACM, 40, 143-184 (1993) · Zbl 0778.03004
[53] Hedin, D.; Birgisson, A.; Bello, L.; Sabelfeld, A., JSFlow: tracking information flow in JavaScript and its APIs, (SAC 2014 (2014), ACM), 1663-1671
[54] Henglein, F., Dynamic typing: syntax and proof theory, Sci. Comput. Program., 22, 197-230 (1994) · Zbl 0809.68083
[55] Hennessy, M., The security pi-calculus and non-interference, J. Log. Algebr. Program., 63, 1, 3-34 (2005) · Zbl 1067.68096
[56] Hennessy, M.; Riely, J., Information flow vs. resource access in the asynchronous pi-calculus, ACM Trans. Program. Lang. Syst., 24, 5, 566-591 (2002)
[57] Honda, K., Types for dyadic interaction, (CONCUR 1993. CONCUR 1993, LNCS, vol. 715 (1993), Springer), 509-523
[58] Honda, K.; Vasconcelos, V. T.; Kubo, M., Language primitives and type discipline for structured communication-based programming, (ESOP 1998. ESOP 1998, LNCS, vol. 1381 (1998), Springer), 122-138
[59] Honda, K.; Vasconcelos, V. T.; Yoshida, N., Secure information flow as typed process behaviour, (ESOP 2000. ESOP 2000, LNCS, vol. 1782 (2000), Springer), 180-199 · Zbl 0960.68126
[60] Honda, K.; Yoshida, N., A uniform type structure for secure information flow, ACM Trans. Program. Lang. Syst., 29, 6 (2007)
[61] Honda, K.; Yoshida, N.; Carbone, M., Multiparty asynchronous session types, (POPL 2008 (2008), ACM), 273-284 · Zbl 1295.68150
[62] Hüttel, H.; Lanese, I.; Vasconcelos, V. T.; Caires, L.; Carbone, M.; Deniélou, P.; Mostrous, D.; Padovani, L.; Ravara, A.; Tuosto, E.; Vieira, H. T.; Zavattaro, G., Foundations of behavioural types (2014)
[63] Jaksic, S., Input/output types for dynamic web data, (ICTCS 2012 (2012))
[64] Kitchin, D.; Quark, A.; Cook, W. R.; Misra, J., The Orc programming language, (FMOODS/FORTE 2009. FMOODS/FORTE 2009, LNCS, vol. 5522 (2009), Springer), 1-25 · Zbl 1217.68049
[65] Kobayashi, N., A type system for lock-free processes, Inf. Comput., 177, 122-159 (2002) · Zbl 1093.68065
[66] Kobayashi, N., Type-based information flow analysis for the pi-calculus, Acta Inform., 42, 4-5, 291-347 (2005) · Zbl 1081.68061
[67] Kolundzija, M., Security types for sessions and pipelines, (WS-FM 2008. WS-FM 2008, LNCS, vol. 5387 (2008), Springer), 175-190
[68] Lapadula, A.; Pugliese, R.; Tiezzi, F., Regulating data exchange in service oriented applications, (FSEN 2007. FSEN 2007, LNCS, vol. 4767 (2007), Springer), 223-239 · Zbl 1141.68509
[69] Mukhija, A.; Dingwall-Smith, A.; Rosenblum, D., QoS-aware service composition in Dino, (ECOWS (2007)), 3-12
[70] Necula, G. C., Proof-carrying code, (POPL 1997 (1997), ACM), 106-119
[71] Ocean Observatories Initiative (2010)
[72] Padovani, L., Deadlock and lock freedom in the linear \(π\)-calculus, (CSL-LICS 2014 (2014), ACM), 72 · Zbl 1392.68311
[73] Pérez, J. A.; Caires, L.; Pfenning, F.; Toninho, B., Linear logical relations and observational equivalences for session-based concurrency, Inf. Comput., 239, 254-302 (2014) · Zbl 1309.68141
[74] Pfenning, F., Intensionality, extensionality, and proof irrelevance in modal type theory, (LICS 2001 (2001), IEEE), 221-230
[75] Pfenning, F.; Caires, L.; Toninho, B., Proof-carrying code in a session-typed process calculus, (CPP 2011. CPP 2011, LNCS, vol. 7086 (2011), Springer), 21-36 · Zbl 1350.68204
[76] Planul, J.; Corin, R.; Fournet, C., Secure enforcement for global process specifications, (CONCUR 2009. CONCUR 2009, LNCS, vol. 5710 (2009), Springer), 511-526 · Zbl 1254.68177
[77] Pottier, F., A simple view of type-secure information flow in the p-calculus, (CSFW 2002 (2002), IEEE), 320-330
[78] Pottier, F.; Skalka, C.; Smith, S. F., A systematic approach to static access control, ACM Trans. Program. Lang. Syst., 27, 2, 344-382 (2005)
[79] Pugliese, R.; Tiezzi, F., A calculus for orchestration of web services, J. Appl. Log., 10, 1, 2-31 (2012)
[80] Ryan, P. Y.A.; Schneider, S. A., Process algebra and non-interference, (CSFW 1999 (1999), IEEE), 214-227
[81] Santos, J. F.; Rezk, T., An information flow monitor-inlining compiler for securing a core of JavaScript, (SEC 2014. SEC 2014, IFIP Adv. ICT, vol. 428 (2014), Springer), 278-292
[82] Siek, J.; Taha, W., Gradual typing for objects, (ECOOP 2007. ECOOP 2007, LNCS, vol. 4609 (2007), Springer), 2-27
[83] Siek, J. G.; Taha, W., Gradual typing for functional languages, (Scheme and Functional Programming Workshop (2006)), 81-92
[84] Simonet, V., The Flow Caml System: Documentation and User’s Manual (2003), INRIA
[85] Sunshine, J.; Naden, K.; Stork, S.; Aldrich, J.; Tanter, É., First-class state change in Plaid, (OOPSLA 2011 (2011), ACM), 713-732
[86] Swamy, N.; Chen, J.; Fournet, C.; Strub, P.; Bhargavan, K.; Yang, J., Secure distributed programming with value-dependent types, J. Funct. Program., 23, 4, 402-451 (2013) · Zbl 1290.68033
[87] Thiemann, P., Gradual typing for session types, (TGC 2014. TGC 2014, LNCS, vol. 8902 (2014), Springer), 144-158 · Zbl 1444.68123
[88] Tobin-Hochstadt, S.; Felleisen, M., Interlanguage migration: from scripts to programs, (OOPSLA 2006 (2006), ACM), 964-974
[89] Toninho, B.; Caires, L.; Pfenning, F., Dependent session types via intuitionistic linear type theory, (PPDP 2011 (2011), ACM), 161-172
[90] Tov, J. A.; Pucella, R., Stateful contracts for affine types, (ESOP 2010. ESOP 2010, LNCS, vol. 6012 (2010), Springer), 550-569 · Zbl 1260.68054
[91] Vallecillo, A.; Vasconcelos, V. T.; Ravara, A., Typing the behavior of software components using session types, Fundam. Inform., 73, 4, 583-598 (2006) · Zbl 1114.68384
[92] Vasconcelos, V. T.; Gay, S. J.; Ravara, A., Type checking a multithreaded functional language with session types, Theor. Comput. Sci., 368, 1-2, 64-87 (2006) · Zbl 1171.68410
[93] Volpano, D.; Irvine, C.; Smith, G., A Sound Type System for Secure Flow Analysis, J. Comput. Secur., 4, 2-3, 167-187 (1996)
[94] Winskel, G., Event structures, (APN 1986. APN 1986, LNCS, vol. 255 (1986), Springer), 325-392
[95] Wolff, R.; Garcia, R.; Tanter, É.; Aldrich, J., Gradual typestate, (ECOOP 2011. ECOOP 2011, LNCS, vol. 6813 (2011), Springer), 459-483
[96] Yoshida, N.; Hu, R.; Neykova, R.; Ng, N., The Scribble protocol language, (TGC 2013. TGC 2013, LNCS, vol. 8358 (2013), Springer), 22-41
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.