On the complexity of monitoring Orchids signatures, and recurrence equations | Formal Methods in System Design Skip to main content
Log in

On the complexity of monitoring Orchids signatures, and recurrence equations

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Modern monitoring tools such as our intrusion detection tool Orchids work by firing new monitor instances dynamically. Given an Orchids signature (a.k.a. a rule, a specification), what is the complexity of checking that specification, that signature? In other words, let f(n) be the maximum number of monitor instances that can be fired on a sequence of n events: we design an algorithm that decides whether f(n) is asymptotically exponential or polynomial, and in the latter case returns an exponent d such that \(f(n) = \varTheta (n^d)\). Ultimately, the problem reduces to the following mathematical question, which may have other uses in other domains: given a system of recurrence equations described using the operators \(+\) and \(\max \), and defining integer sequences \(u_n\), what is the asymptotic behavior of \(u_n\) as n tends to infinity? We show that, under simple assumptions, \(u_n\) is either exponential or polynomial, and that this can be decided, and the exponent computed, using a simple modification of Tarjan’s strongly connected components algorithm, in linear time.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5

Similar content being viewed by others

Notes

  1. To dispel a possible misunderstanding, these threads are not system-level threads, rather pairs of a pending transition and an environment holding the values of variables, and which are handled and scheduled by the Orchids engine. Similarly, “forking” an Orchids thread simply means making a copy of the current thread and adding it to the Orchids thread queue.

  2. Variables are thread-local: if an Orchids thread modifies one of its variables, this does not affect any other thread.

References

  1. Akian M, Bapat R, Gaubert S (2006) Max-plus algebras. In: Hogben L (ed) Handbook of linear algebra, discrete mathematics and its applications, vol 39, chap 25. Chapman and Hall/CRC, Boca Raton

    Google Scholar 

  2. Albert E, Arenas P, Genaim S, Puebla G (2011) Closed-form upper bounds in static cost analysis. J Autom Reason 46(2):161–203

    Article  MathSciNet  MATH  Google Scholar 

  3. Assaf M (2015) From qualitative to quantitative program analysis: permissive enforcement of secure information flow. PhD thesis, Université Rennes I

  4. Basin D, Klaedtke F, Müller S, Zălinescu E (2015) Monitoring metric first-order temporal properties. J Assoc Comput Mach 62(2):15:1–15:45

    Article  MathSciNet  MATH  Google Scholar 

  5. Brockschmidt M, Emmes F, Falke S, Fuhs C, Giesl J (2014) Alternating runtime and size complexity analysis of integer programs. In: Proceedings of international conference of tools and algorithms for the construction and analysis of systems (TACAS’14). Lecture notes in computer science, vol 8413. Springer

  6. Flajolet P, Sedgwick R (2009) Analytic combinatorics. Cambridge University Press, iSBN 0521898064. ISBN-13 978-0521898065

  7. Flores-Montoya A, Hähnle R (2014) Resource analysis of complex programs with cost equations. In: Proceedings of 12th Asian symposium on programming languages and systems (APLAS’14). Lecture notes in computer science, vol 8858. Springer, Singapore, Singapore

  8. Goubault-Larrecq J, Olivain J (2008) A smell of Orchids. In: Leucker M (ed) Proceedings of the 8th workshop on runtime verification (RV’08). Lecture notes in computer science, vol 5289, pp 1–20. Springer, Budapest, Hungary. https://doi.org/10.1007/978-3-540-89247-2_1

  9. Goubault-Larrecq J, Olivain J (2013) On the efficiency of mathematics in intrusion detection: the NetEntropy case. In: Danger JL, Debbabi M, Marion JY, Garcia-Alfaro J, Zincir-Heywood N (eds) Revised selected papers of the 6th international symposium on foundations and practice of security (FPS’13). Lecture notes in computer science, vol 8352. Springer, La Rochelle, France, pp 3–16. https://doi.org/10.1007/978-3-319-05302-8_1

  10. Havelund K, Reger G (2015) Specification of parametric monitors—quantified event automata versus rule systems. In: Drechsler R, Kuhne U (eds) Formal modeling and verification of cyber-physical systems. Springer, pp 151–189, 1st international summer school on methods and tools for the design of digital systems (SyDe). Springer, Bremen, Germany, pp 151–189

  11. Jin D, O’Neil Meredith P, Lee C, Roşu G (2012) JavaMOP: efficient parametric runtime monitoring framework. In: Proceeding of the 34th international conference on software engineering (ICSE’12), IEEE, pp 1427–1430. https://doi.org/10.1109/ICSE.2012.6227231

  12. Luo Q, Zhang Y, Lee C, Jin D, O’Neil Meredith P, Şerbănuţă TF, Roşu G (2014) RV-monitor: efficient parametric runtime verification with simultaneous properties. In: Bonakdarpour B, Smolka SA (eds) Proceedings of the 5th international conference on runtime verification (RV’14), LNCS, vol 8734. Springer, Toronto, ON, CA, pp 285–300

  13. Olivain J, Goubault-Larrecq J (2005) The Orchids intrusion detection tool. In: Etessami K, Rajamani S (eds) Proceedings of the 17th international conference on computer aided verification (CAV’05). Lecture notes in computer science, vol 3576. Springer, Edinburgh, Scotland, UK, pp 286–290. https://doi.org/10.1007/11513988_28

  14. Purczyński W (2003) Linux kernel privileged process hijacking vulnerability. http://www.securityfocus.com/bid/7112, bugTraq Id 7112. Last read: september, 2003

  15. Roger M, Goubault-Larrecq J (1999) Procédé et dispositif de résolution de modèles, utilisation pour la détection des attaques contre les systèmes informatiques. Dépôt français du 13 sep. 1999, correspondant Dyade, demandeurs : 1. INRIA 2. Bull S.A. Numéro de publication: 2 798 490. Numéro d’enregistrement national: 99 11716. Classification: G 06 F 19/00. Date de mise à la disposition du public de la demande: 16 mars 2001, bulletin 01/11

  16. Roger M, Goubault-Larrecq J (2001) Log auditing through model checking. In: Proceedings of the 14th IEEE computer security foundations workshop (CSFW’01). IEEE Computer Society Press, Cape Breton, Nova Scotia, Canada, pp 220–236

  17. Tarjan RE (1972) Depth-first search and linear graph algorithms. SIAM J Comput 1(2):146–160

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

The first author would like to thank Mounir Assaf for drawing his attention to analytic combinatorics, and the anonymous referees for their suggestions.

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Jean Goubault-Larrecq.

Additional information

Partially funded by INRIA-DGA Grant 12 81 0312 (2013-2016). The second author also thanks Hydro-Québec and Les Offices jeunesse internationaux du Québec (LOJIQ) for their financial support.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Goubault-Larrecq, J., Lachance, JP. On the complexity of monitoring Orchids signatures, and recurrence equations. Form Methods Syst Des 53, 6–32 (2018). https://doi.org/10.1007/s10703-017-0303-x

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-017-0303-x

Keywords

Mathematics Subject Classification

Navigation