×

Monitorable hyperproperties of nonterminating systems. (English) Zbl 07576526

Summary: Runtime monitoring for a hyperproperty is aimed at giving a verdict of satisfaction or violation on the whole system under monitoring, and not on its individual execution traces. Indeed, a monitor for a hyperproperty should naturally be able to observe prefixes of several different traces of the system and establish the relationships among them at run time. The traces of nonterminating systems, however, are of infinite length, and the monitor cannot normally observe anything other than the prefixes of only one single running trace. In this paper, we study the feasibility of monitoring nonterminating systems against hyperproperties. To do so, we introduce single-trace monitorability as a novel conception of a monitorable hyperproperty, and illustrate that the members of only one particular, small class of hyperproperties are monitorable if no prior knowledge about the system under monitoring is available. The concept of single-trace monitorability is then generalized to the environments where the monitor has access to an under/over-approximation of the set of the traces that may occur at run time. We investigate the closure properties of the set of monitorable hyperproperties given an approximation, and study the relationships among the proposed notions of monitorability.

MSC:

68-XX Computer science
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Lamport, L., Proving the correctness of multiprocess programs, IEEE Trans. Softw. Eng., 3, 2, 125-143 (1977) · Zbl 0349.68006
[2] Clarkson, M. R.; Schneider, F. B., Hyperproperties, J. Comput. Secur., 18, 6, 1157-1210 (2010)
[3] Goguen, J. A.; Meseguer, J., Security policies and security models, (Proceedings of the IEEE Symposium on Security and Privacy (S&P’82). Proceedings of the IEEE Symposium on Security and Privacy (S&P’82), Oakland, CA, USA, April 26-28, 1982 (1982), IEEE Computer Society), 11-20
[4] Zdancewic, S.; Myers, A. C., Observational determinism for concurrent program security, (Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW’03). Proceedings of the 16th IEEE Computer Security Foundations Workshop (CSFW’03), Pacific Grove, CA, USA, June 30-July 2, 2003 (2003), IEEE Computer Society), 29-43
[5] Falcone, Y.; Fernandez, J.; Mounier, L., What can you verify and enforce at runtime?, Int. J. Softw. Tools Technol. Transf., 14, 3, 349-382 (2012)
[6] Leucker, M.; Schallhart, C., A brief account of runtime verification, J. Log. Algebraic Methods Program., 78, 5, 293-303 (2009) · Zbl 1192.68433
[7] Pnueli, A.; Zaks, A., PSL model checking and run-time verification via testers, (Proceedings of the 14th International Symposium on Formal Methods (FM’06). Proceedings of the 14th International Symposium on Formal Methods (FM’06), Hamilton, Canada, August 21-27, 2006. Proceedings of the 14th International Symposium on Formal Methods (FM’06). Proceedings of the 14th International Symposium on Formal Methods (FM’06), Hamilton, Canada, August 21-27, 2006, LNCS, vol. 4085 (2006), Springer), 573-586
[8] Agrawal, S.; Bonakdarpour, B., Runtime verification of k-safety hyperproperties in HyperLTL, (Proceedings of the IEEE 29th Computer Security Foundations Symposium (CSF’16). Proceedings of the IEEE 29th Computer Security Foundations Symposium (CSF’16), Lisbon, Portugal, June 27-July 1, 2016 (2016), IEEE Computer Society), 239-252
[9] Brett, N.; Siddique, U.; Bonakdarpour, B., Rewriting-based runtime verification for alternation-free HyperLTL, (Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17). Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17), Uppsala, Sweden, April 22-29, 2017. Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17). Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’17), Uppsala, Sweden, April 22-29, 2017, LNCS, vol. 10206 (2017), Springer), 77-93 · Zbl 1452.68114
[10] Pinisetty, S.; Schneider, G.; Sands, D., Runtime verification of hyperproperties for deterministic programs, (Proceedings of the 6th Conference on Formal Methods in Software Engineering (FormaliSE’18). Proceedings of the 6th Conference on Formal Methods in Software Engineering (FormaliSE’18), Gothenburg, Sweden, June 2, 2018 (2018), ACM), 20-29
[11] Finkbeiner, B.; Hahn, C.; Stenger, M.; Tentrup, L., Monitoring hyperproperties, Form. Methods Syst. Des., 54, 3, 336-363 (2019) · Zbl 1425.68254
[12] Harel, D.; Pnueli, A., On the development of reactive systems, (Proceedings of the Logics and Models of Concurrent Systems. Proceedings of the Logics and Models of Concurrent Systems, Colle-sur-Loup, France, October 8-19, 1984 (1984), Springer), 477-498 · Zbl 0581.68046
[13] Manna, Z.; Pnueli, A., The Temporal Logic of Reactive and Concurrent Systems - Specification (1992), Springer
[14] Stucki, S.; Sánchez, C.; Schneider, G.; Bonakdarpour, B., Gray-box monitoring of hyperproperties with an application to privacy, Form. Methods Syst. Des., 58, 126-159 (2021) · Zbl 1502.68187
[15] Clarkson, M. R.; Finkbeiner, B.; Koleini, M.; Micinski, K. K.; Rabe, M. N.; Sánchez, C., Temporal logics for hyperproperties, (Proceedings of the 3rd International Conference on Principles of Security and Trust (POST’14). Proceedings of the 3rd International Conference on Principles of Security and Trust (POST’14), Grenoble, France, April 5-13, 2014. Proceedings of the 3rd International Conference on Principles of Security and Trust (POST’14). Proceedings of the 3rd International Conference on Principles of Security and Trust (POST’14), Grenoble, France, April 5-13, 2014, LNCS, vol. 8414 (2014), Springer), 265-284
[16] Pnueli, A., The temporal logic of programs, (Proceedings of the 18th Annual Symposium on Foundations of Computer Science. Proceedings of the 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, October 31-November 1, 1977 (1977), IEEE Computer Society), 46-57
[17] Bonakdarpour, B.; Sánchez, C.; Schneider, G., Monitoring hyperproperties by combining static analysis and runtime verification, (Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’18). Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’18), Limassol, Cyprus, November 5-9, 2018. Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’18). Proceedings of the 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA’18), Limassol, Cyprus, November 5-9, 2018, LNCS, vol. 11245 (2018), Springer), 8-27
[18] Hsu, T.; Sánchez, C.; Bonakdarpour, B., Bounded model checking for hyperproperties, (Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’21). Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’21), Luxembourg City, Luxembourg, March 27-April 1, 2021. Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’21). Proceedings of the 27th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’21), Luxembourg City, Luxembourg, March 27-April 1, 2021, LNCS, vol. 12651 (2021), Springer), 94-112 · Zbl 1467.68086
[19] Shamir, A., How to share a secret, Commun. ACM, 22, 11, 612-613 (1979) · Zbl 0414.94021
[20] Hahn, C.; Stenger, M.; Tentrup, L., Constraint-based monitoring of hyperproperties, (Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’19). Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’19), Prague, Czech Republic, April 6-11, 2019. Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’19). Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’19), Prague, Czech Republic, April 6-11, 2019, LNCS, vol. 11428 (2019), Springer), 115-131
[21] Bonakdarpour, B.; Finkbeiner, B., The complexity of monitoring hyperproperties, (Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF’18). Proceedings of the 31st IEEE Computer Security Foundations Symposium (CSF’18), Oxford, United Kingdom, July 9-12, 2018 (2018), IEEE Computer Society), 162-174
[22] Finkbeiner, B.; Hahn, C.; Stenger, M.; Tentrup, L., RVHyper: a runtime verification tool for temporal hyperproperties, (Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18). Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18), Thessaloniki, Greece, April 14-20, 2018. Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18). Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’18), Thessaloniki, Greece, April 14-20, 2018, LNCS, vol. 10806 (2018), Springer), 194-200
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.