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.
Similar content being viewed by others
Notes
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.
Variables are thread-local: if an Orchids thread modifies one of its variables, this does not affect any other thread.
References
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
Albert E, Arenas P, Genaim S, Puebla G (2011) Closed-form upper bounds in static cost analysis. J Autom Reason 46(2):161–203
Assaf M (2015) From qualitative to quantitative program analysis: permissive enforcement of secure information flow. PhD thesis, Université Rennes I
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
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
Flajolet P, Sedgwick R (2009) Analytic combinatorics. Cambridge University Press, iSBN 0521898064. ISBN-13 978-0521898065
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
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
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
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
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
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
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
Purczyński W (2003) Linux kernel privileged process hijacking vulnerability. http://www.securityfocus.com/bid/7112, bugTraq Id 7112. Last read: september, 2003
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
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
Tarjan RE (1972) Depth-first search and linear graph algorithms. SIAM J Comput 1(2):146–160
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
Corresponding author
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
About this article
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
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-017-0303-x