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.
larvaBIG/asyncLarva
Larva monitoring relies heavily on main memory. For large systems Larva is a non-starter.
For industrial systems we have larvaBIG which extracts system events using aspect-oriented programming as in Larva but stores monitors in database tables. Its sister tool is asyncLarva which interfaces with a log database to obtain system events rather than aspect-oriented programming. AsyncLarva is thus particularly useful for non-intrusive monitoring.
|