Formally Verified Hardware Encapsulation Mechanism for Security, Integrity, and Safety.

摘要

Safety- and security-critical systems both require encapsulation of code and data belonging to different applications and sensitivity levels. It must be impossible for a fault or Trojan Horse in one application to affect the operation or real-time performance of another, or for information of one sensitivity level to contaminate that of another. Encapsulation is achieved by the combination of software in an operating system kernel managing hardware protection mechanisms. The critical nature of the applications concerned means that extremely high assurance is required for the correctness of the encapsulation mechanisms. A systematic approach is developed for the formal specification and verification of these encapsulation properties and mechanisms, addressing the interaction between a processor, custom protection hardware, and the kernel software managing them; it encompasses both safety and security concerns and may be adjusted for different classes of systems. It is validated by mechanically checked verification. This validation provides a formal guarantee -- from kernel interface down through hardware -- of both spatial (memory) and temporal (time-slicing) encapsulation for the processor.