A Review of Dynamic Verification of Security and Dependability Properties

A Review of Dynamic Verification of Security and Dependability Properties

Antonio Muñoz, Jamal Toutouh, Francisco Jaime
Copyright: © 2019 |Pages: 26
DOI: 10.4018/978-1-5225-7353-1.ch007
OnDemand:
(Individual Chapters)
Available
$37.50
Current Special Offers
No Current Special Offers
TOTAL SAVINGS: $37.50

Abstract

This chapter reviews the notions of security and dependability properties from the perspective of software engineering, providing the reader with a technical background on dynamic verification and runtime monitoring techniques. The chapter covers the technical background on security and dependability properties with system verification through dynamic verification or monitoring. The authors initially provide a short overview of the security and dependability properties themselves. Once definitions of security and dependability properties are introduced, they present a critical analysis of current research on dynamic verification by presenting general purpose and security oriented dynamic verification approaches.
Chapter Preview
Top

Dynamic Verification Of Security Properties

In first place, a review of security properties is given, and then the most relevant dynamic verification mechanisms are described. We distinguish between languages for expressing security properties for dynamic verification and languages for expressing all types of properties for dynamic verification.

Most of the approaches deploy languages based on some sort of temporal logic, as these languages provide the necessary operators for expressing conditions about the temporal ordering and boundaries of occurrence of events, which is required for the expression of most of the properties that need to be verified at runtime. The most popular formal notation for expressing security properties is Linear Temporal Logic (LTL), or extensions of it, and languages with similar expressive power such as Event Calculus.

Some dynamic verification techniques reason about systems at both, low and high level of abstraction, such as Primitive Event Definition Language (PEDL) and Meta Event Definition Language (MEDL) in Java Monitoring and Checking (JavaMaC) framework (Lee, 1999). PEDL is used for writing low-level specifications and is tightly related to the programming language, while MEDL specification makes use of primitive events and conditions in order to state high-level requirements.

Complete Chapter List

Search this Book:
Reset