Semantics and correctness

  We describe just enough of our semantics so that we can state our correctness properties. A full semantics can be found in a separate paper [6].

The basis of QCM is the named relational algebra, which can be found in any standard database textbook (e.g., [1]). A QCM program is a set of definitions,

$$R_1=M_1, \ldots, R_n=M_n$$

where each $R_i$ is a relation symbol and each $M_i$ is a relational algebra expression. We require the definitions to typecheck, and we do not permit recursive definitions. We saw several examples of QCM programs in the last section.

QCM programs interact by exchanging database queries and responses. A response is a certificate

$$\textbf{$q$\space says $M\supseteq N$}$$

where M is a relational algebra query and N is a table. A query is a certificate

$$\textbf{$p$\space asks $M$\space noting $C$}$$

where M is the relational algebra query, and C is a set of response certificates submitted along with the query.

The exchange of messages and verification of signatures is specified by an automaton, which we do not describe fully here; the examples of the last section show some of the details. The main task of the automaton is to gather a set of inclusions,

$$M_1\supseteq N_1, \ldots, M_n\supseteq N_n,$$

that will be used to evaluate queries. These inclusions are gathered from responses to queries and also from certificates that are submitted to the automaton along with queries. The main correctness theorem states that the responses a principal issues in fact follow from these inclusions:

Theorem: If (p says $M\supseteq N$), then $M\supseteq N$ is implied by the inclusions of p 's automaton.

There are two important consequences of the theorem. The first is that programmers are justified in thinking of their programs as defining sets--according to the theorem, the answer to a query follows from the inclusions, and does not depend on the sequence of message exchanges used to gather the inclusions.

Second, we must be very careful in what we believe: if the inclusions are inconsistent , then they imply any conclusion $M\supseteq N$. The following example, based on SDSI 1.1, shows that carelessness in this matter can lead to a security breach. We define two groups, $\textbf{school}$ and $\textbf{employees}$:

$$\begin{array} {l} \textbf{school}= \textbf{teachers}\cup \t... ...bf{employees}= \textbf{school}- \textbf{students}. \end{array}$$

Suppose $\textbf{students}$ is maintained by a remote principal, p . In order to decide whether or not a principal q is a member of $\textbf{school}$ or $\textbf{employees}$, we require a document, signed by p , stating whether or not q is a member of $\textbf{students}$: that is, a certificate (p says $q\in\textbf{students}$), or (p says $q\not\in\textbf{students}$). Suppose an `error' occurs and we are presented with both certificates. This might seem impossible, but the set of students is bound to change (students graduate) so an adversary could collect contradictory certificates over time and submit them together. Since $q\in\textbf{students}$, by the first definition we have $q\in\textbf{school}$. And then since $q\not\in\textbf{students}$, we have $q\in\textbf{employees}$--even though q was never a teacher or administrator!

In our full QCM paper, we show how this can be prevented by an automatic analysis that rejects certificates that could cause inconsistencies.