×

Bounded-memory runtime enforcement with probabilistic and performance analysis. (English) Zbl 07873309

Summary: Runtime Enforcement (RE) is a technique aimed at monitoring the executions of a system at runtime and ensure its compliance against 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. All of our results are formalized and proved. We also analyze probabilistically how much memory is required on an average case for a given regular property, such that the output of the bounded enforcer is equal to that of the unbounded enforcer up to a fixed probability. The proposed framework is implemented and a case study is worked out to show the practicability and usefulness of the bounded enforcer in the real-world and to show the usage of the aforementioned probabilistic analysis on them. The performance is evaluated via some examples from application scenarios and it indicates linear changes in the execution time of the enforcers in response to increases in trace length, property complexity, and buffer sizes.

MSC:

68-XX Computer science

Software:

GitHub
Full Text: DOI

References:

[1] Beauquier, D.; Cohen, J.; Lanotte, R., Security policies enforcement using finite and pushdown edit automata, Int J Inf Secur, 12, 4, 319-336, 2013 · doi:10.1007/s10207-013-0195-8
[2] Bielova N, Massacci F (2011) Predictability of enforcement. In: Proceedings of the third international conference on engineering secure software and systems. Springer-Verlag, Berlin, Heidelberg, ESSoS’11, p 73-86, doi:10.1007/978-3-642-19125-1_6
[3] Bloem R, Könighofer B, Könighofer R, et al (2015) Shield synthesis: runtime enforcement for reactive systems. In: Baier C, Tinelli C (eds.) Tools and algorithms for the construction and analysis of systems. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 533-548, doi:10.1007/978-3-662-46681-0_51 · Zbl 1420.68119
[4] cinlar E (1969) Markov renewal theory. Adv Appl Probab 1(2):123-187. doi:10.2307/1426216 · Zbl 0212.49601
[5] Clarke E, Grumberg O, Peled D (2001) Model checking
[6] Dolzhenko, E.; Ligatti, J.; Reddy, S., Modeling runtime enforcement with mandatory results automata, Int J Inf Secur, 14, 1, 47-60, 2015 · doi:10.1007/s10207-014-0239-8
[7] Falcone Y, Fernandez JC, Mounier L (2009) Runtime verification of safety-progress properties. In: Runtime verification, Springer, pp 40-59, doi:10.1007/978-3-642-04694-0_4
[8] Falcone, Y.; Mounier, L.; Fernandez, J., Runtime enforcement monitors: composition, synthesis, and enforcement abilities, Formal Methods Syst Des, 38, 3, 223-262, 2011 · Zbl 1219.68089 · doi:10.1007/s10703-011-0114-4
[9] 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 · doi:10.1007/s10009-011-0196-8
[10] Falcone, Y.; Jéron, T.; Marchand, H., Runtime enforcement of regular timed properties by suppressing and delaying events, Syst Control Lett, 123, 2-41, 2016 · doi:10.1016/j.scico.2016.02.008
[11] Falcone Y, Mariani L, Rollet A, et al (2018) Runtime failure prevention and reaction. In: Lectures on runtime verification—introductory and advanced topics. pp 103-134, doi:10.1007/978-3-319-75632-5_4
[12] Fong PWL (2004) Access control by tracking shallow execution history. In: IEEE symposium on security and privacy, 2004. Proceedings. 2004, pp 43-55, doi:10.1109/SECPRI.2004.1301314
[13] Grimmett, G.; Stirzaker, D., Probability and random processes (4th edition), 2020, Oxford University Press
[14] Ligatti, J.; Bauer, L.; Walker, D., Edit automata: enforcement mechanisms for run-time security policies, Int J Inf Secur, 4, 1-2, 2-16, 2005 · doi:10.1007/s10207-004-0046-8
[15] Ligatti, J.; Bauer, L.; Walker, D., Run-time enforcement of nonsafety policies, ACM Trans Inf Syst Secur, 10, 1145-1455526, 1455532, 2009
[16] Norris JR (1997) Markov Chains. Cambridge series in statistical and probabilistic mathematics, Cambridge University Press,. doi:10.1017/CBO9780511810633 · Zbl 0873.60043
[17] Pearce, H.; Pinisetty, S.; Roop, PS, Smart i/o modules for mitigating cyber-physical attacks on industrial control systems, IEEE Transact Ind Inf, 16, 7, 4659-4669, 2020 · doi:10.1109/TII.2019.2945520
[18] Pinisetty S, Falcone Y, Jéron T, et al (2012) Runtime enforcement of timed properties. In: Qadeer S, Tasiran S (eds) Runtime verification, third international conference, RV 2012, Istanbul, Turkey, September 25-28, 2012, Revised Selected Papers, Lecture Notes in Computer Science, vol 7687. Springer, pp 229-244, doi:10.1007/978-3-642-35632-2_23
[19] Pinisetty, S.; Falcone, Y.; Jéron, T., Runtime enforcement of timed properties revisited, Formal Methods Syst Design, 45, 3, 381-422, 2014 · Zbl 1314.68102 · doi:10.1007/s10703-014-0215-y
[20] Pinisetty, S.; Preoteasa, V.; Tripakis, S., Predictive runtime enforcement, Formal Methods Syst Des, 51, 1, 154-199, 2017 · Zbl 1370.68207 · doi:10.1007/s10703-017-0271-1
[21] Pinisetty, S.; Roop, PS; Smyth, S., Runtime enforcement of cyber-physical systems, ACM Trans Embed Comput Syst, 2017 · doi:10.1145/3126500
[22] Pinisetty S, Roop PS, Smyth S, et al (2017c) 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, doi:10.1145/3092282.3092291
[23] Privault N (2018) Discrete-time Markov chains, Springer Singapore, Singapore, pp 89-113. doi:10.1007/978-981-13-0659-4_4
[24] Renard M, Falcone Y, Rollet A, et al (2015) Enforcement of (timed) properties with uncontrollable events. In: Theoretical aspects of computing - ICTAC 2015 - 12th international colloquium Cali, Colombia, 2015, Proceedings, pp 542-560, doi:10.1007/978-3-319-25150-9_31 · Zbl 1407.68300
[25] Renard M, Falcone Y, Rollet A, et al (2017) Optimal enforcement of (timed) properties with uncontrollable events. Math Struct Comput Sci pp 1-46. doi:10.1017/S0960129517000123
[26] Renard, M.; Rollet, A.; Falcone, Y., Runtime enforcement of timed properties using games, Formal Asp Comput, 32, 2, 315-360, 2020 · Zbl 1458.68120 · doi:10.1007/s00165-020-00515-2
[27] Roc su, G., On safety properties and their monitoring, Sci Ann Comput Sci, 22, 2, 327-365, 2012 · Zbl 1424.68043 · doi:10.7561/SACS.2012.2.327
[28] Schneider, FB, Enforceable security policies, ACM Trans Inf Syst Secur, 3, 1, 30-50, 2000 · doi:10.1145/353323.353382
[29] Shankar S (2022) Bounded-memory runtime enforcer. https://github.com/saumyashankarsinha/BMRE
[30] Shankar S, R UV, Pinisetty S, et al (2020) Formal runtime monitoring approaches for autonomous vehicles. In: Benedictis RD, Geretti L, Micheli A (eds.) Proceedings of the 2nd workshop on artificial intelligence and formal verification, Logic, Automata, and Synthesis hosted by the Bolzano Summer of Knowledge 2020 (BOSK 2020), September 25, 2020, CEUR Workshop Proceedings, vol 2785. CEUR-WS.org, pp 89-94, http://ceur-ws.org/Vol-2785/paper15.pdf
[31] Shankar S, Rollet A, Pinisetty S, et al (2022) Bounded-memory runtime enforcement. In: Legunsen O, Rosu G (eds) Model checking software. Springer International Publishing, Cham, pp 114-133, doi:10.1007/978-3-031-15077-7_7
[32] Talhi C, Tawbi N, Debbabi M (2008) Execution monitoring enforcement under memory-limitation constraints. Inf Comput 206(2):158-184. doi:10.1016/j.ic.2007.07.009, joint Workshop on foundations of computer security and automated reasoning for security protocol analysis (FCS-ARSPA ’06) · Zbl 1146.68356
[33] Woodcock, J.; Larsen, PG; Bicarregui, J., Formal methods: practice and experience, ACM Comput Surv, 10, 1145-1592434, 1592436, 2009
[34] Wu M, Zeng H, Wang C (2016) Synthesizing runtime enforcer of safety properties under burst error. In: NASA formal methods—8th international symposium, NFM 2016, Minneapolis, MN, USA, 2016, Proceedings, pp 65-81, doi:10.1007/978-3-319-40648-0_6
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.