Systems and methods for formal verification of computer platforms
Systems and methods for mathematical modeling of the hardware and software stack of commodity computer platforms are provided, enabling provable guarantees on memory, device, and program execution. This approach addresses the technical problem of reliance on system agents that rely on implicit trust in the operating environment, which can be exploited by sophisticated attackers using complex threats such as memory access exploits and code/data integrity exploits. The solution provides a proactive, mathematically-backed security solution that eliminates entire classes of cyberattacks by design, ensuring realizable guarantees on commodity computer platforms running hardware and software stack elements at the lowest operating level. This approach has significant advantages over current reactive cybersecurity methods, including reduced complexity and overhead, and increased confidence in the integrity of the system. The solution's main uses include providing mathematically-backed security and availability guarantees for critical infrastructure, financial institutions, and other organizations vulnerable to cyberattacks.
1. A system for providing formal verification of a design and operation of a computer platform, the system comprising:
at least one processor; and
at least one computer-readable storage medium having stored thereon instructions which, when executed, program the at least one processor to perform act(s) of:
evaluating a mathematical model that defines interfaces to hardware elements and software stack elements of the computer platform, encodes operational aspects of the hardware elements and software stack elements using the interfaces, and specifies invariants with assume-guarantee interface-confined mathematical reasoning,
wherein the evaluating determines whether the invariants hold throughout the lifetime of the computer platform
wherein
the hardware elements and software stack elements of the computer platform comprise memory, peripherals, computing processors and program execution elements;
the interfaces include a direct memory access (DMA) interface;
the mathematical model specifies at least one peripheral among the peripherals that accesses the memory via the DMA interface;
the DMA interface is governed by one or more DMA access control tables and/or channels which specify access control permissions of said peripheral to access specified regions of the memory;
the one or more DMA access control tables and/or channels are implemented in hardware and programmable via software source or binary embedding within the program execution element; and
the DMA interface is modeled via mathematical process calculi logic allowing for multiple hardware elements to access the DMA interface concurrently in the computer platform.
2. The system of claim 1 , wherein the mathematical model is defined in one or more mathematical logic languages.
3. The system of claim 1 , wherein a peripheral among the peripherals is a validated computer platform.
4. The system of claim 1 , wherein
the computer platform is a first computer platform and the mathematical model is a first mathematical model,
the at least one computer-readable storage medium further has stored thereon instructions which, when executed, program the at least one processor to perform additional acts of
evaluating a second mathematical model for a second computer platform; and
if the invariants hold for both the first and second computer platform, determining that a combined computer platform, consisting of both the first and second computer platform, is validated.
5. The system of claim 1 , wherein at least one of the invariants is a security property.
6. The system of claim 5 , wherein the security property is selected from the group consisting of control-flow integrity, memory safety, memory-integrity, privilege separation, and approved execution, and authorized data encryption and decryption.
7. The system of claim 1 , wherein the invariants specified by the mathematical model include at least one liveness property that is used to describe availability of a platform resource.
8. The system of claim 1 , wherein the invariants specified by the mathematical model are formulated using the interfaces.
9. The system of claim 1 , wherein determining from the mathematical model whether the invariants hold throughout the lifetime of the computer platform comprises analyzing the invariants to determine whether a model system property (MSP) is satisfied.
10. The system of claim 9 , wherein analyzing the invariants to determine whether the MSP is satisfied comprises encoding the invariants into a computer-assisted theorem proving system and using the computer-assisted theorem proving system to analyze the invariants to determine if the MSP is satisfied.
11. The system of claim 9 , wherein the at least one computer-readable storage medium further has stored thereon instructions which, when executed, program the at least one processor to perform additional act(s) of:
if the MSP is found not to be satisfied, generating a counterexample that shows that the MSP does not hold for an operational aspect among the operational aspects of the computer platform.
12. The system of claim 1 , wherein
the mathematical model further defines an operational state space for the computer platform; and
determining from the mathematical model whether the invariants hold throughout the lifetime of the computer platform comprises determining if a state in the operational state space can be reached from an initial state for all possible state transitions of the mathematical model.
13. A method for formal verification of a design and operation of a computer platform, the method comprising act(s) of:
defining interfaces to hardware elements and software stack elements of the computer platform in a mathematical model;
encoding operational aspects of the hardware elements and software stack elements using the interfaces in the mathematical model;
specifying invariants with assume-guarantee interface-confined mathematical reasoning in the mathematical model; and
evaluating the mathematical model to determine whether the invariants hold throughout the lifetime of the computer platform
wherein
the hardware elements and software stack elements of the computer platform comprise memory, peripherals, computing processors and program execution elements;
the interfaces include a direct memory access (DMA) interface;
the mathematical model specifies at least one peripheral among the peripherals that accesses the memory via the DMA interface;
the DMA interface is governed by one or more DMA access control tables and/or channels which specify access control permissions of said peripheral to access specified regions of the memory;
the one or more DMA access control tables and/or channels are implemented in hardware and programmable via software source or binary embedding within the program execution element; and
the DMA interface is modeled via mathematical process calculi logic allowing for multiple hardware elements to access the DMA interface concurrently in the computer platform.
14. The method of claim 13 , wherein the mathematical model is provided in one or more mathematical logic languages.
15. At least one computer-readable storage medium having stored thereon instructions which, when executed, program at least one processor to perform a method comprising acts of:
defining interfaces to hardware elements and software stack elements of a computer platform in a mathematical model;
encoding operational aspects of the hardware elements and software stack elements using the interfaces in the mathematical model;
specifying invariants with assume-guarantee interface-confined mathematical reasoning in the mathematical model; and
evaluating the mathematical model to determine whether the invariants hold throughout the lifetime of the computer platform
wherein
the hardware elements and software stack elements of the computer platform comprise memory, peripherals, computing processors and program execution elements;
the interfaces include a direct memory access (DMA) interface;
the mathematical model specifies at least one peripheral among the peripherals that accesses the memory via the DMA interface;
the DMA interface is governed by one or more DMA access control tables and/or channels which specify access control permissions of said peripheral to access specified regions of the memory;
the one or more DMA access control tables and/or channels are implemented in hardware and programmable via software source or binary embedding within the program execution element; and
the DMA interface is modeled via mathematical process calculi logic allowing for multiple hardware elements to access the DMA interface concurrently in the computer platform.
16. The least one computer-readable storage medium of claim 15 , wherein the mathematical model is provided in one or more mathematical logic languages.