Runtime Verification
Robustness and reliability are key factors in the success of the deployment of security-critical systems. Testing, fails to address these concerns adequately since not all possible execution paths are covered. On the other hand, verification - the analysis of all execution paths - is usually unfeasible due to the large state space of such systems. Runtime-verification addresses the issue by enabling formal verification of the system during its execution. An adequate logic and language to express typical security properties is a prerequisite to enable runtime verification.

LarvaSTAT
LarvaStat is an extension to the LARVA runtime verification tool and logic with statistical capabilities. The logic is concise and intuitive, yet sufficiently expressive to express a wide variety of statistics including those with real-time aspects. Examples of typical statistics which one can gather with LarvaSTAT are "How many logins occurred in the last 24 hours", "How many downloads took place from login till logout", "How many mouse clicks take place on average during the first minute of visiting a webpage".

Overview:
LARVA is a compiler which given a script file in LARVA, will generate the appropriate monitoring JAVA code. For this code to be integrated into the target system, one should copy the generated files into a folder named "larva" (the name of the package) together with the other packages of the system. Once the system is recompiled with the AspectJ compiler, it will become a runtime-verified system.

Downloads:
If you would like a copy of the tool, please fill in the following form, and we will send you the tool directly via email. Should you have any problems with the form, or fail to receive a response in a reasonable amount of time, please let us know via email.