nach oben

Erschienen in:

2022 | OriginalPaper | Buchkapitel

Bounded-Memory Runtime Enforcement

verfasst von : Saumya Shankar, Antoine Rollet, Srinivas Pinisetty, Yliès Falcone

Erschienen in: Model Checking Software

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Runtime Enforcement (RE) is a monitoring technique to ensure that a system obeys a set of formal requirements (properties). RE employs an enforcer (a safety wrapper for the system) which modifies the (untrustworthy) output by performing actions such as delaying (by storing/buffering) and suppressing events, when needed. In this paper, to handle practical applications with memory constraints, we propose a new RE paradigm where the memory of the enforcer is bounded/finite. Besides the property to be enforced, the user specifies a bound on the enforcer memory. Bounding the memory poses various challenges such as how to handle the situation when the memory is full, how to optimally discard events from the buffer to accommodate new events and let the enforcer continue operating. We define the bounded-memory RE problem and develop a framework for any regular property. The proposed framework is implemented and its performance evaluated via some examples from application scenarios indicates that the enforcer has reasonable execution time overhead.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Verifying the SHA-3 Implementation from OpenSSL with the Software Analysis Workbench

Nächstes Kapitel Solving String Theories Involving Regular Membership Predicates Using SAT

A dead state is represented by a square throughout the paper.

Experiments were conducted on an Intel Core i7-9700K CPU at 3.60GHz \( \times \) 8, with 32 GB RAM, and running on Ubuntu 18.04.5 LTS.

Beauquier, D., Cohen, J., Lanotte, R.: Security policies enforcement using finite and pushdown edit automata. Int. J. Inf. Sec. 12(4), 319–336 (2013). https://doi.org/10.1007/s10207-013-0195-8, http://dx.doi.org/10.1007/s10207-013-0195-8

Bielova, N., Massacci, F.: Predictability of enforcement. In: Erlingsson, Ú., Wieringa, R., Zannone, N. (eds.) ESSoS 2011. LNCS, vol. 6542, pp. 73–86. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19125-1_6CrossRef

Bloem, R., Könighofer, B., Könighofer, R., Wang, C.: Shield synthesis. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 533–548. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_51CrossRefMATH

Dolzhenko, E., Ligatti, J., Reddy, S.: Modeling runtime enforcement with mandatory results automata. Int. J. Inf. Secur. 14(1), 47–60 (2015). https://doi.org/10.1007/s10207-014-0239-8

Falcone, Y., Fernandez, J.-C., Mounier, L.: Runtime verification of safety-progress properties. In: Bensalem, S., Peled, D.A. (eds.) RV 2009. LNCS, vol. 5779, pp. 40–59. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04694-0_4CrossRef

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). https://doi.org/10.1007/s10009-011-0196-8

Falcone, Y., Jéron, T., Marchand, H., Pinisetty, S.: Runtime enforcement of regular timed properties by suppressing and delaying events. Syst. Control Lett. 123, 2–41 (2016). https://doi.org/10.1016/j.scico.2016.02.008CrossRef

Falcone, Y., Mariani, L., Rollet, A., Saha, S.: Runtime failure prevention and reaction. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Verification. LNCS, vol. 10457, pp. 103–134. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-75632-5_4CrossRef

Falcone, Y., Mounier, L., Fernandez, J., Richier, J.: Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Formal Methods Syst. Des. 38(3), 223–262 (2011). https://doi.org/10.1007/s10703-011-0114-4

10.

Fong, P.W.L.: Access control by tracking shallow execution history. In: IEEE Symposium on Security and Privacy, 2004. Proceedings. 2004, pp. 43–55 (2004). https://doi.org/10.1109/SECPRI.2004.1301314

11.

Ligatti, J., Bauer, L., Walker, D.: Edit automata: enforcement mechanisms for run-time security policies. Int. J. Inf. Sec. 4(1-2), 2–16 (2005). https://doi.org/10.1007/s10207-004-0046-8

12.

Ligatti, J., Bauer, L., Walker, D.: Run-time enforcement of nonsafety policies. ACM Trans. Inf. Syst. Secur. 12(3) (2009). https://doi.org/10.1145/1455526.1455532, https://doi.org/10.1007/s10207-004-0046-8

13.

Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H., Rollet, A., Nguena Timo, O.: Runtime enforcement of timed properties revisited. Formal Methods Syst. Des. 45(3), 381–422 (2014). https://doi.org/10.1007/s10703-014-0215-yCrossRefMATH

14.

Pinisetty, S., Falcone, Y., Jéron, T., Marchand, H., Rollet, A., Nguena Timo, O.L.: Runtime enforcement of timed properties. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 229–244. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35632-2_23CrossRefMATH

15.

Pinisetty, S., Preoteasa, V., Tripakis, S., Jéron, T., Falcone, Y., Marchand, H.: Predictive runtime enforcement. Formal Methods Syst. Des. 51(1), 154–199 (2017). https://doi.org/10.1007/s10703-017-0271-1

16.

Pinisetty, S., Roop, P.S., Smyth, S., Tripakis, S., Hanxleden, R.V.: Runtime enforcement of reactive systems using synchronous enforcers. In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, pp. 80–89 (2017)

17.

Renard, M., Falcone, Y., Rollet, A., Jéron, T., Marchand, H.: Optimal enforcement of (timed) properties with uncontrollable events. Math. Struct. Comput. Sci. 1–46 (2017). https://doi.org/10.1017/S0960129517000123

18.

Renard, M., Falcone, Y., Rollet, A., Pinisetty, S., Jéron, T., Marchand, H.: Enforcement of (timed) properties with uncontrollable events. In: Theoretical Aspects of Computing - ICTAC 2015–12th International Colloquium Cali, Colombia, October 29–31, 2015, Proceedings, pp. 542–560 (2015). https://doi.org/10.1007/978-3-319-25150-9_31

19.

Renard, M., Rollet, A., Falcone, Y.: Runtime enforcement of timed properties using games. Formal Aspects Comput. 32(2), 315–360 (2020)MathSciNetCrossRefMATH

20.

Roc SU, G.: On safety properties and their monitoring. Sci. Ann. Comput. Sci. 22(2), 327–365 (2012). https://doi.org/10.7561/SACS.2012.2.327

21.

Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30–50 (2000). https://doi.org/10.1145/353323.353382CrossRef

22.

Talhi, C., Tawbi, N., Debbabi, M.: Execution monitoring enforcement under memory-limitation constraints. Inf. Comput. 206(2), 158–184 (2008). https://doi.org/10.1016/j.ic.2007.07.009, https://www.sciencedirect.com/science/article/pii/S0890540107001320, joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCS-ARSPA 2006)

23.

Wu, M., Zeng, H., Wang, C.: Synthesizing runtime enforcer of safety properties under burst error. In: NASA Formal Methods - 8th International Symposium, NFM 2016, Minneapolis, MN, USA, 7–9 June 2016, Proceedings, pp. 65–81 (2016). https://doi.org/10.1007/978-3-319-40648-0_6

Titel: Bounded-Memory Runtime Enforcement
verfasst von: Saumya Shankar
Antoine Rollet
Srinivas Pinisetty
Yliès Falcone
Verlag: Springer International Publishing
Buch: Model Checking Software
Print ISBN: 978-3-031-15076-0

Electronic ISBN: 978-3-031-15077-7

Copyright-Jahr: 2022
DOI: https://doi.org/10.1007/978-3-031-15077-7_7

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner