Abstract
We study the repair problem for hyperproperties specified in the temporal logic HyperLTL. Hyperproperties are system properties that relate multiple computation traces. This class of properties includes information flow policies like noninterference and observational determinism. The repair problem is to find, for a given Kripke structure, a substructure that satisfies a given specification. We show that the repair problem is decidable for HyperLTL specifications and finite-state Kripke structures. We provide a detailed complexity analysis for different fragments of HyperLTL and different system types: tree-shaped, acyclic, and general Kripke structures.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
References
Ábrahám, E., Bonakdarpour, B.: HyperPCTL: a temporal logic for probabilistic hyperproperties. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 20–35. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-99154-2_2
Agrawal, S., Bonakdarpour, B.: Runtime verification of \(k\)-safety hyperproperties in HyperLTL. In: Proceedings of the IEEE 29th Computer Security Foundations (CSF), pp. 239–252 (2016)
Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design (FMCAD), pp.1–8 (2013)
Alur, R., Tripakis, S.: Automatic synthesis of distributed protocols. SIGACT News 48(1), 55–90 (2017)
Bonakdarpour, B., Ebnenasir, A., Kulkarni, S.S.: Complexity results in revising UNITY programs. ACM Trans. Auton. Adapt. Syst. (TAAS) 4(1), 1–28 (2009)
Bonakdarpour, B., Finkbeiner, B.: The complexity of monitoring hyperproperties. In: Proceedings of the IEEE 31th Computer Security Foundations (CSF), pp. 162–174 (2018)
Bonakdarpour, B., Kulkarni, S.S.: Masking faults while providing bounded-time phased recovery. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 374–389. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_26
Bonakdarpour, B., Sanchez, C., Schneider, G.: Monitoring hyperproperties by combining static analysis and runtime verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11245, pp. 8–27. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03421-4_2
Brett, N., Siddique, U., Bonakdarpour, B.: Rewriting-based runtime verification for alternation-free HyperLTL. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 77–93. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54580-5_5
Chaum, D.: Security without identification: transaction systems to make big brother obsolete. Commun. ACM 28(10), 1030–1044 (1985)
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. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15
Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)
Coenen, N., Finkbeiner, B., Hahn, C., Hofmann, J.: The hierarchy of hyperlogics. In: 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (2019)
Coenen, N., Finkbeiner, B., Sánchez, C., Tentrup, L.: Verifying hyperliveness. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 121–139. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_7
Ebnenasir, A., Kulkarni, S.S., Bonakdarpour, B.: Revising UNITY programs: possibilities and limitations. In: Anderson, J.H., Prencipe, G., Wattenhofer, R. (eds.) OPODIS 2005. LNCS, vol. 3974, pp. 275–290. Springer, Heidelberg (2006). https://doi.org/10.1007/11795490_22
Etessami, K.: Counting quantifiers, successor relations, and logarithmic space. J. Comput. Syst. Sci. 54(3), 400–411 (1997)
Finkbeiner, B., Hahn, C.: Deciding hyperproperties. In: Proceedings of the 27th International Conference on Concurrency Theory (CONCUR), pp. 13:1–13:14 (2016)
Finkbeiner, B., Hahn, C., Hans, T.: MGHyper: checking satisfiability of HyperLTL formulas beyond the \(\exists ^*\forall ^*\) fragment. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 521–527. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_31
Finkbeiner, B., Hahn, C., Lukert, P., Stenger, M., Tentrup, L.: Synthesizing reactive systems from hyperproperties. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 289–306. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_16
Finkbeiner, B., Hahn, C., Stenger, M.: EAHyper: satisfiability, implication, and equivalence checking of hyperproperties. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 564–570. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_29
Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: \(\text{ RVHyper }\): a runtime verification tool for temporal hyperproperties. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 194–200. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_11
Finkbeiner, B., Hahn, C., Stenger, M., Tentrup, L.: Monitoring hyperproperties. Formal Methods Syst. Des.(2019)
Finkbeiner, B., Hahn, C., Torfah, H.: Model Checking quantitative hyperproperties. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 144–163. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_8
Finkbeiner, B., Müller, C., Seidl, H., Zalinescu, E.: Verifying security policies in multi-agent workflows with loops. In: Proceedings of the 15th ACM Conference on Computer and Communications Security (CCS), pp. 633–645 (2017)
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, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_3
Finkbeiner, B., Schewe, S.: Uniform distributed synthesis. In: Proceedings of LICS, pp. 321–330. IEEE Computer Society (2005)
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, New York (1979)
Goguen, J.A., Meseguer, J.: Security policies and security models. In: Proceedings of the IEEE Symposium on Security and Privacy (S & P), pp. 11–20 (1982)
Hahn, C., Stenger, M., Tentrup, L.: Constraint-based monitoring of hyperproperties. In: Vojnar, T., Zhang, L. (eds.) TACAS 2019. LNCS, vol. 11428, pp. 115–131. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-17465-1_7
Jacob, J.: On the derivation of secure components. In: Proceedings of the IEEE Symposium on Security and Privacy (S & P), pp. 242–247 (1989)
Jiang, S., Kumar, R.: Supervisory control of discrete event systems with CTL* temporal logic specifications. SIAM J. Control Optim. 44(6), 2079–2103 (2006)
Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226–238. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_23
Kuhtz, L., Finkbeiner, B.: Weak Kripke structures and LTL. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 419–433. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-23217-6_28
Lengauer, T., Wagner, K.W.: The correlation between the complexities of the nonhierarchical and hierarchical versions of graph problems. J. Comput. Syst. Sci. 44(1), 63–93 (1992)
Lin, F.: Analysis and synthesis of discrete event systems using temporal logic. In: Proceedings of the 1991 IEEE International Symposium on Intelligent Control, pp. 140–145, (August 1991)
McCullough, D.: Noninterference and the composability of security properties. In: Proceedings IEEE Symposium on Security and Privacy, pp. 177–186, (April 1988)
Rabe, M.N.: A Temporal Logic Approach to Information-flow Control. PhD thesis, Saarland University (2016)
Solar-Lezama, A.: Program sketching. J. Softw. Tool Technol. Transfer STTT 15(5–6), 475–495 (2013). https://doi.org/10.1007/s10009-012-0249-7
Stucki, S., Sánchez, C., Schneider, G., Bonakdarpour, B.: Graybox monitoring of hyperproperties. In: Proceedings of the 23rd International Symposium on Formal Methods (FM) (2019). To appear
Thistle, J.G., Wonham, W.M.: Control problems in a temporal logic framework. Int. J. Control 44(4), 943–976 (1986)
Acknowledgments
We would like to thank Sandeep Kulkrani, Reza Hajisheykhi (Michigan State University), and Shreya Agrawal (Google). The repair problem was originally inspired through our interaction with them. This work is sponsored in part by NSF SaTC Award 1813388. It was also supported by the German Research Foundation (DFG) as part of the Collaborative Research Center “Methods and Tools for Understanding and Controlling Privacy” (CRC 1223) and the Collaborative Research Center “Foundations of Perspicuous Software Systems” (TRR 248, 389792660), and by the European Research Council (ERC) Grant OSARES (No. 683300).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Bonakdarpour, B., Finkbeiner, B. (2019). Program Repair for Hyperproperties. In: Chen, YF., Cheng, CH., Esparza, J. (eds) Automated Technology for Verification and Analysis. ATVA 2019. Lecture Notes in Computer Science(), vol 11781. Springer, Cham. https://doi.org/10.1007/978-3-030-31784-3_25
Download citation
DOI: https://doi.org/10.1007/978-3-030-31784-3_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-31783-6
Online ISBN: 978-3-030-31784-3
eBook Packages: Computer ScienceComputer Science (R0)