Type-preserving compiler for security verification
US8955043B2 · kind B2 · utility
4Cited by
4References
20Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Jan 27, 2010 |
| Grant date | Feb 10, 2015 |
| Priority date | — |
| Expiry date | Aug 22, 2032 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F21/54
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.