PollyRV

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. This technique naturally involves interaction with the original system, invariably modifying the system to some extent.

Emerging industrial settings, such as online portals, present new challenges to the field of runtime verification as they frequently involve high volume throughput and concoctions of technologies. Most runtime verification techniques do not maintain a well defined system-monitor boundary, leading to monitors being tightly coupled to the underlying systems. This generally means that the monitor is considerably intrusive and technology dependent. The second generation of the Larva runtime verification tool PollyRV, strives towards a clear-cut system-monitor boundary which enables the monitor to be technology agnostic, possibly interfacing with various technologies at a time.

PollyRV
PollyRV is a parametrised event-based runtime-verification tool supporting monitoring of real-time specifications. In addition, the PollyRV runtime monitoring framework :

(i) is system side language agnostic

(ii) provides a configurable system-monitor boundary using explicit tagging of monitoring code locality (system or monitor)

(i) a 'frontend'

handling the event extraction instrumentation and the system interaction aspect

(ii) a verification 'back-end'

enabling greater flexibility to support different languages, for which only the language-specific front-end needs to be developed

Overview:
In order for the PollyRV framework to be adopted, a system which is to be monitored and a high-level specification of the properties that must be obeyed by this system are expected to be provided as input. A PollyRV runtime monitoring framework is generated in a two-step sequence. In the first step the PollyRV monitor is created, as a JAVA program, from the high-level specification. The second step then handles the generation of aspect code which is to be weaved into the target system. This code must be generated in the target system language and therefore requires a PollyRV language specific compiler to generate it.

Using PollyRV:

The PollyRV Compiler

Requirements: a JDK installation. The system path should be updated to recognize the commands java and javac.

(i) Generating the PollyRV Monitor

Run the batch file generate_monitor available with the PollyRV release

(ii) Running the PollyRV Monitor

Run the batch file run_monitor available with the PollyRV release

(i) To generate instrumentation code and run the system

use the batch file generateandrun_javasys available with the PollyRV release