LARVA logo

Logical Automata for Runtime Verification and Analysis


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.

<< Semantics & Verification Research Group Home
LARVA Papers
[1] Dynamic Analysis Overview and a Proposed Verification Tool for Temporal Properties in Security-Critical Software, Christian Colombo, in MSc Seminar, Malta 2008. (PDF)
[2] Aspect-Oriented Programming Runtime-Enforcement of Temporal Properties in Security-Critical Software , Christian Colombo, and Gordon J. Pace, in CSAW'2007, Malta. (PDF)
[3] Dynamic Event-Based Runtime Monitoring of Real-Time and Contextual Properties, Christian Colombo, Gordon J. Pace and Gerardo Schneider, in FMICS 2008, Italy. (PDF) (BiBTeX entry)
[4] A Practical Approach to Runtime Verification of Real-Time Properties for Java Programs, Christian Colombo, Gordon J. Pace and Gerardo Schneider, in WICT 2008, Malta. (PDF)
[5] Practical Runtime Monitoring with Impact Guarantees of Java Programs with Real-Time Constraints, Christian Colombo, in MSc Thesis 2008, University of Malta. (PDF)
[6] Safe Runtime Verification of Real-Time Properties, Christian Colombo, Gordon J. Pace and Gerardo Schneider, in FORMATS 2009, Budapest, Hungary. (PDF) (BiBTeX entry)
[7] LARVA - Safer Monitoring of Real-Time Java Programs, Christian Colombo, Gordon J. Pace and Gerardo Schneider, in SEFM 2009, Hanoi, Vietnam. (PDF) (BiBTeX entry)
[8] Resource-Bounded Runtime Verification of Java Programs with Real-Time Properties, Christian Colombo, Gordon J. Pace and Gerardo Schneider, Department of Computer Science, University of Malta. Technical Report CS2009-01, 2009. (PDF) (BiBTeX entry)
[9] Offline Runtime Verification with Real-Time Properties: A Case Study, Christian Colombo, Gordon J. Pace and Patrick Abela, internal report 01-WICT-2009, Malta. (PDF)
[10] Statistics and Runtime Verification, Andrew Gauci, Gordon J. Pace and Christian Colombo, internal report 02-WICT-2009, Malta. (PDF)
[11] LarvaStat: Monitoring of Statistical Properties, Christian Colombo, Andrew Gauci and Gordon J. Pace, in RV, Malta, 2010. (PDF)
[12] Compensation-Aware Runtime Monitoring, Christian Colombo, Gordon J. Pace and Patrick Abela, in RV 2010, Malta. (PDF)
[13] Runtime Verification using Larva, Christian Colombo and Gordon J. Pace, in RV-CuBES, Seattle, USA, 2017. (PDF)

NEW! (October 2017): Larva public repository

Larva is now available through a repository which includes the code, sample systems and scripts, user manual, and a tutorial.


Larva Tutorial

Get your hands dirty by trying out a simple tutorial.


Eclipse plugin

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).


The Toolkit

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.


Name:
Institution:
Address:
Email:
Help us fight spam:

Comments/Questions/Problems:




There is also a very basic standalone UI for Larva written in Java. Available for whom it might be useful:
  • LARVA GUI (version 0.2): The current version of LARVA GUI
This is a short video tutorial on using Larva (sorry the audio is poor and not in sync with the visual)


Contact details
Gordon J. Pace
Department of Computer Science,
Faculty of ICT,
University of Malta,
Msida MSD2080,
MALTA

Tel: (+356) 2340 2504
Fax: (+356) 2132 0539
E-mail: Gordon.Pace@um.edu.mt
Christian Colombo
Department of Computer Science,
Faculty of ICT,
University of Malta,
Msida MSD2080,
MALTA

Tel: (+356) 2340 2640
E-mail: christian.colombo@um.edu.mt