Page 254 - DCAP305_PRINCIPLES_OF_SOFTWARE_ENGINEERING

Principles of Software Engineering

Notes Specification Structure Metrics
The user is presented with a summary of the architectures of the original and the extracted
specifications. This allows comparison so as to get an idea of the difficulty of implication proof.
All the metrics are subjective, and we do not have specific values that would give confidence
in the ability of the PVS theorem proves to complete the implication proof.
We developed the following heuristics to both select transformations and determine the order
of application:
• Dependent transformations are applied in order.
• Transformations that impact the major sources of difficulty, such as code and VC size, are
applied first.
• Transformations that affect global structure are applied earlier and those that affect local
structure are applied later.
• Refactoring proceeds until all proofs are possible.
• Refactoring proceeds until all subprograms can easily annotate.

• And the program structure “matches” the specifications. In practice, if specification
extraction or either of the proofs fails to complete, or if either proof is unreasonably
difficult, the user returns to refactoring and applies additional transformations.
12.4.1 Verification Refactoring

The Advanced Encryption Standard (AES) implementation employs various optimizations
(including implementing functions using table lookups, fully or partially unrolling loops,
and packing four 8-bit bytes into a 32-bit word) that improved performance but also created
difficulties for verification. For instance, the SPARK tools ran out of resources on the original
program because the unrolled loops created verification conditions that were too large.

We applied a total of 50 refactoring transformations in eight categories. Of those 50, the following
38 transformations from six categories were selected from the prototype Echo refactoring library
(the number after the category name is the number of transformations applied in that category):
rerolling loops (5); reversing inline functions or cloned code (11); splitting procedures (2); moving
statements into or out of conditionals (3); adjusting loop forms (4); modifying redundant or
intermediate computations (2); and modifying redundant or intermediate storage (11). The
rationale and use of these transformations are discussed in the next section.
In addition to the transformations above, we also added two new categories of transformations
specifically for AES:
Adjusting Data Structures
The 32-bit words were replaced by arrays of four bytes, and sets of four words were packed into
blocks or states as defined by the specification. Constants and operators on those types were
also redefined accordingly to reflect the transformations.
Reversing Table Lookups
The table lookups were replaced with explicit computations based on the original documentation
and the precompiled tables removed. Both of these two added transformation types were driven
by the goal of reversing documented optimizations and matching the extracted specification
to the original specification. The final refectories AES program contained 25 functions and was
506 lines long.

248 LOVELY PROFESSIONAL UNIVERSITY