zbMATH — the first resource for mathematics

A secrecy-preserving language for distributed and object-oriented systems. (English) Zbl 1395.68198
Summary: In modern systems it is often necessary to distinguish between confidential (low-level) and non-confidential (high-level) information. Confidential information should be protected and not communicated or shared with low-level users. The non-interference policy is an information flow policy stipulating that low-level viewers should not be able to observe a difference between any two executions with the same low-level inputs. Only high-level viewers may observe confidential output. This is a non-trivial challenge when considering modern distributed systems involving concurrency and communication.
The present paper addresses this challenge, by choosing language mechanisms that are both useful for programming of distributed systems and allow modular system analysis. We consider a general concurrency model for distributed systems, based on concurrent objects communicating by asynchronous methods. This model is suitable for modeling of modern service-oriented systems, and gives rise to efficient interaction avoiding active waiting and low-level synchronization primitives such as explicit signaling and lock operations. This concurrency model has a simple semantics and allows us to focus on information flow at a high level of abstraction, and allows realistic analysis by avoiding unnecessary restrictions on information flow between confidential and non-confidential data.
Due to the non-deterministic nature of concurrent and distributed systems, we define a notion of interaction non-interference policy tailored to this setting. We provide two kinds of static analysis: a secrecy-type system and a trace analysis system, to capture inter-object and network level communication, respectively. We prove that interaction non-interference is satisfied by the combination of these analysis techniques. Thus any deviation from the policy caused by implicit information leakage visible through observation of network communication patterns, can be detected. The contribution of the paper lies in the definition of the notion of interaction non-interference, and in the formalization of a secrecy type system and a static trace analysis that together ensure interaction non-interference. We also provide several versions of a main example (a news subscription service) to demonstrate network leakage.

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX Cite
Full Text: DOI
[1] Heintze, N.; Riecke, J. G., The slam calculus: programming with secrecy and integrity, (POPL’98: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (1998)), 365-377
[2] Hedin, D.; Sabelfeld, A., A perspective on information-flow control, (Software Safety and Security - Tools for Analysis and Verification, NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 33, (2012), IOS Press), 319-347
[3] Clarkson, M. R.; Schneider, F. B., Hyperproperties, J. Comput. Secur., 18, 6, 1157-1210, (2010)
[4] Goguen, J. A.; Meseguer, J., Unwinding and inference control, (IEEE Symposium on Security and Privacy, (1984)), 75
[5] Heintze, N.; Riecke, J. G., The slam calculus: programming with secrecy and integrity, (POPL’98, POPL’98, (1998), ACM), 365-377
[6] Askarov, A.; Hunt, S.; Sabelfeld, A.; Sands, D., Termination-insensitive noninterference leaks more than just a bit, (Proceedings of the 13th European Symposium on Research in Computer Security: Computer Security, ESORICS ’08, (2008), Springer-Verlag Berlin, Heidelberg), 333-348
[7] (2017), Open web application security project (owasp) top 10 2010 and 2013
[8] S. Christey, J.E. Kenderdine, et al., Common weakness enumeration (CWE version 2.9) (2015).
[9] Johnsen, E. B.; Owe, O., An asynchronous communication model for distributed concurrent objects, Softw. Syst. Model., 6, 1, 35-58, (2007)
[10] Johnsen, E. B.; Blanchette, J. C.; Kyas, M.; Owe, O., Intra-object versus inter-object: concurrency and reasoning in creol, Electron. Notes Theor. Comput. Sci., 243, 89-103, (2009)
[11] Dovland, J.; Johnsen, E. B.; Owe, O.; Steffen, M., Lazy behavioral subtyping, (Cuellar, J.; Maibaum, T., Proc. 15th International Symposium on Formal Methods (FM’08), Lecture Notes in Computer Science, vol. 5014, (2008), Springer), 52-67
[12] Zheng, L.; Myers, A. C., Dynamic security labels and static information flow control, Int. J. Inf. Secur., 6, 2, 67-84, (2007)
[13] Hoare, C. A.R., Communicating sequential processes, International Series in Computer Science, (1985), Prentice Hall · Zbl 0637.68007
[14] Broy, M.; Stølen, K., Specification and development of interactive systems, Monographs in Computer Science, (2001), Springer · Zbl 0981.68115
[15] Dahl, O.-J., Verifiable programming, International Series in Computer Science, (1992), Prentice Hall · Zbl 0790.68005
[16] Dahl, O.-J., Object-oriented specifications, (Research Directions in Object-Oriented Programming, (1987), MIT Press Cambridge, MA, USA), 561-576
[17] Johnsen, E. B.; Owe, O.; Yu, I. C., Creol: a type-safe object-oriented model for distributed concurrent systems, Theor. Comput. Sci., 365, 1-2, 23-66, (2006) · Zbl 1118.68031
[18] Erlingsson, U., The inlined reference monitor approach to security policy enforcement, (2004), Cornell University Ithaca, NY, USA, aAI3114521
[19] Kremenek, T.; Engler, D., Z-ranking: using statistical analysis to counter the impact of static analysis approximations, (International Static Analysis Symposium, (2003), Springer), 295-315 · Zbl 1067.68545
[20] Owe, O.; Ramezanifarkhani, T., Confidentiality of interactions in concurrent object-oriented systems, (Garcia-Alfaro, J.; Navarro-Arribas, G.; Hartenstein, H.; Herrera-Joancomartí, J., Data Privacy Management, Cryptocurrencies and Blockchain Technology, (2017), Springer International Publishing Cham), 19-34
[21] Din, C. C.; Owe, O., A sound and complete reasoning system for asynchronous communication with shared futures, J. Log. Algebraic Methods Program., 83, 5-6, 360-383, (2014) · Zbl 1371.68190
[22] Denning, D. E.; Denning, P. J., Certification of programs for secure information flow, Commun. ACM, 20, 7, 504-513, (1977) · Zbl 0361.68033
[23] Myers, A. C., Jflow: practical mostly-static information flow control, (Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (1999), ACM), 228-241
[24] Volpano, D.; Smith, G.; Irvine, C., A sound type system for secure flow analysis, J. Comput. Secur., 4, 2-3, 167-187, (1996)
[25] V. Simonet, The Flow Caml system. Software release, Jul. 2003, available at cristal.inria.fr/ simonet/flowcaml.
[26] Venkatakrishnan, V. N.; Xu, W.; DuVarney, D. C.; Sekar, R., Provably correct runtime enforcement of non-interference properties, (International Conference on Information and Communications Security, (2006), Springer), 332-351
[27] Leino, K. R.M.; Joshi, R., A semantic approach to secure information flow, Lecture Notes in Computer Science, vol. 1422, 254-271, (1998)
[28] Darvas, Á.; Hähnle, R.; Sands, D., A theorem proving approach to analysis of secure information flow, (International Conference on Security in Pervasive Computing, (2005), Springer), 193-209
[29] Austin, T. H.; Flanagan, C., Efficient purely-dynamic information flow analysis, ACM SIGPLAN Not., 44, 8, 20-31, (2009)
[30] Devriese, D.; Piessens, F., Noninterference through secure multi-execution, (2010 IEEE Symposium on Security and Privacy, SP, (2010), IEEE), 109-124
[31] Zheng, L.; Myers, A. C., Dynamic security labels and noninterference, (Formal Aspects in Security and Trust, (2005), Springer), 27-40
[32] Tse, S.; Zdancewic, S., Run-time principals in information-flow type systems, ACM Trans. Program. Lang. Syst., 30, 1, 6, (2007)
[33] Sabelfeld, A.; Russo, A., From dynamic to static and back: riding the roller coaster of information-flow control research, (Pnueli, A.; Virbitskaite, I.; Voronkov, A., Perspectives of Systems Informatics, vol. 5947, (2010), Springer Berlin, Heidelberg), 352-365
[34] Russo, A.; Sabelfeld, A., Dynamic vs. static flow-sensitive security analysis, (Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, (2010), IEEE Computer Society), 186-199
[35] Beringer, L., End-to-end multilevel hybrid information flow control, (Asian Symposium on Programming Languages and Systems, (2012), Springer), 50-65
[36] Buiras, P.; Vytiniotis, D.; Russo, A., HLIO: mixing static and dynamic typing for information-flow control in Haskell, (Fisher, K.; Reppy, J. H., Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015, (2015), ACM), 289-301 · Zbl 1360.68316
[37] Sayed, B., Protection against malicious javascript using hybrid flow-sensitive information flow monitoring, (2015), Department of Electrical and C omputer Engineering, University of Victoria Canada, Ph.D. Thesis
[38] Liu, J.; George, M.; Vikram, K.; Qi, X.; Waye, L.; Myers, A., Fabric: a platform for secure distributed computation and storage, (Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP ’09, ACM, New York, NY, USA, (2009)), 321-334
[39] Guernic, G. L., Automata-based confidentiality monitoring of concurrent programs, (Proceedings of IEEE Computer Security Foundations Symposium, (2007)), 218-232
[40] Miller, M. S., Robust composition: towards a unified approach to access control and concurrency control, (2006), John Hopkins University, Ph.D. Thesis
[41] Hammer, C.; Snelting, G., Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs, Int. J. Inf. Secur., 8, 6, 399-422, (2009)
[42] Hammer, C., Experiences with PDG-based IFC, (International Symposium on Engineering Secure Software and Systems, (2010), Springer), 44-60
[43] Fisher, K.; Launchbury, J.; Richards, R., The HACMS program: using formal methods to eliminate exploitable bugs, Phil. Trans. R. Soc. A, 375, 2104, (2017)
[44] Wardell, D. C.; Mills, R. F.; Peterson, G. L.; Oxley, M. E., A method for revealing and addressing security vulnerabilities in cyber-physical systems by modeling malicious agent interactions with formal verification, Proc. Comput. Sci., 95, 24-31, (2016)
[45] Owe, O., Verifiable programming of object-oriented and distributed systems, (Petre, L.; Sekerinski, E., From Action Systems to Distributed Systems - The Refinement Approach, (2016), Chapman and Hall/CRC), 61-79
[46] Owe, O., Reasoning about inheritance and unrestricted reuse in object-oriented concurrent systems, (Ábrahám, E.; Huisman, M., Integrated Formal Methods - Proceedings, 12th International Conference, IFM 2016, Reykjavik, Iceland, June 1-5, 2016, Lecture Notes in Computer Science, vol. 9681, (2016), Springer), 210-225
[47] Ramezanifarkhani, T.; Razzazi, M., Principles of data flow integrity: specification and enforcement, J. Inf. Sci. Eng., 31, 2, 529-546, (2015)
[48] Mantel, H.; Sudbrock, H., Types vs. PDGs in information flow analysis, (International Symposium on Logic-Based Program Synthesis and Transformation, (2012), Springer), 106-121 · Zbl 1394.68078
[49] Din, C. C.; Dovland, J.; Johnsen, E. B.; Owe, O., Observable behavior of distributed systems: component reasoning for concurrent objects, J. Log. Algebraic Program., 81, 3, 227-256, (2012) · Zbl 1247.68184
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.