Type-preserving compiler for security verification
Described is a source program code language that facilitates the association of security proofs obtained from a solver (e.g., a Z3 theorem prover) with the program code. The code may include affine types, dependent types and/or refinement types. A derefinement procedure replaces each refinement type with a dependent pair type corresponding to the proof. A target code type checker verifies the target code with respect to the security policies. If verified as complying with security policy, a verified program corresponding to the translated program may then be installed and run.
1. A system comprising:
at least one processor; and
a memory communicatively coupled to the at least one processor; and
one or more software components stored on the memory comprising:
a compiler component to compile source program code written in a source language that integrates affine types with dependent types and refinement types,
wherein the compiler component further includes a type checker component coupled to a solver component to obtain proofs of refinement formulas from the solver component,
wherein the compiler component further to:
translate the source program code into target code having the proofs associated with the target code,
verify security policies, and
translate each value of a refinement type within the source program into a proof term of a corresponding refinement formula.
2. The system of claim 1 , wherein the compiler component translates the source program code into target code associated with the proofs through replacement of each refinement type with a dependent pair comprising a value and proof.
3. The system of claim 2 , wherein the target code preserves types used in the source program code, the types corresponding to the source language.
4. The system of claim 1 , wherein the compiler component extracts proofs from the solver component as values.
5. The system of claim 1 , wherein the target code comprises dependent common intermediate language corresponding to .NET code.
6. The system of claim 1 , the compiler component further comprising a target code type checker component that verifies the target code with respect to the security policies.
7. The system of claim 1 , wherein the solver component is internal or external to the compiler component.
8. The system of claim 1 , wherein the target code comprises a plugin component.
9. A method employing at least one processor to perform steps, comprising:
compiling, via the at least one processor, source program code having refinement types, dependent types, and affine types that correspond to a state of an authorization policy,
wherein the compiling step further includes
extracting security proofs of refinement formulas from the source program code; and
translating the source program code into type-preserving target code,
wherein the translating step further includes replacing each refinement type with a dependent pair type that associates the security proofs with the target code.
10. The method of claim 9 , wherein extracting the security proofs further comprises providing the source program code to a theorem prover that provides information to a compiler that compiles the source code.
11. The method of claim 9 , wherein compiling the source program code further comprises type checking the source program code.
12. The method of claim 9 , further comprises verifying the target code by performing type checking.
13. The method of claim 9 , further comprising:
verifying that the target code complies with security policy; and
allowing installation of a verified program corresponding to the target code.
14. The method of claim 9 , wherein replacing each refinement type further comprises placing the security proofs as values in the source program code.
15. The method of claim 9 , wherein translating the source program code further comprises producing the type-preserving target code as code that corresponds to .NET common intermediate language runtime code.
16. The method of claim 9 , wherein producing the type-preserving target code further includes providing type-level functions, classes parameterized by values, or affine types, or any combination of type-level functions, classes parameterized by values, or affine types.
17. One or more physical computer-readable storage media having computer-executable instructions, which when executed perform steps, comprising:
compiling source program code that has refinement types into a source program, wherein the compiling step further includes
type checking the source program code,
extracting security proofs of refinement formulas by communicating with a solver, and
replacing each refinement type with security proofs comprising values in the source program code;
translating the source program into a target program; and
type checking the target program to verify whether the target program complies with security policy.
18. The one or more physical computer-readable storage media of claim 17 , wherein compiling the source program code further comprises processing affine types that correspond to a state of an authorization policy.
19. The one or more physical computer-readable storage media of claim 17 ,
wherein type checking the target program determines that the target program complies with security policy, and
wherein having further computer-executable instructions comprising:
allowing installation of the target program.
20. The one or more physical computer-readable storage media of claim 19 ,
wherein type checking the target program is performed on a computing system on which the target program is installed, and
wherein the computing system does not include the solver.