Chapter 4: Documentation and Design Reviews (Inspections)

An inspection or review is logically reported as one or more tests with a verdict of Pass or Fail. The number of tests reported corresponds to how the test lab chooses to structure the inspection.

To the extent possible, these VVSG provide guidance on the criteria to be applied. However, the nature of some of these inspections is to rely on the professional judgment of an expert reviewer to assess conformity with general guidelines.

4.1 Initial Review of Documentation

The accredited test lab reviews the documentation submitted by the manufacturer for its completeness and satisfaction of requirements.

4.2 Physical Configuration Audit

The Physical Configuration Audit (PCA) is the formal examination of the as-built version of a voting system against its design documentation in order to establish the product baseline. After successful completion of the audit, subsequent changes are subject to test lab review and reexamination.

4.4 Manufacturer Practices for Quality Assurance and Configuration Management

4.4.1 Examination of quality assurance and configuration management data package

4.4.2 Examination of voting systems submitted for testing

These requirements deal with the quality assurance and configuration examination of voting systems submitted for testing to a test lab.

4.4.2.1 Configuration management

4.5 Source Code Review

In the source code review, the accredited test lab will look at programming completeness, consistency, correctness, modifiability, structure, modularity and construction.

4.5.1 Workmanship

Although these requirements are scoped to application logic, in some cases the test lab may need to inspect border logic and third-party logic to assess conformity. Per Requirement Part 2: 3.4.7.2-E, the source code for all of these must be provided.

4.5.2 Security

4.6 Logic Verification

This inspection is to assess conformity with Requirement Part 1: 6.3.2-A and related requirements.

Because of its high complexity, the scope of logic verification is pragmatically limited to core logic. Software modules that are solely devoted to interacting with election officials or voters or formatting reports are not subject to logic verification. However, they are required to conform with Requirement Part 1: 6.1-A, the testing of which is described in Part 3: 4.3 “Verification of Design Requirements” and Part 3: 4.5.2 “Security”.

Although these requirements are scoped to core logic, in some cases the test lab may need to inspect other application logic, border logic and third-party logic to assess conformity. Per Requirement Part 2: 3.4.7.2-E, the source code for all of these must be provided.

[Redmill88] provides the following description of logic verification, therein known as "program proving:"

Assertions are made at various locations in the program, which are used as pre-, and post-conditions to various paths through the program. The proof consists of two parts. The first involves showing that the program transfers the pre-conditions into the post-conditions according to a set of logical rules defining the semantics of the programming language, provided that the program actually terminates (i.e., reaches its proper conclusion). The second part is to demonstrate that the program does indeed terminate (e.g., does not go into an infinite loop). Both parts may need inductive arguments.

The inspection specified here does not assume that the programming language has formally specified semantics. Consequently, a formal proof at any level cannot be mandated. Instead, a combination of informal arguments (see Requirement Part 2: 3.4.7.2-F.b) and limitations on complexity (see Requirement Part 1: 6.4.1.4-B.1) seeks to make the correctness of callable units at the lowest level intuitively obvious and to enable the verification of higher level units using the correctness of invoked units as theorems. The resulting inspection is not as rigorous as a formal proof, but still provides greater assurance than is provided by operational testing alone.

Inasmuch as the following behaviors would almost certainly preclude a demonstration of the correctness of the logic, logic verification will almost certainly involve a demonstration that they cannot occur:

• Numeric errors such as overflow and divide-by-zero;
• Buffer overruns / out-of-bounds accesses of arrays or strings;
• Null pointer dereferences;
• Stack overflows;
• Invocations of undefined or implementation-dependent behaviors;
• Race conditions or other nondeterministic execution;
• Abrupt termination.

It is acceptable, even expected, that logic verification will show that some or most exception handlers in the source code cannot logically be invoked. These exception handlers are not redundant—they provide defense-in-depth against faults that escape detection during logic verification and unpredictable failures that compromise the system.