Our proposed infrastructure is strongly influenced by ideas from programming language research. In our view, security protocols are simply programs, and security breaches are the result of program bugs. Security can thus be enhanced by incorporating techniques from programming languages that eliminate entire classes of bugs from programs. For example, automatic memory management is a language feature that relieves programmers from explicitly allocating and deallocating data: allocation and deallocation instructions are inserted by the language implementation. Not only does this make programs easier to write and understand, it also eliminates dangling pointer bugs. Such bugs are common in languages with explicit memory management, and can lead to security failures; Rivest reports that they were the largest class of bugs encountered in implementing the security infrastructure SDSI [personal communication].
If memory management is hard to get right, cryptography and protocol design are even harder. Many cryptographic protocols designed by experts have turned out to be flawed, and application programmers are not experts in cryptographic algorithms, security protocols, and formal methods. Even when provided with formally verified, bug-free cryptography and protocols, they still build insecure systems [2,3]. Taking automatic memory management as a guide, we seek to eliminate security bugs by hiding the use of cryptography, protocols, and message exchange from the programmer. Instead, the basic primitive we provide is authenticated data distribution , and we implement it by the automatic management of queries and certificates . Hence, the system is called the Query Certificate Manager , or QCM .
Common examples of authenticated data distribution include obtaining public keys or access control information from remote servers. These examples can be implemented in more than one way; for example: (1) by sending queries and responses over an authenticated channel between client and server; or (2) by means of certificates signed by the remote server and submitted to the client. The important thing to note is that the application programmer does not care how the remote information is obtained; he only cares that the correct information is obtained. Since the means of obtaining the data--cryptography and message exchange in (1), and careful examination of signatures in (2)--are complicated and error-prone, they should not be the responsibility of the typical programmer.
In our system, programmers do not write message-sending code to obtain remote data; the necessary messages are sent automatically by the query management system. To ensure authenticity, queries and replies are digitally-signed certificates; but programmers do not write code to verify signatures. This is done automatically by the certificate management system. And if certificates from remote servers are submitted to the system, messages to the remote servers are short-circuited, again automatically.
A second way in which we have been inspired by programming languages is in our use of formal methods. Like many programming languages, our system has a formal semantics, based on automata theory and a model of sets and relations. Having a semantics has proven invaluable in designing QCM, and places no burden on the users of QCM. For users, the semantics insures that all programs written in QCM have a sensible meaning: they define sets and relations. Thus, programmers do not need to understand the complicated semantics of message exchange and signature verification; they are justified in thinking of their programs as defining sets. This is in sharp contrast with security infrastructures based on message exchange and cryptography, where the users of the infrastructure typically need to use formal methods to have any assurance of security in their protocols.
The semantics has helped our design in several ways. First, a semantics is necessary in order to state and prove properties of the system, and so the semantics is fundamental to the correctness of our system. Second, in stating our correctness properties, we discovered some subtleties involving the contents of certificates, which could never be caught by a formal proof of correctness for the cryptographic protocols; see §3. This led us to an automatic analysis, consistency checking , that catches certain bugs that could lead to security failures, and that are likely to be overlooked by the application programmer.
Notice that our correctness properties are proved once for the QCM system. They then apply to any program written in QCM; no further correctness proof is needed. Essentially, we implement a QCM program by a protocol of message exchange and signature verification, and we have proven the correctness of a large class of protocols, namely, the protocols corresponding to all QCM programs.
There have been many other recent proposals for managing certificates, including PolicyMaker [4], SDSI [7], and SPKI [5]. These systems include only limited support for distributed database operations (to form groups, define access control lists, provide for queries about identity certificates, and so on). But we think that application programmers will need to interface with existing database systems--for example, databases of customers--in order to support some of their intended applications. Therefore, we have designed QCM as a database language, and we directly support database integration. This avoids redundancy with technology already developed by the database community, and we can take advantage of new algorithms developed for databases on the web.
The remainder of the paper presents an informal overview of QCM, omitting most technical details. A complete definition can be found in a separate paper [6]. In §2 we give some examples of QCM programming. In §3 we discuss our semantics and correctness guarantees, and we conclude in §4.