Dynamic automata in LARVA

Abstract

Computer systems are today, more than ever, present in our daily lives. They are increasingly becoming larger, and more sophisticated, thus bringing about an increased level of possible execution paths and environment configurations, which ultimately makes them more error prone. On the other hand, people continue to expect these softwares to guarantee their reliability and availability at all times. As such, it is becoming evident that testing alone can not provide the required guarantees, and therefore many developers are turning onto dynamic software verification to be able to provide a higher quality assurance. In this document, we present dLarva, which is an extension of the runtime verification tool LARVA. ..While LARVA already supports dynamic automaton creation, thanks to its underlying DATE (Dynamic Automata with Timers and Events) architecture, dLarva introduces support for on-the-fly state generating automata. This will make it possible to use runtime verification with an infinite state property (automaton) which brings about numerous advantages such as always having a concise representation of the property and its state at hand. Moreover, we posit that in certain cases, it could be easier to specify a dynamic automaton by specifying its transition function rather than specifying an equivalent static automaton which would need to be statically derived from its (possibly natural) dynamic definition. To demonstrate the possibilities of dLarva, we provide an implementation of LARVA/dLarva that accepts properties using a rather simple regular expression which are evaluated at run-time using derivatives. Then, we provide a simple case scenario where regular expressions are used to implement a rule-based intrusion detection system for the AnomicFTPD FTP server.