Systems and methods for checking safety properties
In some embodiments, a system is provided, comprising enforcement hardware configured to execute, at run time, a state machine in parallel with application code. Executing the state machine may include maintaining metadata that corresponds to one or more state variables of the state machine; matching instructions in the application code to transitions in the state machine; and, in response to determining that an instruction in the application code does not match any transition from a current state of the state machine, causing an error handling routine to be executed. In some embodiments, a description of a state machine may be translated into at least one policy to be enforced at run time based on metadata labels associated with application code and/or data manipulated by the application code.
1. A system comprising enforcement hardware configured to:
execute, at run time, a state machine in parallel with application code, comprising:
maintaining metadata that corresponds to one or more state variables of the state machine;
matching instructions in the application code to transitions in the state machine; and
in response to determining that an instruction in the application code does not match any transition from a current state of the state machine, causing an error handling routine to be executed, wherein:
the enforcement hardware comprises policy enforcement hardware configured to check run time behavior of the application code against at least one policy; and
the at least one policy comprises rules corresponding to transitions in the state machine.
2. The system of claim 1 , wherein:
the state machine represents a safety property to be enforced while the application code is executed.
3. The system of claim 1 , wherein:
the instruction comprises a first instruction; and
executing the state machine in parallel with the application code further comprises:
in response to determining that a second instruction in the application code matches a transition from a current state of the state machine, performing a metadata update according to the matched transition.
4. The system of claim 1 , wherein causing an error handling routine to be executed comprises:
generating an alert; and/or
preventing the instruction from being executed.
5. The system of claim 1 , wherein:
the at least one policy comprises a safety policy; and
the policy enforcement hardware is further configured to enforce a security policy, and/or is further configured to enforce a privacy policy.
6. The system of claim 5 , wherein:
the policy enforcement hardware is further configured to enforce the security policy; and
the security policy comprises an information flow integrity policy.
7. The system of claim 1 , wherein:
maintaining metadata comprises associating metadata with the instruction in the application code; and
the enforcement hardware is configured to attempt to match the instruction in the application code to a transition in the state machine based on the metadata associated with the instruction.
8. The system of claim 1 , wherein:
maintaining metadata comprises associating metadata with data manipulated by the instruction in the application code; and
the enforcement hardware is configured to attempt to match the instruction in the application code to a transition in the state machine based on the metadata associated with the data manipulated by the instruction.
9. A method implemented by a system comprising enforcement hardware, the method comprising an act of:
executing, at run time, a state machine in parallel with application code, comprising:
maintaining metadata that corresponds to one or more state variables of the state machine;
matching instructions in the application code to transitions in the state machine; and
in response to determining that an instruction in the application code does not match any transition from a current state of the state machine, causing an error handling routine to be executed, wherein:
the enforcement hardware comprises policy enforcement hardware configured to check run time behavior of the application code against at least one policy; and
the at least one policy comprises rules corresponding to transitions in the state machine.
10. The method of claim 9 , wherein:
the state machine represents a safety property to be enforced while the application code is executed.
11. The method of claim 9 , wherein:
the instruction comprises a first instruction; and
executing the state machine in parallel with the application code further comprises:
in response to determining that a second instruction in the application code matches a transition from a current state of the state machine, performing a metadata update according to the matched transition.
12. The method of claim 9 , wherein causing an error handling routine to be executed comprises:
generating an alert; and/or
preventing the instruction from being executed.
13. The method of claim 9 , wherein:
the at least one policy comprises a safety policy; and
the policy enforcement hardware is further configured to enforce a security policy, and/or is further configured to enforce a privacy policy.
14. The method of claim 13 , wherein:
the policy enforcement hardware is further configured to enforce the security policy; and
the security policy comprises an information flow integrity policy.
15. The method of claim 9 , wherein:
maintaining metadata comprises associating metadata with the instruction in the application code; and
matching instructions in the application code to transitions in the state machine comprises attempting to match the instruction in the application code to a transition in the state machine based on the metadata associated with the instruction.
16. The method of claim 9 , wherein:
maintaining metadata comprises associating metadata with data manipulated by the instruction in the application code; and
matching instructions in the application code to transitions in the state machine comprises attempting to match the instruction in the application code to a transition in the state machine based on the metadata associated with the data manipulated by the instruction.
17. At least one non-transitory computer-readable medium having encoded thereon instructions configured to program at least one processor to perform a method comprising an act of:
executing, at run time, a state machine in parallel with application code, comprising:
maintaining metadata that corresponds to one or more state variables of the state machine;
matching instructions in the application code to transitions in the state machine; and
in response to determining that an instruction in the application code does not match any transition from a current state of the state machine, causing an error handling routine to be executed, wherein:
the at least one processor is programmed to check run time behavior of the application code against at least one policy; and
the at least one policy comprises rules corresponding to transitions in the state machine.
18. The at least one non-transitory computer-readable medium of claim 17 , wherein:
the state machine represents a safety property to be enforced while the application code is executed.
19. The at least one non-transitory computer-readable medium of claim 17 , wherein:
the instruction comprises a first instruction; and
executing the state machine in parallel with the application code further comprises:
in response to determining that a second instruction in the application code matches a transition from a current state of the state machine, performing a metadata update according to the matched transition.
20. The at least one non-transitory computer-readable medium of claim 17 , wherein causing an error handling routine to be executed comprises:
generating an alert; and/or
preventing the instruction from being executed.
21. The at least one non-transitory computer-readable medium of claim 17 , wherein:
the at least one policy comprises a safety policy; and
the at least one processor is further programmed to enforce a security policy, and/or is further programmed to enforce a privacy policy.
22. The at least one non-transitory computer-readable medium of claim 17 , wherein:
the at least one processor is further programmed to enforce the security policy; and
the security policy comprises an information flow integrity policy.
23. The at least one non-transitory computer-readable medium of claim 17 , wherein:
maintaining metadata comprises associating metadata with the instruction in the application code; and
the at least one processor is programmed to attempt to match the instruction in the application code to a transition in the state machine based on the metadata associated with the instruction.
24. The at least one non-transitory computer-readable medium of claim 17 , wherein:
maintaining metadata comprises associating metadata with data manipulated by the instruction in the application code; and
the at least one processor is programmed to attempt to match the instruction in the application code to a transition in the state machine based on the metadata associated with the data manipulated by the instruction.
25. The at least one non-transitory computer-readable medium of claim 17 , wherein:
the at least one processor comprises at least one field-programmable gate array (FPGA).