**[BOARD OF ADVISORS & STANDARDS BOARD]{.underline}**

**[VVSG TRAINING WORKSHOP]{.underline}**

**[John Wack- Logic Verification, OCTOBER 16, 2007]{.underline}**

**[NIST BOULDER]{.underline}**

**(START OF AUDIOTAPE 1, SIDE A)**

JOHN WACK: First I would like to preface my final topic with an erratum
from my presentation yesterday. I'm looking at a slide titled 7.7
Counting. Its page 87, talking about subsection 775 accuracy. On here I
have a bullet that says "shall reject marginal marks." The reference
requirement is in fact a "should." So, I apologize for that mistake.

Yesterday there was one significant change from the previous guidelines
that I did not get a chance to talk about. I'm going to talk about that
for fifteen minutes this morning. That is logic verification beginning
on page 101, title slide "Logic Verification, part III, section 4.6."

What is Logic Verification? This is in fact a new test method that is
described for the first time in this iteration of the guidelines. Logic
Verification is formal characterization of software behavior within a
carefully restricted scope followed by proof that this behavior conforms
to specified assertions such as that votes are reported correctly in all
cases. This compliments what we usually mean by testing which is
sometimes called "falsification testing" to contrast it with
verification.

The difference is this. When you are talking about falsification
testing, if an implementation fails the test, you have demonstrated
non-conformity. If it passes the test, you haven't necessarily
demonstrated conformity.

The goal of verification is actually to build confidence, positive
evidence of conformity to certain requirements. This particular method
has, within the field of computer science, been referred to by various
names including "inductive assertions," "core logic," and "program
proving."

The motivation for adding this test -- is there a question?

FEMALE SPEAKER 1: Yes. Where is that in the Guidelines?

MALE SPEAKER 1: Part III, section 4.6.

MALE SPEAKER 2: Chapter 4, page 48 of Part III.

MALE SPEAKER 1: So this was responsive to a TGDC resolution and it also
helps to give a higher level of assurance in operational testing along
and to clarify the objectives of source code review.

The way it works is that, oh, dear, I said vendor instead of
manufacturer. The manufacturer specifies pre and post conditions of
reach callable unit and unfortunately, I've now delved into some jargon
I didn't introduce earlier. We are talking about discrete units of
software, individual pieces of software. Each piece of software will
essentially have a contract for what that piece of software does which
has been specified by the manufacturer.

Using these contract it should then be possible to prove assertions
about the correctness of tabulation by composing these contracts
together. If this goes in, that should come out. If you add several of
these together in a string, you eventually get to a conclusion about the
correctness of tabulation.

Having this information provided by the vendor testing authority is
responsible for reviewing, checking the math and logic, and issuing
findings that ideally will show that the pre and post conditions
correctly characterized the software and that the assertions are
satisfied.

What I have described at a very high level sounds very much like an
activity in the software engineering profession creates fear and
loathing all around because it is identified with a very detailed, very
rigorous analysis that is very expensive to complete. What is required
in the guidelines has significant compromises to bring it into a more
pragmatic level that we can actually do.

Compromise number 1 is that the scope has been limited to core logic.
Core logic is defined as a subset of application logic that is
responsible for vote recording and tabulation. If you think about it,
this is excluding a million lines of code and the user interface. Its
excluding the ten million lines of code in the COTS operating system. We
really are just looking at the core, if you will, of the actual vote
counting process.

Limiting the scope in this way does limit our assurance but if we don't
limit the scope what we have is an analysis process that is not
practical to complete during the conformity assessment process.

The second compromise has to do with how formal, what level of rigor is
going to be required in this analysis. We know already that we are not
guaranteed that the programing language being used has formally
specified semantics, so a completely formal proof cannot be mandated.

Nevertheless it is worthwhile to work through this analysis with as much
formality as possible, using informal arguments where its not. Also,
relying on limitations on the complexity of software units to make the
correctness at the lowest level intuitively obvious. Although there has
been significant compromises with respect to the rigor of this process,
its still better than operational testing alone. We still have some
additional assurance of the correctness of the software, more than what
we would have if we simply did operational testing.

The practical impact of this as anticipated in the conformity assessment
process, is that it boils down to another document that manufacturers
have to produce. The production of this document will require a computer
science undergraduate skill level but that's not expected to be a big
hardship. As I said, it will give a higher level of assurance and
operational testing alone.

Part if the impact also I would expect will be some fear about just how
difficult this process is going to be. As I have discussed in previous
slides, the attempt has been made to limit the difficulty of completing
this process to something that is possible and practical to complete.

When people hear logic verification the first thing that flashes into
their mind is, oh my gosh this is common criteria, highest evaluation
assurance level. They are thinking about the military systems and things
that have gone through very, very expensive verifications.

The case needs to be made repeatedly that this is not that. This is what
we can accomplish within the resources that we realistically have here.
Its been limited both in scope and rigor to what is practical to
accomplish. Question?

FEMALE SPEAKER 2: I don't disagree with you because I understand why its
doing that, I think -- what kinds of things go through the higher level?

(TOO FAR FROM MICROPHONE TO BE UNDERSTOOD).

JOHN WACK: The question was can I related this to where it falls with
respect to other industries such as gaming software and military
systems, where this falls in the scope of rigor.

With respect to the military systems, here we are talking about systems
where security and related requirements were the number one, absolute
top priority and the system was built from the ground up so that these
requirements could be demonstrated and verified. So, this imposes severe
limitations on the complexity of the system you can build. Here is your
set of security requirements, everything else follows from this. You
don't get to write election law that contradicts this. You don't get to
modify it in any way. These are the rules. All these systems are really
classified and I know nothing about them.

With respect to gaming systems, I should probably hand it over to the
folks from Nevada to talk about that. I've heard it said that the amount
of money available for engineering and verification validation of gaming
systems is significantly greater than what's available on elections. Its
less than what is spent on military systems.

That basically gives you the hierarchy here. We are talking about doing
an exercise here that is slightly more than what the average software
shop does because they are not required to do, but its not subject to
the same regulatory apparatus that gaming systems are.

What it boils down to really, since there is a limitation on rigor, this
is going to force another review of the code. Its going to force people
to go back and read the code again and make sure its correct. That's
pretty much always a good thing.

Now, backing up to what I intend to be my final slide, page 100, Title
Related Requirements. This cites other sections of the document that
have impact on logic verification which is Part III, section 4.6.

There is a requirement in Part I that the vote recording and tabulation
be verifiably correct, meaning you can't deliver a system that is so
obfuscated that you can't even do this in formal exercise to show that
its correct.

There is a requirement 632(a) that integrity restraints be satisfied,
meaning votes will be counted correctly. There is a series of
documentation requirements that oblige the vendors to provide the
material that I described that is necessary to perform the verification.

I have three minutes left of my fifteen minutes slot so, if there is any
further questions on this I can answer them. Hearing none, I will hand
it over to the next subcommittee.

Thank you very much.