  In many industries, the importance of software components provided by
third-party suppliers is steadily increasing. As the suppliers seek to secure
their intellectual property (IP) rights, the customer usually has no direct
access to the suppliers' source code, and is able to enforce the use of
verification tools only by legal requirements. In turn, the supplier has no
means to convince the customer about successful verification without revealing
the source code. This paper presents an approach to resolve the conflict
between the IP interests of the supplier and the quality interests of the
customer. We introduce a protocol in which a dedicated server (called the
"amanat") is controlled by both parties: the customer controls the verification
task performed by the amanat, while the supplier controls the communication
channels of the amanat to ensure that the amanat does not leak information
about the source code. We argue that the protocol is both practically useful
and mathematically sound. As the protocol is based on well-known (and
relatively lightweight) cryptographic primitives, it allows a straightforward
implementation on top of existing verification tool chains. To substantiate our
security claims, we establish the correctness of the protocol by cryptographic
reduction proofs.
