nach oben

Formal Methods in System Design

14.02.2024

Bounded-memory runtime enforcement with probabilistic and performance analysis

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

Erschienen in: Formal Methods in System Design

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 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.

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 "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

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

Nur mit Berechtigung zugänglich

Storing/ delaying the events (into the internal memory of the enforcer) makes this enforcement mechanism suitable for transactional systems and unsuitable for reactive systems which has to continuously capture and emit events.

For applications/systems where discarding of events is not acceptable, one may use the approach of halting when the above situations raise. For all the applications/systems where halting of the system/enforcer is not acceptable, the proposed approach can be used to minimally discard “idempotent" events and let the enforcer/system continue to operate.

We employ finite-state automata to model and define regular properties. We consider enforcement of all regular properties, where the property to be enforced is modelled/defined as an automaton and given as input to the enforcement mechanism. With each input event, the state of the property automaton progresses, and the potential output is determined based on the state it reaches. For instance, when the automaton depicted in Fig. 2 of Example 1 moves from state \(q_2\) to \(q_0\) (an accepting state), the enforcer generates output by emitting the events accumulated in its internal memory. This occurs because the input word is accepted by the automaton, marked by the attainment of an accepting state.

In various contexts, such as queue-based systems like FIFO (First-In-First-Out), the most obsolete event is an event that was initially encountered or recorded earliest in the timeline.

Within the degraded mode, there exist distinct categories of suppression i.e., suppression due to a lack of future property satisfaction or due to buffer fullness. At present, our framework generates a common degraded mode information (i.e., \(\bot \)) as output for both the types of suppression. However, we plan to provide separate mode information for these cases to users in the future.

The prefix-closed properties are commonly known as safety properties.

The automaton modelling the property of logging of steering commands can be designed using just three states, i.e., one accepting and two non-accepting states. From a non-accepting state (but not a dead state), upon {R,F,L}, it remains at the same non-accepting state, whereas upon S, it makes a transition to an accepting state. Similarly, from the accepting state, upon S, it remains at the same accepting state whereas upon {R,F,L}, it makes the transition to the non-accepting state (but not a dead state). For all other inputs (e.g., E) and from all states, the automaton goes to a dead state. However, we choose to keep the automaton in Fig. 7 as it is close to the automata which can be used for steering the AV.

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.

The input trace can be obtained by driving some miles and recording the commands, or by randomly generating the commands.

aa: accepting state to accepting state, an: accepting state to non-accepting state, likewise.

For instance, when examining an input sequence of length 10, a suitable trace for property \(P_1\) can be aaaaaaaaa2, abcdabcd21, etc. Here, the significant observation is that the digits (which fulfill the property) are positioned at the end of the trace, allowing a higher buffer of events and consequently more frequent invocations of function \(\texttt {clean}\).

Despite enlarging the buffer size and subsequently decreasing the frequency of invoking function \( \texttt {clean} \), the average time taken by function \( \texttt {clean} \) still increases linearly. This outcome arises from the fact that although the function is called fewer times, each invocation involves a larger list of uncorrected events (events in \(\sigma _c\)). The substantial overhead required to manage this expanded list significantly contributes to the heightened average processing time.

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

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, https://doi.org/10.1007/978-3-642-19125-1_6

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, https://doi.org/10.1007/978-3-662-46681-0_51

cinlar E (1969) Markov renewal theory. Adv Appl Probab 1(2):123–187. https://doi.org/10.2307/1426216

Clarke E, Grumberg O, Peled D (2001) Model checking

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

Falcone Y, Fernandez JC, Mounier L (2009) Runtime verification of safety-progress properties. In: Runtime verification, Springer, pp 40–59, https://doi.org/10.1007/978-3-642-04694-0_4

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

Falcone Y, Fernandez J, Mounier L (2012) What can you verify and enforce at runtime? Int J Softw Tools Technol Transf 14(3):349–382. https://doi.org/10.1007/s10009-011-0196-8CrossRef

10.

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

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, https://doi.org/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, https://doi.org/10.1109/SECPRI.2004.1301314

13.

Grimmett G, Stirzaker D (2020) Probability and random processes (4th edition). Oxford University Press

14.

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

15.

Ligatti J, Bauer L, Walker D (2009) Run-time enforcement of nonsafety policies. ACM Trans Inf Syst Secur 10(1145/1455526):1455532

16.

Norris JR (1997) Markov Chains. Cambridge series in statistical and probabilistic mathematics, Cambridge University Press,. https://doi.org/10.1017/CBO9780511810633

17.

Pearce H, Pinisetty S, Roop PS et al (2020) Smart i/o modules for mitigating cyber-physical attacks on industrial control systems. IEEE Transact Ind Inf 16(7):4659–4669. https://doi.org/10.1109/TII.2019.2945520CrossRef

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, https://doi.org/10.1007/978-3-642-35632-2_23

19.

Pinisetty S, Falcone Y, Jéron T et al (2014) Runtime enforcement of timed properties revisited. Formal Methods Syst Design 45(3):381–422. https://doi.org/10.1007/s10703-014-0215-yCrossRef

20.

Pinisetty S, Preoteasa V, Tripakis S et al (2017) Predictive runtime enforcement. Formal Methods Syst Des 51(1):154–199. https://doi.org/10.1007/s10703-017-0271-1CrossRef

21.

Pinisetty S, Roop PS, Smyth S et al (2017) Runtime enforcement of cyber-physical systems. ACM Trans Embed Comput Syst. https://doi.org/10.1145/3126500CrossRef

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, https://doi.org/10.1145/3092282.3092291

23.

Privault N (2018) Discrete-time Markov chains, Springer Singapore, Singapore, pp 89–113. https://doi.org/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, https://doi.org/10.1007/978-3-319-25150-9_31

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. https://doi.org/10.1017/S0960129517000123

26.

Renard M, Rollet A, Falcone Y (2020) Runtime enforcement of timed properties using games. Formal Asp Comput 32(2):315–360. https://doi.org/10.1007/s00165-020-00515-2MathSciNetCrossRef

27.

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

28.

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

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, https://doi.org/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. https://doi.org/10.1016/j.ic.2007.07.009, joint Workshop on foundations of computer security and automated reasoning for security protocol analysis (FCS-ARSPA ’06)

33.

Woodcock J, Larsen PG, Bicarregui J et al (2009) Formal methods: practice and experience. ACM Comput Surv 10(1145/1592434):1592436

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, https://doi.org/10.1007/978-3-319-40648-0_6

Titel: Bounded-memory runtime enforcement with probabilistic and performance analysis
verfasst von: Saumya Shankar
Ankit Pradhan
Srinivas Pinisetty
Antoine Rollet
Yliès Falcone
Publikationsdatum: 14.02.2024
Verlag: Springer US
Erschienen in: Formal Methods in System Design
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI: https://doi.org/10.1007/s10703-024-00446-1

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 "Wirtschaft"

Springer Professional "Technik"

Premium Partner