Axe, an automated formal equivalence checking tool for programs
Abstract/Contents
- Abstract
- This dissertation describes Axe, an automated formal verification tool for proving equivalence of programs. Axe has been used to verify real-world Java implementations of cryptographic operations, including block ciphers, stream ciphers, and cryptographic hash functions. Axe proves the bit-for-bit equivalence of the outputs of two programs, one of which may be a formal, mathematical specification. To do so, Axe relies on a novel combination of techniques from combinational equivalence checking and inductive theorem proving. First, the loops in some programs can be completely unrolled, creating large loop-free terms. Axe proves the equivalence of such terms using a phased approach, including aggressive word-level simplifications, bit-blasting, test-case-based identification of internal equivalences, and ``sweeping and merging.'' For loops that cannot be unrolled, Axe uses execution traces to detect loop properties, including loop invariants for single loops and connection relationships between corresponding loops. Axe proves such properties inductively. In many cases, synchronizing transformations must be performed to align the loop structures of the programs being compared; Axe can perform and verify a variety of these transformations.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2011 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Smith, Eric Whitman |
|---|---|
| Associated with | Stanford University, Computer Science Department |
| Primary advisor | Dill, David L |
| Thesis advisor | Dill, David L |
| Thesis advisor | Engler, Dawson R |
| Thesis advisor | Mitchell, John |
| Advisor | Engler, Dawson R |
| Advisor | Mitchell, John |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Eric Whitman Smith. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph.D.)--Stanford University, 2011. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2011 by Eric Whitman Smith
Also listed in
Loading usage metrics...