Formalized Analysis and Verification

Meta-Information

Origin: Colin Snook / University of Southampton

Written: October 2018

Purpose: Verify that the design of a system or procedure involving dependability (e.g. security) is indeed dependable (e.g. secure), or analyze any flaws that are found to determine the scenarios that lead to the dependability requirement being violated.

Context/Pre-Conditions:

– The required property must be clearly understood so that it can be formally modelled.

– The design of the system or procedure must be precisely described so that it can be formally modelled.

To consider:

– Requires high level of expertise in formal modelling involving abstraction/refinement.

– Requires the ability to understand and reason about models using set-theory and predicate logic.

– Requires experience of using model checker and theorem prover tools.

.

Structure

(1) Modelling of Dependability Property:

(2) Modelling of Dependability Mechanisms:

(3) Analysis of Dependability Mechanisms:

(3.2) Check whether Dependability is Violated:

Participants and Important Artefacts

V&V Engineer: The person responsible for executing this workflow, and in particular creating/refining the models, formulating properties, interpreting verification tool results etc.

Domain Expert: Person responsible for checking that the models behaviour (as demonstrated by validation tools) reflects the desired system or procedure.

Theorem Provers: Tool that takes a model and a property, generates proof obligations and checks whether it can find a logical proof that the goal of proof obligation is true.

Model-checker: Tool that takes a model and a property, and checks whether it can verify the model or find a trace that violates the property. Such a trace is called “counter example”.

Counter Example: A trace of the model generated by the model-checker exemplifying how the model may violate a given property.

Dependability property model: An abstract behavioral model of the desired (e.g. security) property, keeping essential properties of the domain only.

Dependability mechanism model: A behavioral model that refines the (e.g. security) property model and describes the design (i.e. mechanism) of the system or procedure, keeping essential properties of the design only.

Actions and collaborations

(1) An abstract model is constructed in just enough detail to express the desired dependability property.

(2) A refined model is constructed to describe how the system achieves the desired property. (This is normally done over several refinement iterations depending on the complexity of the system).

(2.a) The model is proven to be a correct refinement of the abstract model or previous refinement. If all proof obligations are discharged the specified system achieves the desired dependability property and step 3 is not required. If some proof obligations cannot be proved they are analysed as described in step 3.

(2.b) The model is animated to validate that it represents the real system.

(3) If some proof obligations could not be proved they are analysed as follows:

(3.a) The model checker provides a counter example demonstrating where the gluing invariant is violated (the gluing invariant is a relationship between the abstract and concrete models that describes why the dependability mechanism achieves the desired dependability property).

(3.b) The concrete model is then ‘detached’ from the refinement chain (the gluing invariant is removed) and the dependability property is entered directly in the concrete model.

(3.c) The model checker is run again to find a counter example that breaks the dependability property:

(3.c.a) If none is found, the gluing invariant may be too strong.

(3.c.b) If one is found it illustrates a complete trace showing a scenario that illustrates how a flaw in the dependability mechanism leads to a breach of the dependability property.

Discussion

Choice of Language and Tools: In principle, this pattern is independent of modelling language and tools. However, the pattern was developed using the Rodin platform for Event-B including plug-ins for UML-B diagrammatic modelling and ProB model checker and it may be difficult to find an alternative tool-set that offers a similar range of facilities. The language used should support abstraction with statically verifiable refinement, entity relationship modelling and state-transition behaviour. The language should be supported by strong V&V tools including both theorem provers (to prove properties irrespective of instantiation) and model-checkers (to find counter examples and provide animation).

Further Details: A detailed description and example is available in:

Snook C., Hoang T.S., Butler M. (2017) Analysing Security Protocols Using Refinement in iUML-B. In: Barrett C., Davies M., Kahsai T. (eds) NASA Formal Methods. NFM 2017. Lecture Notes in Computer Science, vol 10227. Springer, Cham

Application Examples

VLAN double tagging attack.: The pattern is described using this example. (The formal model is available here: https://eprints.soton.ac.uk/403533/).

ENABLE-S3 Use Case 7 “Touch and Go Assistant”: The pattern is used for analysing security of authentication process between aircraft and ground cart service equipment. (TBD).

ENABLE-S3 Use Case 9 “Interlocking”: The pattern has been used to analyse a railway interlocking control system component.

Relations to other Patterns

Pattern Name	Relation
Runtime Monitoring	Both patterns use formalized requirement presentation (called „dependability property“ here)
KPI Model-based Validation	Both patterns are alternative approaches
Requirements Formalization	Both patterns use similar approaches