User and Evaluator Expectations for Trusted Extensions

David S. Hardin
Rockwell Collins, Inc.

Industrial users of Interactive Theorem Provers (ITPs) value the high
degree of trust that can be placed in them, especially in a
high-assurance security evaluation context.  The complexity of
industrial targets of evaluation have motivated users to consider
external solvers, connections to other ITPs, etc., in order to
expedite the verification process.  Such external extensions cannot be
adopted casually, however, lest the trust story be compromised.  In
this talk, we discuss expectations and issues in the creation and use
of Trusted Extensions from the user and evaluator perspective,
including the vetting of external tools, correctness of the
translation from one tool input form to another, production of uniform
evaluation evidence, and tool "version drift" (potentially resulting
in regressions over time).