Dynamic automata in Larva

Abstract

As computer systems become larger and more sophisticated, they bring about an increased level of possible execution

paths and environment configurations, which, generally, cannot be reliably catered for by testing due to its inherent lack

of coverage. As such, many developers are turning onto runtime software verification to be able to provide higher system

quality assurance, intercepting undiscovered bugs as they arise. However, sophisticated systems tend to involve large

specification properties and thus pose a considerable overhead when the states of such properties are fully enumerated

to perform runtime verification. The problem is even more intricate with infinite-state properties where enumeration is not possible. A solution to this issue is through the use of on-the-fly state generation techniques where the next state is dynamically computed at runtime. In this paper, we present dLarva — an extension of the Larva runtime verification tool supporting on-the-fly state-generating automata. This enables the definition of automata in a symbolic manner

while also making it possible to traverse infinite state properties. To demonstrate the possibilities of dLarva, we provide

an implementation of dLarva that accepts properties using

regular expressions which are dynamically evaluated at runtime using derivatives. This implementation is used as the

basis for a simple rule-based intrusion detection system for the AnomicFTPD FTP server.