Abstract
Web-based workflow management systems, like EasyChair, HealthVault, Ebay, or Amazon, often deal with confidential information such as the identity of reviewers, health data, or credit card numbers. Because the number of participants in the workflow is in principle unbounded, it is difficult to describe the information flow policy of such systems in specification languages that are limited to a fixed number of agents. We introduce a first-order version of HyperLTL, which allows us to express information flow requirements in workflows with arbitrarily many agents. We present a bounded model checking technique that reduces the violation of the information flow policy to the satisfiability of a first-order formula. We furthermore identify conditions under which the resulting satisfiability problem is guaranteed to be decidable.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Amtoft, T., Banerjee, A.: Information flow analysis in logical form. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 100–115. Springer, Heidelberg (2004)
Andersen, H.R.: A polyadic modal \(\mu \)-calculus. Technical report, Danmarks TekniskeUniversitet (1994)
Arapinis, M., Bursuc, S., Ryan, M.: Privacy supporting cloud computing: ConfiChair, a case study. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. LNCS, vol. 7215, pp. 89–108. Springer, Heidelberg (2012)
Ball, T., Bjørner, N., Gember, A., Itzhaky, S., Karbyshev, A., Sagiv, M., Schapira, M., Valadarsky, A.: Vericon: towards verifying controller programs in software-defined networks. In: ACM SIGPLAN Notices, vol. 49, pp. 282–293. ACM (2014)
Bhardwaj, C., Prasad, S.: Parametric information flow control in ehealth. Proc. HealthCom 2015, 102–107 (2015)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Heidelberg (1997)
Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014)
Dimitrova, R., Finkbeiner, B., Kovács, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 169–185. Springer, Heidelberg (2012)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Finkbeiner, B., Rabe, M.N.: The linear-hyper-branching spectrum of temporal logics. IT - Inf. Technol. 56(6), 273–279 (2014)
Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for Model Checking HyperLTL and HyperCTL\(^*\). In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 30–48. Springer, Heidelberg (2015)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11–20 (1982)
Halpern, J.Y., O’Neill, K.R.: Secrecy in multiagent systems. ACM Trans. Inf. Syst. Secur. 12(1), 5:1–5:47 (2008)
Hunt, S., Sands, D.: On flow-sensitive security types. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of POpPL 2006, pp. 79–90 (2006)
Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 167–183. Springer, Heidelberg (2014)
Manna, Z., Pnueli, A.: Verification of Concurrent Programs: The Temporal Framework. The Correctness Problem in Computer Science, pp. 215–273. Academic Press, London (1981)
Padon, O., Immerman, N., Karbyshev, A., Lahav, O., Sagiv, M., Shoham, S.: Decentralizing SDN policies. In: ACM SIGPLAN Notices, vol. 50, pp. 663–676. ACM (2015)
Sabelfeld, A., Sands, D.: Dimensions and principles of declassification. In: Proceedings CSFW 2005, pp. 255–269. IEEE Computer Society (2005)
Sutherland, D.: A model of information. In: Proceedings of the 9th National Computer Security Conference, pp. 175–183. DTIC Document (1986)
Zdancewic, S., Myers, A.C.: Observational determinism for concurrent program security. In: Proceedings CSFW 2003 (2003)
Acknowledgment
This work was partially supported by the German Research Foundation (DFG) under the project “SpAGAT” (grant no. FI 936/2-1) in the priority program “Reliably Secure Software Systems “RS3” and the doctorate program “Program and Model Analysis - PUMA” (no. 1480).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Finkbeiner, B., Seidl, H., Müller, C. (2016). Specifying and Verifying Secrecy in Workflows with Arbitrarily Many Agents. In: Artho, C., Legay, A., Peled, D. (eds) Automated Technology for Verification and Analysis. ATVA 2016. Lecture Notes in Computer Science(), vol 9938. Springer, Cham. https://doi.org/10.1007/978-3-319-46520-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-46520-3_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-46519-7
Online ISBN: 978-3-319-46520-3
eBook Packages: Computer ScienceComputer Science (R0)