Top

Annals of Telecommunications

Published in:

17-04-2023

A modular pipeline for enforcement of security properties at runtime

Authors: Rania Taleb, Sylvain Hallé, Raphaël Khoury

Published in: Annals of Telecommunications | Issue 7-8/2023

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Runtime enforcement ensures the respect of a user-specified security policy by a program by providing a valid replacement for any misbehaving sequence of events that may occur during that program’s execution. However, depending on the capabilities of the enforcement mechanism, multiple possible replacement sequences may be available, and the current literature is silent on the question of how to choose the optimal one. Furthermore, the current design of runtime monitors imposes a substantial burden on the designer, since the entirety of the monitoring task is accomplished by a monolithic construct, usually an automata-based model. In this paper, we propose a new modular model of enforcement monitors, in which the tasks of altering the execution, ensuring compliance with the security policy, and selecting the optimal replacement are split into three separate modules, which simplifies the creation of runtime monitors. We implement this approach by using the event stream processor BeepBeep and a use case is presented. Experimental evaluation shows that our proposed framework can dynamically select an adequate enforcement actions at runtime, without the need to manually define an enforcement monitor.

previous article HistoTrust: tracing AI behavior with secure hardware and blockchain technology

next article Secure and low PAPR OFDM system using TCCM

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

When used as a proxy in our enforcement pipeline, the Mealy machine of Fig. 19 does not create this issue, as on the second c⁺ input event, control is not switched to the enforcement pipeline as no violation is detected.

Ancona D, Dagnino F, Franceschini L (2018) A formalism for specification of java API interfaces. In: Dolby J, Halfond WGJ, Mishra A (eds) Companion Proceedings for the ISSTA/ECOOP 2018 Workshops, ISSTA 2018, Amsterdam, Netherlands, July 16-21, 2018. ACM, pp 24–26. https://doi.org/10.1145/3236454.3236476

Avalle M, Pironti A, Sisto R (2014) Formal verification of security protocol implementations: a survey. Form Asp Comput 26(1):99–123. https://doi.org/10.1007/s00165-012-0269-9CrossRef

Bartocci E, Majumdar R (eds.) (2015) Runtime Verification – 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings, Lecture Notes in Computer Science. Springer, vol 9333 https://doi.org/10.1007/978-3-319-23820-3

Bartocci E, Falcone Y, Francalanza A et al (2018) Introduction to runtime verification. In: Bartocci E, Falcone Y (eds) Lectures on runtime verification - introductory and advanced topics, Lecture Notes in Computer Science, vol 10457. Springer, pp 1–33. https://doi.org/10.1007/978-3-319-75632-5_1

Bauer A, Jürjens J (2010) Runtime verification of cryptographic protocols. Comput Secur 29(3):315–330. https://doi.org/10.1016/j.cose.2009.09.003, https://www.sciencedirect.com/science/article/pii/S0167404809001047. special issue on software engineering for secure systemsCrossRef

Bauer A, Leucker M, Schallhart C (2006) Monitoring of real-time properties. In: Arun-Kumar S, Garg N (eds) FSTTCS 2006: Foundations of Software Technology and Theoretical Computer Science, 26th International Conference, Kolkata, India, December 13-15, 2006, Proceedings, Lecture Notes in Computer Science, vol 4337. Springer, pp 260–272. https://doi.org/10.1007/11944836_25

Bauer A, Leucker M, Schallhart C (2007) The good, the bad, and the ugly, but how ugly is ugly? In: Sokolsky O, Tasiran S (eds) Runtime Verification, 7th International Workshop, RV 2007, Vancouver, Canada, March 13, 2007, Revised Selected Papers, Lecture Notes in Computer Science, vol 4839. Springer, pp 126–138. https://doi.org/10.1007/978-3-540-77395-5_11

Bauer A, Leucker M, Schallhart C (2010) Comparing LTL semantics for runtime verification. J Log Comput 20(3):651–674MathSciNetCrossRefMATH

Bauer A, Leucker M, Schallhart C (2011) Runtime verification for LTL and TLTL. ACM Trans Softw Eng Methodol 20(4):14:1–14:64. https://doi.org/10.1145/2000799.2000800CrossRef

10.

Bauer L, Ligatti J, Walker D (2002) More enforceable security policies. In: In foundations of computer security

11.

Beauquier D, Cohen J, Lanotte R (2013) Security policies enforcement using finite and pushdown edit automata. Int J Inf Sec 12(4):319–336CrossRefMATH

12.

Betti Q, Montreuil B, Khoury R et al (2020) Smart contracts-enabled simulation for hyperconnected logistics. Springer International Publishing, Cham, pp 109–149

13.

Bielova N, Massacci F (2011a) Do you really mean what you actually enforced? Int J of Inf Security :1–16. https://doi.org/10.1007/s10207-011-0137-2

14.

Bielova N, Massacci F (2011b) Do you really mean what you actually enforced? – edited automata revisited. Int J Inf Sec 10(4):239–254CrossRef

15.

Bielova N, Massacci F (2012) Iterative enforcement by suppression: towards practical enforcement theories. J Comput Secur 20(1)

16.

Bodden E, Hendren LJ, Lam P et al (2010) Collaborative runtime verification with tracematches. J Log Comput 20(3):707–723. https://doi.org/10.1093/logcom/exn077MathSciNetCrossRefMATH

17.

Boussaha MR, Khoury R, Hallé S (2017) Monitoring of security properties using BeepBeep. In: Imine A, Fernandez JM, Marion J et al (eds) Foundations and Practice of Security – 10th International Symposium, FPS 2017, Nancy, France, October 23-25, 2017, Revised Selected Papers, Lecture Notes in Computer Science, vol 10723. Springer, pp 160–169. https://doi.org/10.1007/978-3-319-75650-9_11

18.

Chabot H, Khoury R, Tawbi N (2011) Extending the enforcement power of truncation monitors using static analysis. pp 194–207

19.

Chang E, Manna Z, Pnueli A (1993) The safety-progress classification. In: Bauer FL, Brauer W, Schwichtenberg H (eds) Logic and algebra of specification. Springer, Berlin, pp 143–202

20.

Chen F, Meredith PO, Jin D et al (2009) Efficient formalism-independent monitoring of parametric properties. In: ASE. IEEE Computer Society, pp 383–394

21.

Colombo C, Pace GJ, Schneider G (2009) LARVA—safer monitoring of real-time java programs (tool paper). In: Hung DV, Krishnan P (eds) 7th IEEE international conference on software engineering and formal methods, SEFM 2009, Hanoi, Vietnam, 23–27 November 2009. IEEE Computer Society, pp 33–37. https://doi.org/10.1109/SEFM.2009.13

22.

Colombo C, Ellul J, Pace GJ (2018) Contracts over smart contracts: recovering from violations dynamically. In: Margaria T, Steffen B (eds) ISoLA 2018, LNCS, vol 11247. Springer, pp 300–315

23.

Convent L, Hungerecker S, Leucker M, etal (2018) TeSSLa: Temporal stream-based specification language. In: Massoni T, Mousavi MR (eds) Formal methods: foundations and applications - 21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26–30, 2018, Proceedings, Lecture Notes in Computer Science, vol 11254. Springer, pp 144–162. https://doi.org/10.1007/978-3-030-03044-5_10

24.

D’Angelo B, Sankaranarayanan S, Sánchez C et al (2005) LOLA: runtime monitoring of synchronous systems. In: TIME. IEEE Computer Society, pp 166–174

25.

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

26.

Dolzhenko E, Ligatti J, Reddy S (2015b) Modeling runtime enforcement with mandatory results automata. Int J Inf Secur 14(1):47–60CrossRef

27.

Drábik P, Martinelli F, Morisset C (2012a) Cost-aware runtime enforcement of security policies. In: Jøsang A, Samarati P, Petrocchi M (eds) STM, LNCS, vol 7783. Springer, pp 1–16

28.

Drábik P, Martinelli F, Morisset C (2012b) A quantitative approach for inexact enforcement of security policies. In: Gollmann D, Freiling FC (eds) ISC 2012, LNCS, vol 7483. Springer, pp 306–321

29.

Erlingsson U (2004) The inlined reference monitor approach to security policy enforcement. PhD thesis, USA, aAI3114521

30.

Falcone Y, Salaün G (2021) Runtime enforcement with reordering, healing, and suppression. In: Calinescu R, Pasareanu CS (eds) Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings, Lecture Notes in Computer Science, vol 13085. Springer, pp 47–65. https://doi.org/10.1007/978-3-030-92124-8_3

31.

Falcone Y, Mounier L, Fernandez JC et al (2011) Runtime enforcement monitors: composition, synthesis, and enforcement abilities. Form Methods Syst Des 38(3):223–262CrossRefMATH

32.

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

33.

Falcone Y, Mariani L, Rollet A et al (2018) Runtime failure prevention and reaction. In: Bartocci E, Falcone Y (eds) Lectures on runtime verification – introductory and advanced topics, LNCS, vol 10457. Springer, pp 103–134

34.

Fong PWL (2004) Access control by tracking shallow execution history. In: S&P 2004. IEEE Computer Society, pp 43–55

35.

Frigeri A, Pasquale L, Spoletini P (2014) Fuzzy time in linear temporal logic. ACM Trans Comput Log 15(4):30:1–30:22MathSciNetCrossRefMATH

36.

Hallé S, Khoury R (2017) Event stream processing with beepbeep 3. In: Reger G, Havelund K (eds) RV-CuBES 2017. An International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, September 15, 2017, Seattle, WA, USA, Kalpa Publications in Computing, vol 3. EasyChair, pp 81–88. https://doi.org/10.29007/4cth

37.

Hallé S, Khoury R (2018) Writing domain-specific languages for BeepBeep. In: Colombo C, Leucker M (eds) RV, LNCS, vol 11237. Springer, pp 447–457. https://doi.org/10.1007/978-3-030-03769-7_27

38.

Hallé S, Gaboury S, Bouchard B (2016) Activity recognition through complex event processing: first findings. In: Bouchard B, Giroux S, Bouzouane A et al (eds) Artificial intelligence applied to assistive technologies and smart environments, Papers from the 2016 AAAI Workshop, Phoenix, Arizona, USA, February 12, 2016, AAAI Technical Report, vol WS-16-01. AAAI Press. http://www.aaai.org/ocs/index.php/WS/AAAIW16/paper/view/12561

39.

Hallé S, Khoury R, Awesso M (2018) Streamlining the inclusion of computer experiments in a research paper. Computer 51(11):78–89. https://doi.org/10.1109/MC.2018.2876075CrossRef

40.

Hallé S (2018) Event stream processing with BeepBeep 3: log crunching and analysis made easy. Presses de l’Université du Québec

41.

Hallé S, Villemaire R (2008) Runtime monitoring of message-based workflows with data. pp 63–72. https://doi.org/10.1109/EDOC.2008.32

42.

Hamlen KW, Morrisett JG, Schneider FB (2006a) Computability classes for enforcement mechanisms. ACM Trans Program Lang Syst 28(1):175–205CrossRef

43.

Hamlen KW, Morrisett JG, Schneider FB (2006b) Computability classes for enforcement mechanisms. ACM Trans Program Lang Syst 28(1):175–205. https://doi.org/10.1145/1111596.1111601CrossRef

44.

Havelund K, Goldberg A (2008) Verify your runs, vol 4171, pp 374–383. https://doi.org/10.1007/978-3-540-69149-5_40

45.

Jaksic S, Bartocci E, Grosu R et al (2018) Quantitative monitoring of STL with edit distance. Formal Methods Syst Des 53(1):83–112. https://doi.org/10.1007/s10703-018-0319-xCrossRefMATH

46.

Khoury R, Hallé S (2015a) Runtime enforcement with partial control. In: García-Alfaro J, Kranakis E, Bonfante G (eds) FPS 2015, LNCS, vol 9482. Springer, pp 102–116

47.

Khoury R, Hallé S (2015b) Runtime enforcement with partial control. In: García-Alfaro J, Kranakis E, Bonfante G (eds) Foundations and Practice of Security - 8th International Symposium, FPS 2015, Clermont-Ferrand, France, October 26-28, 2015, Revised Selected Papers, Lecture Notes in Computer Science, vol 9482. Springer, pp 102–116. https://doi.org/10.1007/978-3-319-30303-1_7

48.

Khoury R, Hallé S (2018) Tally keeping-LTL: an LTL semantics for quantitative evaluation of LTL specifications. In: IRI 2018. IEEE, pp 495–502

49.

Khoury R, Tawbi N (2012a) Corrective enforcement: a new paradigm of security policy enforcement by monitors. ACM Trans Inf Syst Secur 15(2):10CrossRef

50.

Khoury R, Tawbi N (2012b) Which security policies are enforceable by runtime monitors? A survey. Comput Sci Rev 6(1):27–45CrossRefMATH

51.

Khoury R, Hallé S, Waldmann O (2016) Execution trace analysis using LTL-FO ˆ+. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation: discussion, dissemination, applications - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II, pp 356–362. https://doi.org/10.1007/978-3-319-47169-3_26

52.

Kiczales G, Lamping J, Mendhekar A et al (1997) Aspect-oriented programming. In: European conference on object-oriented programming. Springer, pp 220–242

53.

Koymans R (1990) Specifying real-time properties with metric temporal logic. Real Time Syst 2(4):255–299. https://doi.org/10.1007/BF01995674CrossRef

54.

Legunsen O, Marinov D, Rosu G (2015) Evolution-aware monitoring-oriented programming. In: Bertolino A, Canfora G, Elbaum S G (eds) 37th IEEE/ACM international conference on software engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, vol 2. IEEE Computer Society, pp 615–618. https://doi.org/10.1109/ICSE.2015.206

55.

Leucker M, Schallhart C (2009) A brief account of runtime verification. J Log Algebraic Methods Program 78(5):293–303. https://doi.org/10.1016/j.jlap.2008.08.004CrossRefMATH

56.

Manna Z, Pnueli A (1995) Temporal verification of reactive systems - safety. Springer, BerlinCrossRefMATH

57.

Mealy GH (1955) A method for synthesizing sequential circuits. Bell Syst Tech J 34(5):1045–1079. https://doi.org/10.1002/j.1538-7305.1955.tb03788.xMathSciNetCrossRef

58.

Pace GJ, Pardo R, Schneider G (2016) On the runtime enforcement of evolving privacy policies in online social networks. In: Margaria T, Steffen B (eds) Leveraging applications of formal methods, verification and validation: discussion, dissemination, applications - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part II, pp 407–412. https://doi.org/10.1007/978-3-319-47169-3_33

59.

Pinisetty S, Falcone Y, Jéron T et al (2013) Runtime enforcement of timed properties. In: Qadeer S, Tasiran S (eds) Runtime verification. Springer, Berlin, pp 229–244

60.

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-1CrossRefMATH

61.

Pnueli A (1977) The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October - 1 November 1977. IEEE Computer Society, pp 46–57. https://doi.org/10.1109/SFCS.1977.32

62.

Reger G, Cruz HC, Rydeheard DE (2015) MarQ: monitoring at runtime with QEA. In: Baier C, Tinelli C (eds) TACAS 2015, LNCS, vol 9035. Springer, pp 596–610

63.

Roudjane M, Rebaine D, Khoury R et al (2019) Predictive analytics for event stream processing. In: 23rd IEEE international enterprise distributed object computing conference, EDOC 2019, Paris, France, October 28-31, 2019. IEEE, pp 171–182. https://doi.org/10.1109/EDOC.2019.00029

64.

Schneider FB (2000) Enforceable security policies. ACM Trans Inf Syst Secur 3(1):30–50CrossRef

65.

Selyunin K, Jaksic S, Nguyen T et al (2017) Runtime monitoring with recovery of the sent communication protocol. In: Majumdar R, Kunčak V (eds) Computer aided verification. Springer International Publishing, Cham, pp 336–355

66.

Taleb R, Hallé S, Khoury R (2021a) A modular runtime enforcement model using multi-traces. In: Aïmeur E, Laurent M, Yaich R et al (eds) Foundations and practice of security - 14th international symposium, FPS 2021, Paris, France, December 7-10, 2021, Revised Selected Papers, Lecture Notes in Computer Science, vol 13291. Springer, pp 283–302. https://doi.org/10.1007/978-3-031-08147-7_19

67.

Taleb R, Khoury R, Hallé S et al (2021b) Runtime verification under access restrictions. In: Bliudze S, Gnesi S, Plat N (eds) FormaliSE@ICSE 2021. IEEE, pp 31–41. https://doi.org/10.1109/FormaliSE52586.2021

68.

Taleb R, Hallé S, Khoury R (2022) Benchmark measuring the overhead of runtime enforcement using multi-traces (LabPal package). https://doi.org/10.5281/zenodo.5976001

69.

Talhi C, Tawbi N, Debbabi M (2006) Execution monitoring enforcement for limited-memory systems. In: PST, PST ’06. Association for Computing Machinery, New York

70.

Varvaressos S, Lavoie K, Gaboury S et al (2017) Automated bug finding in video games: a case study for runtime monitoring. Comput Entertain 15(1):1:1–1:28. https://doi.org/10.1145/2700529CrossRef

71.

Vella M, Colombo C, Abela R et al (2021) RV-TEE: secure cryptographic protocol execution based on runtime verification. J Comput Virol Hacking Tech 17:229–248CrossRef

72.

Yu F, Bultan T, Ibarra OH (2011) Relational string verification using multi-track automata. Int J Found Comput Sci 22(8):1909–1924. https://doi.org/10.1142/S0129054111009112MathSciNetCrossRefMATH

Title: A modular pipeline for enforcement of security properties at runtime
Authors: Rania Taleb
Sylvain Hallé
Raphaël Khoury
Publication date: 17-04-2023
Publisher: Springer International Publishing
Published in: Annals of Telecommunications / Issue 7-8/2023
Print ISSN: 0003-4347
Electronic ISSN: 1958-9395
DOI: https://doi.org/10.1007/s12243-023-00952-z

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Other articles of this Issue 7-8/2023

Secure and low PAPR OFDM system using TCCM

Attribute-based encryption of LSSS access structure with expressive dynamic attributes based on consortium blockchain

Foreword of the special issue on « FPS 2021» symposium

HistoTrust: tracing AI behavior with secure hardware and blockchain technology

Adaptive password guessing: learning language, nationality and dataset source

A modified ZF algorithm for signal detection in an underwater MIMO STBC-OFDM acoustic communication system