OPEN ACCESS
From Earth observation to inter-companies relations, more and more organizations form decentralized systems in which information gets exchanged. In such settings it becomes crucial to explicit the rules governing information diffusion between parties, in what is called information exchange policies. This paper proposes a formal approach to exchange policies specification and analysis, together with a tool allowing the user to define policies and verify a number of formal requirements. In this paper, we first focus on a set of generic logical requirements, then we formalize two types antagonist requirements, the first being about enforcing necessary information diffusion, and the second about restricting the diffusion of specific kinds of information. Finally we explain how to reconcile these conflicting requirements in a single policy, thanks to an information filtering operator, the specification of which emerges naturally.
exchange policy analysis, requirements, formal methods, verification, SMT solvers
Akl S., Denning D. (1987). Checking classification constraints for consistency and completeness. In Ieee symposium on security and privacy, p. 196-201. IEEE Computer Society.
Barhamgi M., Benslimane D., Oulmakhzoune S., Cuppens-Boulahia N., Cuppens F., Mrissa M. et al. (2013). Secure and privacy-preserving execution model for data services. In C. Salinesi, M. C. Norrie, O. Pastor (Eds.), Caise, vol. 7908, p. 35-50. Springer.
Bieber P., Cuppens F. (1992). A logical view of secure dependencies. Journal of Computer Security, vol. 1, no 1, p. 99-130.
Bieber P., Cuppens F. (1993). Expression of confidentiality policies with deontic logic. In J.-J. C. Meyer, R. J. Wieringa (Eds.), Deontic logic in computer science: Normative system specification, p. 103-123. John Wiley & Sons, Inc.
Browne J., Zhang J. (1999). Extended and virtual enterprises similarities and differences. International Journal of Agile Management Systems, vol. 1, no 1, p. 30-36.
Castan˜eda H. N. (1975). Thinking and doing. D. Reidel, Dordrecht. Chocron P., Fontaine P., Ringeissen C. (2014). A gentle non-disjoint combination of satisfiability procedures. In S. Demri, D. Kapur, C.Weidenbach (Eds.), ijcar, vol. 8562, p. 122–136.
Springer.
Cholvy L., Cuppens F. (1997, may). Analyzing consistency of security policies. In Security and privacy, 1997. proceedings., 1997 ieee symposium on, p. 103 -112.
Cuppens-Boulahia N., Cuppens F. (2008). Specifying intrusion detection and reaction policies: An application of deontic logic. In Deon, p. 65-80.
Dal Bello B. R. (2011). Managing risk in space. Federation of American Scientists, Public Interest Report, Winter, vol. 64, no 4.
Delmas R., Polacsek T. (2013). Formal methods for exchange policy specification. In C. Salinesi, M. C. Norrie, O. Pastor (Eds.), Caise, vol. 7908, p. 288-303. Springer.
Delmas R., Polacsek T. (2014). Exigences de confidentialité et de diffusion concernant les politiques d’échanges d’information. Génie Logiciel, vol. 111, p. 49–53.
Delmas R., Polacsek T. (2015a). Critical information diffusion systems. In New trends in databases and information systems - ADBIS 2015 workshops wisard, vol. 539, p. 557–566. Springer.
Delmas R., Polacsek T. (2015b). Need-to-share & non-diffusion requirements verification in exchange policies. In Caise’15: Proceedings of advanced information systems engineering - 27th international conference. Springer.
Denning D. E., Akl S. G., Heckman M., Lunt T. F., Morgenstern M., Neumann P. G. et al. (1987). Views for multilevel database security. IEEE Trans. Software Eng., vol. 13, no 2, p. 129-140.
Department Of Defense. (1985). Department Of Defense Standard Department Of Defense Trusted Computer System Evaluation Criteria.
Dyer J. H., Singh H. (1998). The Relational View: Cooperative Strategy and Sources of Interorganizational Competitive Advantage. The Academy of Management Review, vol. 23, no 4, p. 660–679.
Edmonds B. (2002). How formal logic can fail to be useful for modelling or designing mas. In G. Lindemann, D. Moldt, M. Paolucci (Eds.), Regulated agent-based social systems, first international workshop, rasta 2002, bologna, italy, july 16, 2002, revised selected and invited papers, vol. 2934, p. 1-15. Springer.
Gallier J. H. (1987). Logic for computer science: Foundations of automatic theorem proving. In, p. 448-476. Wiley.
Heymann D. L., Rodier G. R. (2001). Hot spots in a wired world: {WHO} surveillance of emerging and re-emerging infectious diseases. The Lancet Infectious Diseases, vol. 1, no 5, p. 345 - 353.
ITSEC. (1991). Information technology security evaluation criteria (itsec): Preliminary harmonised criteria. Rapport technique no Document COM(90) 314, Version 1.2. Commission of the European Communities.
Jones A. J. I., Sergot M. J. (1992). Formal specification of security requirements using the theory of normative positions. In Proceedings of the second european symposium on research in computer security, p. 103–121. Springer-Verlag.
Kalam A. A. E., Baida R. E., Balbiani P., Benferhat S., Cuppens F., Deswarte Y. et al. (2003). Organization based access control. In Proceedings. policy 2003. ieee 4th international workshop on policies for distributed systems and networks, 2003.
Kalam A. A. E., Benferhat S., Miège A., Baida R. E., Cuppens F., Saurel C. et al. (2003). Organization based access contro. In Policy, p. 120-131. IEEE Computer Society.
Mandl K. D., Overhage J., Wagner M. M., Lober W. B., Sebastiani P., Mostashari F. et al. (2004). Implementing syndromic surveillance: a practical guide informed by the early experience. Journal of the American Medical Informatics Association, vol. 11, p. 141 - 150.
McCarthy J. (1997). Modality, si! modal logic, no! Studia Logica, vol. 59, no 1, p. 29-32.
Meynard J., Chaudet H., Texier G., Ardillon V., Ravachol F., Deparis X. et al. (2008). Value of syndromic surveillance within the armed forces for early warning during a dengue fever outbreak in french guiana in 2006. BMC Med. Inf. & Decision Making, vol. 8, p. 29.
Moura L. de, Bjørner N. (2008). Z3: An efficient smt solver. In Tools and algorithms for the construction and analysis of systems, 14th international conference, tacas 2008, vol. 4963, p. 337-340. Springer.
Sebastiani R., Vescovi M. (2009). Automated reasoning in modal and description logics via sat encoding: the case study of k(m)/alc-satisfiability. J. Artif. Intell. Res. (JAIR), vol. 35, p. 343-389.
Taverne B. (2015). Anticiper les flambées épidémiques à virus Ebola : pas sans les sciences sociales ! Global Health Promotion, vol. 22, no 2, p. 85–56.
Varraine-Leca A. (2015). Ebola : chronique d’une traque. Humanitaire. Enjeux, pratiques, débats, vol. 40, p. 80–87.