US 12,748,679 B2 · System and methods for end-to-end provable guarantees for safety critical computer platforms

Abstract

A system and methods are disclosed for end-to-end provable guarantees for safety critical computer platforms. The technical problem addressed by this invention is the need to provide assurance that a complex safety-critical computer platform behaves as intended and is secure, particularly in safety-critical contexts where errors or malicious attacks can have devastating effects. Despite advances in methodologies and toolchains for high-assurance software production, there remains a significant gap between theoretical guarantees and practical implementation at the operation instruction level (e.g., Assembly language instruction, byte-code instruction, digital circuit state-machine instruction etc.). The present invention overcomes this limitation by providing a system for verifying key security properties for safety-critical computer platforms at the operation instruction level without reliance on custom generation pipelines or certified compilers, thereby enabling the practical development of more secure and reliable computer platforms.

Claims28

Dependent claims

A system for verifying a computer platform via verification of a set of program execution elements (PEEs), the computer platform comprising the set of PEEs, the system comprising:

at least one processor;
and
a non-transitory computer-readable storage medium having stored thereon code executable by the at least one processor, the code comprising
a set of compilers for compiling the set of PEEs into operational instructions that accomplish operational semantics of each PEE;
a PEE lifting mechanism to lift the operational instructions into an idiomatic code representation (ICR);
and
a PEE verification mechanism that enforces a compartmentalization security mechanism (CSM) that preserves properties verified at a respective source level of each respective PEE in the set of PEEs down to the operational instructions of the respective PEE generated by the set of compilers,
wherein
a first PEE in the set of PEEs comprise one or more PEE functions as units of execution, and
the PEE verification mechanism further checks properties of the one or more PEE functions and corresponding ICR that guarantee one or more of the group consisting of a behavior property, a security property and timing property.

7 more elements

Dependencies are inferred from the claim text.

System and methods for end-to-end provable guarantees for safety critical computer platforms

Life of this patent

System and methods for end-to-end provable guarantees for safety critical computer platforms

Life of this patent

Abstract

Claims28