Ontological Hazard Analysis

Ontological Hazard Analysis is a method for eliciting safety or security requirements by using Formal Refinement to achieve a very high level of confidence, starting with an extremely simple high-level abstraction, and subsequently refining it to a concrete level, where it can be implemented or directly compared to an existing implementation.

The key notions in OHA are abstraction and refinement. One starts by formulating a very abstract specification of the system and identifying the security requirements by enumeration and selection. One then refines (introduces more detail into) this abstract specification in a number of steps, identifying further hazards and accumulating security requirements, until one has reached a specification which directly corresponds to an actual system.

Such a development traces security requirements through system design, in principle down to object code, giving confidence to developer and client that developmental security goals have been achieved.

The full potential of using it down to object code can only be achieved when using critical-systems programming languages and development systems, such as SPARK or SCADE, to create a new implementation. Methods of reverse-engineering or examining existing systems cannot achieve as high a confidence level as using formal methods to create and verify a new implementation.