Larva Featured on InfoQ

Video Introducing Runtime Verification

Handling Runtime Monitoring Overhead - Christian Colombo from CESCA on Vimeo.

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.

LARVA
LARVA is a runtime verification platform for runtime verification of critical systems. A language was specifically designed to allow a user to specify the security properties of a JAVA software system. Once these are specified in a text file, the compiler generates the necessary code in JAVA and AspectJ which verifies that the properties in the script are being adhered to during the execution of the system. The advantage of taking this approach is that the monitoring is done without changing any code in the system being monitored.

Centralisation:

Security properties can be specified separately in one central location and outside of the system code with the possibility of easily turning on or off this extra checking.

Different uses:

LARVA use can either be limited during the testing phase or else it can be used also after deployment. The latter has the advantage of reassuring that under no circumstance will any of the security properties be violated. However, this also has the disadvantage of adding extra overhead to the system.

Simplicity:

Another appealing feature of the language is that it was kept as simple as possible to make it as easy as possible to use. In fact the logic of the language is equivalent to a state-machine with local variables and some other features.

Visualisation:

The compiler uses a graphics program to generate the state-machine equivalent of the logic in the script. Therefore, the user has the advantage of visualizing the logic written.

Real-Time:

The LARVA language allows the user to use real-time clocks in the specification. These can be used to trigger events and measure the time elapsed between events. This can be very useful to describe numerous interesting properties. For example no more than 3 bad logins should be allowed with 10 minutes.

Future Directions
In the near future we intend to analyse the extent of the overhead created upon the system being monitored. One approach to this issue is to give guarantees as the upperbound of the overhead. Alternatively, we can run the monitoring system on a separate machine so that the monitored system will not be affected. However, this approach will raise synchronisation issues because the monitoring system may not be able to keep up with the monitored system.

Introduction to Aspect-Oriented Programming as a Tool for Runtime Verification:

In [1], we have given some examples to illustrate the appropriateness of using aspect-oriented programming. The most appealing contribution of aspect-oriented programming is the fact the monitoring code is automatically injected in the code without the need of manual intervention.

Literature Review of Runtime Verification and Proposed Work:

In [2], we have gone through major works in the area of runtime verification, highlighting examples and technologies which will be useful for our proposed work. The paper ends with a concrete proposal for creating a runtime verification tool (LARVA) and employing it in an appropriate case-study.

Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties:

In [3], we give the mathematical background of the runtime verification system LARVA. In addition, we give account of a case-study carried out on a transaction system. Finally, LARVA is compared to other prominent tools in the area of runtime verification through a benchmark.

Larva is now available through a repository which includes the code, sample systems and scripts, user manual, and a tutorial.
PS: Note that the latest version of the Larva compiler doesn't run on Windows. Will fix this asap.

Get your hands dirty by trying out a simple tutorial.

Using the plugin the Larva compiler will be automatically invoked each time you save your Larva script. Each invocation automatically generates monitors in the same folder as the script. Check the first line of the script for error messages/warnings (due to which files might not be generated).

Install the Larva Eclipse plugin from this update site. This update site also includes the necessary packages from XText on which the plugin is based but requires you to have AJDT plugin installed for the plugin output to be executable.

Alternatively here is an Eclipse download (dropbox) for 64-bit OSX Yosemite with the plugin pre-installed (having AspectJ plugin (AJDT) also installed).

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.

Requirements:
The user requires the JAVA Runtime Environment to be installed on the computer system and the AspectJ software. It is assumed that the system PATH includes the directory of the Java and AspectJ installations. Furthermore, if the user want to generate the diagram equivalent of the automata, he must have Graphviz software installed.

How to compile:
Simply use the batch file provided and it will guide you to enter the necessary parameters.

Input syntax:
For a complete reference manual as regards the LARVA language see the LARVA User Manual. Also, we provide a number of translations from well-known logics including duration calculus, QDDC, and Lustre. The links for the converter are available below.

Downloads:
If you would like a copy of the tool, please visit the repository. Should you have any problems, please let us know via email, or by submitting the following form.

• LARVA GUI (version 0.2): The current version of LARVA GUI