Verification Across Intellectual Property Boundaries
Sagar
Chaki, Christian Schallhart, Helmut Veith,
Proceedings of the 19th International Conference on Computer
Aided Verification (CAV), LNCS 4590, page 82-94, July 3-7,
2007
Abstract:
In many industries, the share 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, and other measures for
enhancing software quality, 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 a
new 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.
PDF /
Online
© Springer