Patent ID: 8341602

Claim:
A method for verification of a safe operating system that correctly supplies “well-formed” stacks and objects, comprising steps for: providing annotated source code comprising a nucleus of an operating system, wherein the nucleus provides hardware and memory access for the operating system, and wherein the annotations correspond to allowed behaviors for each instruction of the source code of the nucleus; evaluating the allowed behaviors of the annotated source code using a verification tool to ensure that the allowed behaviors are consistent with the corresponding instructions; wherein source code having consistent allowed behaviors is compiled to produce an operating system nucleus supplying “well-formed” stacks and objects; providing source code for one or more higher level program elements intended to be run on top of the operating system nucleus; verifying that the source code of the higher level program elements safely interacts with the “well-formed” stacks and objects of the compiled operating system nucleus; compiling verified source code of the higher level program elements; and combining the operating system nucleus with the compiled source code of the higher level program elements to construct a verifiably safe operating system.